fmrisc.ProgramExplorer.Judgements

Class Satisfies

java.lang.Object

fmrisc.ProgramExplorer.Judgements.Satisfies

public final class Satisfies
extends java.lang.Object

The judgement "se, Is, VS |- C: F"

Constructor Summary

Constructors

Constructor and Description
Satisfies(ParamSymbol method, StateType stype, TaskFolder invariants, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Create a judgement processor.

Method Summary

Modifier and Type	Method and Description
static Formula	andFormula(Formula formula1, Formula formula2) Combine formulas by conjunction.
static Formula	andFormula(java.util.Vector<Formula> formulas) Combine formulas by conjunction.
StatJudgement	derive(Statement C) Apply the judgement "se, Is, Vs |- C: F" to compute the specification F of command C 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).
static Formula	existsFormula(TypedIdentifier[] vars, Formula formula) Bind variables in formula by existential quantification.
StatJudgement	extendFrame(StatJudgement S, java.util.Set<VariableSymbol> vars) Extend judgement to the denoted set of modifiable variables.
static Formula	forallFormula(TypedIdentifier[] vars, Formula formula) Bind variables in formula by universal quantification.
ExpressionLogic	getExpressionLogic() Get expression translator of this judgement processor
StateType	getStateType() Get the state type of this judgement processor
Type	getStringType() Get the string type of this judgement processor
static Formula	ifThenElseFormula(Formula formula0, Formula formula1, Formula formula2) Combine formulas by conditional selection.
static Formula	impliesFormula(Formula formula1, Formula formula2) Combine formulas by implication.
static Formula	notFormula(Formula formula) Negate formula.
static Formula	orFormula(Formula formula1, Formula formula2) Combine formulas by disjunction.
static PostVariable	postVariable(Name name) Construct a post-variable.
static PreVariable	preVariable(Name name) Construct a pre-variable.
static Reference	reference(Identifier ident) Construct a reference from an identifier setting also its type.
StateLiteral	stateLiteral(boolean old) Construct a state literal giving it the current state type.
StateMessage	stateMessage(Term state) Construct a state message term.
StateValue	stateValue(Term state) Construct a state value term.

Methods inherited from class java.lang.Object

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

Constructor Detail

Satisfies

public Satisfies(ParamSymbol method,
                 StateType stype,
                 TaskFolder invariants,
                 java.util.Vector<TheorySymbol> theories,
                 Declaration[][] decls,
                 ErrorStream out)

Create a judgement processor.

Parameters:

method - the method in which the judged commands arise.

stype - the type of the state for the context of a command.

invariants - the folder to which to add invariant tasks.

theories - the referenced theories (first is base theory)

decls - a sequence of declaration lists.

out - the stream to which to write error messages.

Method Detail

getStateType

public StateType getStateType()

Get the state type of this judgement processor

Returns:

the state type.

getStringType

public Type getStringType()

Get the string type of this judgement processor

Returns:

the string type.

getExpressionLogic

public ExpressionLogic getExpressionLogic()

Get expression translator of this judgement processor

Returns:

the expression translator

extendFrame

public StatJudgement extendFrame(StatJudgement S,
                                 java.util.Set<VariableSymbol> vars)

Extend judgement to the denoted set of modifiable variables.

Parameters:

S - the judgement.

vars - the set of modifiable variables

Returns:

the extended judgement

derive

public StatJudgement derive(Statement C)

Apply the judgement "se, Is, Vs |- C: F" to compute the specification F of command C 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).

Parameters:

C - the command C

Returns:

the specification F of command C.

reference

public static Reference reference(Identifier ident)

Construct a reference from an identifier setting also its type.

Parameters:

ident - an identifier denoting a value.

Returns:

a reference to the value with the type information attached.

stateLiteral

public StateLiteral stateLiteral(boolean old)

Construct a state literal giving it the current state type.

Parameters:

old - true if it is the old state (the new state, otherwise)

Returns:

the literal with the state type attached.

stateValue

public StateValue stateValue(Term state)

Construct a state value term.

Parameters:

state - the state.

Returns:

the corresponding state value term.

stateMessage

public StateMessage stateMessage(Term state)

Construct a state message term.

Parameters:

state - the state.

Returns:

the corresponding state message term.

preVariable

public static PreVariable preVariable(Name name)

Construct a pre-variable.

Parameters:

name - the name of the variable.

Returns:

the variable.

postVariable

public static PostVariable postVariable(Name name)

Construct a post-variable.

Parameters:

name - the name of the variable.

Returns:

the variable.

forallFormula

public static Formula forallFormula(TypedIdentifier[] vars,
                                    Formula formula)

Bind variables in formula by universal quantification.

Parameters:

vars - the variables.

formula - the formula.

Returns:

the formula with all variables universally quantified.

existsFormula

public static Formula existsFormula(TypedIdentifier[] vars,
                                    Formula formula)

Bind variables in formula by existential quantification.

Parameters:

vars - the variables.

formula - the formula.

Returns:

the formula with all variables existentially quantified.

andFormula

public static Formula andFormula(Formula formula1,
                                 Formula formula2)

Combine formulas by conjunction.

Parameters:

formula1 - the first formula (may be null, representing TRUE).

formula2 - the second formula (may be null, representing TRUE).

Returns:

the conjunction of both formulas (may be null, representing TRUE).

andFormula

public static Formula andFormula(java.util.Vector<Formula> formulas)

Combine formulas by conjunction.

Parameters:

formulas - the formulas (each may be null, representing TRUE).

Returns:

the conjunction of the formulas (may be null, representing TRUE).

impliesFormula

public static Formula impliesFormula(Formula formula1,
                                     Formula formula2)

Combine formulas by implication.

Parameters:

formula1 - the first formula (may be null, representing TRUE).

formula2 - the second formula (may be null, representing TRUE).

Returns:

the conjunction of both formulas (may be null, representing TRUE).

orFormula

public static Formula orFormula(Formula formula1,
                                Formula formula2)

Combine formulas by disjunction.

Parameters:

formula1 - the first formula (may be null, representing FALSE).

formula2 - the second formula (may be null, representing FALSE).

Returns:

the conjunction of both formulas (may be null, representing FALSE).

notFormula

public static Formula notFormula(Formula formula)

Negate formula.

Parameters:

formula - the first formula (may be null, representing TRUE).

Returns:

the negation of the formula (may be null, representing TRUE).

ifThenElseFormula

public static Formula ifThenElseFormula(Formula formula0,
                                        Formula formula1,
                                        Formula formula2)

Combine formulas by conditional selection.

Parameters:

formula0 - the selection formula (may be null, representing TRUE).

formula1 - the first formula (may be null, representing TRUE).

formula2 - the second formula (may be null, representing TRUE).

Returns:

the conjunction of both formulas (may be null, representing TRUE).