| Interface | Description |
|---|---|
| GlobalSymbol |
The interface to a symbol that can be globally referenced.
|
| Symbol |
The interface to symbols.
|
| VariableSymbol |
The interface to a symbol denoting a variable.
|
| Class | Description |
|---|---|
| AxiomSymbol |
A symbol denoting a logical axiom.
|
| BodySymbol |
The symbol for a variable introduced in a method/constructor body.
|
| Checking |
Type-check a class declaration and annotate it semantically.
|
| ClassMethodSymbol |
A symbol denoting a class method.
|
| ClassSymbol |
A symbol denoting a class.
|
| ClassVariableSymbol |
A class value.
|
| ConstructorSymbol |
A symbol denoting a class constructor.
|
| Environment |
An environment giving meaning to identifiers.
|
| FormulaSymbol |
A symbol denoting a logical formula.
|
| FreeVariables |
Compute the free variables of an expression (revised version).
|
| GlobalSymbolBase |
The base class of a symbol that can be globally referenced.
|
| GlobalVariableSymbolBase |
The base class of a variable symbol that can be externally referenced.
|
| LocalVariableSymbolBase |
The base class for a variable symbol that can be only locally referenced.
|
| LogicChecking |
Type-check a logical theory.
|
| LogicEnvironment |
An environment giving meaning to identifiers in the logic context.
|
| LogicTypeTable |
Make logic type expressions unique such that they can be compared by reference.
|
| MethodSymbol |
A symbol denoting a method.
|
| NewVariables |
Create new variables that are not used variables in an expression.
|
| ObjectMethodSymbol |
A symbol denoting an object method.
|
| ObjectVariableSymbol |
An object value.
|
| PackageSymbol |
A symbol denoting a value.
|
| ParameterSymbol |
The symbol for a method/constructor parameter.
|
| ParamSymbol |
A symbol denoting a parameterized entity.
|
| ParamSymbols<S extends ParamSymbol> |
A set of parameterized symbols.
|
| ParamSymbolTable<S extends ParamSymbol> |
A table of parameterized symbols.
|
| PostStateCloner |
Clone a formula transforming all state references to the post-state.
|
| PreStateCloner |
Clone a formula transforming all state references to the pre-state.
|
| ReferenceCloner |
Clone an expression transforming all references to certain symbols.
|
| ReferencedExcs |
Compute the exception types referenced by an expression.
|
| ReferencedUnits |
Compute the units (theory/class) referenced by a unit.
|
| ReferencedVars |
Compute the program variables referenced by an expression.
|
| SymbolBase |
The base class of symbols.
|
| SymbolTable<S extends Symbol> |
A symbol table.
|
| TCCGenerator |
A generator of type-checking conditions (tccs).
|
| TheorySymbol |
A symbol denoting a theory.
|
| ThisSymbol |
The symbol for "this" object in a non-static context.
|
| TypeCloner |
Clone a type expression transforming references to certain symbols.
|
| TypeSymbol |
A symbol denoting a logical type.
|
| TypeTable |
Make type expressions unique such that they can be compared by reference.
|
| TypeTranslator |
Translate program types to logical types.
|
| UsedVariables |
Compute the (logic) variables/constants used in an expression.
|
| ValueSymbol |
A symbol denoting a logical value.
|
| VariableSymbolBase |
A symbol denoting a variable.
|
| VariableTypes |
Set logical types of all variables declared in program.
|