Interface | Description |
---|---|
SemanticCheck |
A common subclass for semantic checks
|
Class | Description |
---|---|
ClausesCheck |
This class checks several dependencies between machine clauses.
|
ClausesCollector | |
DefinitionCollector |
Collects the
APredicateDefinitionDefinition ,
ASubstitutionDefinitionDefinition
and
AExpressionDefinitionDefinition
nodes, i.e. |
DefinitionPreCollector |
Collects the
ADefinition nodes which were found by the PreParser and
stores them into a mapping "definition identifer" -> "rhs of definition". |
DefinitionUsageCheck | |
IdentListCheck |
In several constructs the BParser only checks if a list of identifiers is a
valid list of expressions instead of checking if each entry is an identifier
expression.
|
PrimedIdentifierCheck |
This semantic check looks for occurrences of primed identifiers like x$0 and
checks that the number behind the dollar symbol is 0 in any case if
ParseOptions.restrictPrimedIdentifiers is true
Note, this semantic check do not ensure that a primed identifier only occurs
at a correct place, i.e. |
ProverExpressionsCheck |
Semantic check for expressions that can only be used in the prover, not
standard B machines
|
SemicolonCheck |
This class checks that there is non missing semicolon between two operations.
|