public final class Propagator extends java.lang.Object
|Modifier and Type||Method and Description|
Propagate condition through statement.
public static void execute(Statement C, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, Satisfies satisfies)
C- a statement that is annotated with statement judgements.
statement- a sub-statement of C.
formula- the formula to be attached to statement.
pre- true iff the formula is a precondition (postcondition else).
preMap- a mapping of statements to preconditions; is extended such that its domain is the set of all sub-statements of C (including C).
postMap- an empty mapping of statements to postconditions; is extended such that its domain is the set of all sub-statements of C (including C).
satisfies- a judgement processor.