Class | Description |
---|---|
ExpressionLogic | |
ExpSubstitution |
The expression substitution P[E1/E2]
|
Normalization |
Normalize a specification formula with respect to the set of modified variables.
|
Post |
The judgement "se, Is, VS |- post(C, P) = Q"
|
Pre |
The judgement "se, Is, VS |- pre(C, Q) = P"
|
Propagator |
Propagate pre/postconditions through a statement.
|
RefSubstitution |
Reference substitution P[T1/I1,...]
|
Satisfies |
The judgement "se, Is, VS |- C: F"
|
Simplification |
Simplify a specification formula to make it easier understandable.
|
Simplification2 |
Post-processing of a specification formula to make it easier understandable.
|
StatJudgement |
A statement judgement.
|
Substitution |
The program variable substitution P[U1/VAR x,...]
|
Substitution.Value |
The substitution for a reference to a program variable.
|
Terminates |
The judgement "se, Is, VS |- C |v J F"
|
Enum | Description |
---|---|
Simplification.Tag |
The following simplifications are implemented:
o Some "quasi-normalization":
(A /\ B) /\ C to A /\ (B /\ C)
(A \/ B) \/ C to A \/ (B \/ C)
A imp (B imp C) to (A /\ B) imp C
This simplifies pretty-printing and further processing.
|
Substitution.Action |