Averest


UtyQModule Type

untyped Quartz modules consist of the following entries (some of them refer to the file from which the module has been read from):

  • quartzFileDir is the name of the file's (absolute path) directory
  • quartzFileName is the name of the Quartz file without suffix ".qrz"
  • rootDir specifies the root directory to which the import paths refer to
  • importPaths determines the directories where called modules are searched; these directories are {rootDir+i { i in importPaths} }
  • macros is a map that stores macro definitions of a Quartz file. It maps the name of the macro function to a pair (xL,tau) where xL is the list of formal arguments and tau the right-hand side of the macro definition. For example, the macro definition "max(a,b) = ((a>b)?a:b)" maps the name "max" to the pair ([a,b],((a>b)?a:b)).
  • utyDeclStmt is an untyped statement with the name of the untyped module, its declarations, and its untyped body statement
  • obsrvSpecL is the list of specifications that may be endowed with observers
  • driverL is the list of drivers that can be used to generate closed systems for simulation

Record fields

Record Field Description

driverL

Full Usage: driverL

Field type: UtyDeclStmt list

Field type: UtyDeclStmt list

importPaths

Full Usage: importPaths

Field type: string list

Field type: string list

macros

Full Usage: macros

Field type: Map<QName, (QName list * UtyExpr)>

Field type: Map<QName, (QName list * UtyExpr)>

obsrvSpecL

Full Usage: obsrvSpecL

Field type: (UtyDeclStmt * UtyProofGoal list) list

Field type: (UtyDeclStmt * UtyProofGoal list) list

quartzFileDir

Full Usage: quartzFileDir

Field type: string

Field type: string

quartzFileName

Full Usage: quartzFileName

Field type: string

Field type: string

rootDir

Full Usage: rootDir

Field type: string

Field type: string

utyDeclStmt

Full Usage: utyDeclStmt

Field type: UtyDeclStmt

Field type: UtyDeclStmt