public final class Pre
extends java.lang.Object
Constructor and Description |
---|
Pre(StateType stype)
Create a judgement processor.
|
Modifier and Type | Method and Description |
---|---|
Formula |
derive(Statement C,
Formula Q)
Apply the judgement "se, Is, VS |- pre(C, Q) = P"
to compute the precondition P of command C with respect to postcondition Q
and to generate proving tasks as a side effect
(see Section 4.11 of "A Program Calculus", se, Is, Vs are not needed
because identifiers have already been resolved to symbols).
|
public Pre(StateType stype)
stype
- the current state type.public Formula derive(Statement C, Formula Q)
C
- the command C with judgement attached.Q
- the formula Q