Averest


QModule Type

typed 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 refers to the (absolute path) of the root directory where import paths and qualified module names are referred from
  • declStmt is the core of a Quartz module, i.e., the various kinds of declarations with the typed body statement
  • obsrvSpecL is the list of specifications that may be endowed with observers
  • driverL is the list of drivers that may be used to generate closed systems for simulation

Record fields

Record Field Description

declStmt

Full Usage: declStmt

Field type: DeclStmt

Field type: DeclStmt

driverL

Full Usage: driverL

Field type: DeclStmt list

Field type: DeclStmt list

obsrvSpecL

Full Usage: obsrvSpecL

Field type: (DeclStmt option * ProofGoal list) list

Field type: (DeclStmt option * ProofGoal 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