fmrisc.ProgramExplorer.Judgements

Class Propagator

java.lang.Object

fmrisc.ProgramExplorer.Judgements.Propagator

public final class Propagator
extends java.lang.Object

Propagate pre/postconditions through a statement.

Method Summary

Modifier and Type	Method and Description
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) Propagate condition through statement.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

execute

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)

Propagate condition through statement.

Parameters:

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.