Averest


Statements Module

Module Statements implements the data type for typed statements that are obtained from the type-checker implemented in module UtyStmts and are given to the compile functions.

Types

Type Description

DeclStmt

DeclStmt is a data type for typed statements with different kinds of declarations that refer to the contained statement:

  • name is the index of the name of the DeclStmt (in the Nametable)
  • decL is the list of interface variable declarations (inputs, outputs, inouts)
  • orcL is the list of oracles introduced by replacing nondeterminism
  • lblL is the list of names of the control flow locations of the statement
  • lcVL is the list of the local variable declarations
  • lcNL is the list of local names used in assumptions, assertions and module calls
  • stmt is a typed statement

QModule

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

Stmt

Statements is a discriminated union type for storing the core statements of the Quartz language. The QName arguments denote the program locations where the control flow may rest during macro steps except for ModuleCall whose QName arguments denote the name of the call (instance) and the called module (the other arguments are the argument expressions that may be optional).

Functions and values

Function or value Description

SubstStmt rho stmt

Full Usage: SubstStmt rho stmt

Parameters:
Returns: Stmt

Substitution of variables by arbitrary expressions in statements; the substitution rho is a map from QName to Expr as in case of expressions (see file Core/Expressions.sml).

rho : Map<QName, Expr>
stmt : Stmt
Returns: Stmt