Type | Description |
|
|
The datatype QName implements qualified identifiers with explicit genealogy of an identifier. See Names.sig for more information. |
Function or value | Description |
Full Usage:
AssertIndex
Returns: int ref
|
|
Full Usage:
AssumeIndex
Returns: int ref
|
|
Full Usage:
AuxIndex
Returns: int ref
|
|
|
|
Full Usage:
InstanceIndex
Returns: int ref
|
|
Full Usage:
LabelIndex
Returns: int ref
|
|
Full Usage:
LocalVarIndex
Returns: int ref
|
|
|
determine name of index
index
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Full Usage:
NewUniqueName namestub indexref
Parameters:
string
indexref : int ref
Returns: QName
|
generate new names for program locations, module calls, oracles (used in non- deterministic expressions, local variables (used in macro expansions), assumptions, assertions, and runtime exceptions.
|
Full Usage:
OracleIndex
Returns: int ref
|
|
|
|
|
append the name of a package to a qualified name
|
|
|
|
|
|
|
|
select the root index of a qualified name
|
Full Usage:
RteIndex
Returns: int ref
|
|
Full Usage:
TransIndex
Returns: int ref
|
|
|
|
|
|
Full Usage:
nameTableEntries
Returns: int ref
|
|
|
|