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