| 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.
|