Averest


Names Module

Types

Type Description

Index

QName

The datatype QName implements qualified identifiers with explicit genealogy of an identifier. See Names.sig for more information.

Functions and values

Function or value Description

AssertIndex

Full Usage: AssertIndex

Returns: int ref

Returns: int ref

AssumeIndex

Full Usage: AssumeIndex

Returns: int ref

Returns: int ref

AuxIndex

Full Usage: AuxIndex

Returns: int ref

Returns: int ref

InsertName s

Full Usage: InsertName s

Parameters:
    s : string

Returns: Index

s : string
Returns: Index

InstanceIndex

Full Usage: InstanceIndex

Returns: int ref

Returns: int ref

LabelIndex

Full Usage: LabelIndex

Returns: int ref

Returns: int ref

LocalVarIndex

Full Usage: LocalVarIndex

Returns: int ref

Returns: int ref

NameOfIndex j

Full Usage: NameOfIndex j

Parameters:
Returns: string

determine name of index index name of j

j : Index
Returns: string

NewAssertName ()

Full Usage: NewAssertName ()

Parameters:
    () : unit

Returns: QName

() : unit
Returns: QName

NewAssumeName ()

Full Usage: NewAssumeName ()

Parameters:
    () : unit

Returns: QName

() : unit
Returns: QName

NewAuxName stub

Full Usage: NewAuxName stub

Parameters:
    stub : string

Returns: QName

stub : string
Returns: QName

NewDerivedName st

Full Usage: NewDerivedName st

Parameters:
    st : string

Returns: QName -> QName

st : string
Returns: QName -> QName

NewInstanceName ()

Full Usage: NewInstanceName ()

Parameters:
    () : unit

Returns: QName

() : unit
Returns: QName

NewLabelName ()

Full Usage: NewLabelName ()

Parameters:
    () : unit

Returns: QName

() : unit
Returns: QName

NewLocalName ()

Full Usage: NewLocalName ()

Parameters:
    () : unit

Returns: QName

() : unit
Returns: QName

NewOracleName ()

Full Usage: NewOracleName ()

Parameters:
    () : unit

Returns: QName

() : unit
Returns: QName

NewRteName line

Full Usage: NewRteName line

Parameters:
    line : 'a

Returns: QName

line : 'a
Returns: QName

NewUniqueName namestub indexref

Full Usage: NewUniqueName namestub indexref

Parameters:
    namestub : 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.

namestub : string
indexref : int ref
Returns: QName

OracleIndex

Full Usage: OracleIndex

Returns: int ref

Returns: int ref

PackageOfQName qn

Full Usage: PackageOfQName qn

Parameters:
Returns: string

qn : QName
Returns: string

PackageQName iL qname

Full Usage: PackageQName iL qname

Parameters:
Returns: QName

append the name of a package to a qualified name

iL : Index list
qname : QName
Returns: QName

PrnName id

Full Usage: PrnName id

Parameters:
Returns: PrnDrv -> unit

id : Index
Returns: PrnDrv -> unit

PrnQName qn

Full Usage: PrnQName qn

Parameters:
Returns: PrnDrv -> unit

qn : QName
Returns: PrnDrv -> unit

QNameOfPackage pkg i

Full Usage: QNameOfPackage pkg i

Parameters:
Returns: QName

pkg : string
i : Index
Returns: QName

RootOfQName qname

Full Usage: RootOfQName qname

Parameters:
Returns: Index

select the root index of a qualified name

qname : QName
Returns: Index

RteIndex

Full Usage: RteIndex

Returns: int ref

Returns: int ref

TransIndex

Full Usage: TransIndex

Returns: int ref

Returns: int ref

index2NameTable

Full Usage: index2NameTable

Returns: Map<Index, string> ref

Returns: Map<Index, string> ref

name2IndexTable

Full Usage: name2IndexTable

Returns: Map<string, Index> ref

Returns: Map<string, Index> ref

nameTableEntries

Full Usage: nameTableEntries

Returns: int ref

Returns: int ref

prnQName qn

Full Usage: prnQName qn

Parameters:
Returns: int -> PrnDrv -> unit

qn : QName
Returns: int -> PrnDrv -> unit