Uses of Interface
fmrisc.ProgramExplorer.Syntax.Logic.Formula

Packages that use Formula

Package	Description
fmrisc.ProgramExplorer.InOut
fmrisc.ProgramExplorer.Judgements
fmrisc.ProgramExplorer.Parser
fmrisc.ProgramExplorer.Proving
fmrisc.ProgramExplorer.Semantics
fmrisc.ProgramExplorer.SWT
fmrisc.ProgramExplorer.Syntax.Logic
fmrisc.ProgramExplorer.Syntax.Program
fmrisc.ProgramExplorer.Syntax.Spec
fmrisc.ProgramExplorer.Tasks

Uses of Formula in fmrisc.ProgramExplorer.InOut

Methods in fmrisc.ProgramExplorer.InOut with parameters of type Formula

Modifier and Type	Method and Description
void	PrettyMathML.appendFormula(org.w3c.dom.Node parent, Formula formula) Convert formula to DOM representation of HTML/MathML markup.
static Breaks.Info	Breaks.compute(Formula formula, boolean mathml) Construct the line break information for the denoted formula.
static VirtualDirectory	Presenter.present(Formula formula, int fontSize, int width) Present formula in a certain font size.
static VirtualDirectory	Presenter.present(ParamSymbol symbol, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, int fontSize, int width, int port) Present method in a certain font size.
static void	PrettyPrinter.print(Formula formula, int width, java.io.PrintWriter out) Print formula.

Method parameters in fmrisc.ProgramExplorer.InOut with type arguments of type Formula

Modifier and Type	Method and Description
static VirtualDirectory	Presenter.present(ParamSymbol symbol, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, int fontSize, int width, int port) Present method in a certain font size.
static VirtualDirectory	Presenter.present(ParamSymbol symbol, Statement statement, Formula formula, boolean pre, java.util.Map<Statement,Formula> preMap, java.util.Map<Statement,Formula> postMap, int fontSize, int width, int port) Present method in a certain font size.

Uses of Formula in fmrisc.ProgramExplorer.Judgements

Fields in fmrisc.ProgramExplorer.Judgements declared as Formula

Modifier and Type	Field and Description
Formula	StatJudgement.formula
Formula	StatJudgement.sformula

Methods in fmrisc.ProgramExplorer.Judgements that return Formula

Modifier and Type	Method and Description
static Formula	Satisfies.andFormula(Formula formula1, Formula formula2) Combine formulas by conjunction.
static Formula	Satisfies.andFormula(java.util.Vector<Formula> formulas) Combine formulas by conjunction.
Formula	Pre.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).
Formula	Post.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).
Formula	Terminates.derive(Statement C, ValueSymbol[] J, Formula F) Apply the judgement se, Is, Vs |- C |v J F to prove that command C terminates when executed in a state in which F[J] holds where J is a vector of free variables in F that denotes the measure of the recursive methods in Is that may be called in C (J may be null which indicates that the current method is not recursive).
Formula	ExpressionLogic.deriveFormula(ValueExpression exp, java.util.Vector<Formula> pre) Translate a program expression to an equivalent logic formula.
static Formula	Satisfies.existsFormula(TypedIdentifier[] vars, Formula formula) Bind variables in formula by existential quantification.
static Formula	Satisfies.forallFormula(TypedIdentifier[] vars, Formula formula) Bind variables in formula by universal quantification.
Formula	StatJudgement.getPrecondition() Get the precondition formula.
Formula	StatJudgement.getTermination() Get the termination formula.
static Formula	Satisfies.ifThenElseFormula(Formula formula0, Formula formula1, Formula formula2) Combine formulas by conditional selection.
static Formula	Satisfies.impliesFormula(Formula formula1, Formula formula2) Combine formulas by implication.
static Formula	Satisfies.notFormula(Formula formula) Negate formula.
Formula	ExpressionLogic.notNullFormula(Term term) Create formula that term of object/array type is not null.
static Formula	ExpressionLogic.notNullFormula(Term term, Type booleanType) Create formula that term of object/array type is not null.
Formula	ExpressionLogic.nullFormula(Term term) Create formula that term of object/array type is null.
static Formula	ExpressionLogic.nullFormula(Term term, Type booleanType) Create formula that term of object/array type is null.
static Formula	Satisfies.orFormula(Formula formula1, Formula formula2) Combine formulas by disjunction.
static Formula	Simplification2.perform(Formula formula) Simplify the given formula.
static Formula	Simplification.perform(Formula formula) Simplify the given formula.
static Formula	Normalization.perform(Formula formula) Replace copy of formula with all poststate variables replaced by prestate variables.
static Formula	Normalization.perform(Formula formula, java.util.Collection<VariableSymbol> variables) Replace copy of formula with all poststate variables that do not appear in the set of modifiable variables replaced by prestate variables.
static Formula	Normalization.postCondition(ParamSymbol method) Get normalized postcondition of method (may be null).
static Formula	Normalization.preCondition(ParamSymbol method, boolean init) Get normalized precondition of method (may be null).

Methods in fmrisc.ProgramExplorer.Judgements with parameters of type Formula

Modifier and Type	Method and Description
static Formula	Satisfies.andFormula(Formula formula1, Formula formula2) Combine formulas by conjunction.
static void	Simplification.collect(Simplification.Tag tag, Formula formula, java.util.Collection<Formula> result) Decompose formula into subformulas if it is of denoted formula type.
Formula	Pre.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).
Formula	Post.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).
Formula	Terminates.derive(Statement C, ValueSymbol[] J, Formula F) Apply the judgement se, Is, Vs |- C |v J F to prove that command C terminates when executed in a state in which F[J] holds where J is a vector of free variables in F that denotes the measure of the recursive methods in Is that may be called in C (J may be null which indicates that the current method is not recursive).
static void	Propagator.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.
static Formula	Satisfies.existsFormula(TypedIdentifier[] vars, Formula formula) Bind variables in formula by existential quantification.
static Formula	Satisfies.forallFormula(TypedIdentifier[] vars, Formula formula) Bind variables in formula by universal quantification.
static Formula	Satisfies.ifThenElseFormula(Formula formula0, Formula formula1, Formula formula2) Combine formulas by conditional selection.
static Formula	Satisfies.impliesFormula(Formula formula1, Formula formula2) Combine formulas by implication.
static Formula	Satisfies.notFormula(Formula formula) Negate formula.
static Formula	Satisfies.orFormula(Formula formula1, Formula formula2) Combine formulas by disjunction.
static Formula	Simplification2.perform(Formula formula) Simplify the given formula.
static Formula	Simplification.perform(Formula formula) Simplify the given formula.
static Formula	Normalization.perform(Formula formula) Replace copy of formula with all poststate variables replaced by prestate variables.
static Formula	Normalization.perform(Formula formula, java.util.Collection<VariableSymbol> variables) Replace copy of formula with all poststate variables that do not appear in the set of modifiable variables replaced by prestate variables.
void	StatJudgement.setPrecondition(Formula pre) Get the precondition formula.
void	StatJudgement.setTermination(Formula termination) Set the termination formula.

Method parameters in fmrisc.ProgramExplorer.Judgements with type arguments of type Formula

Modifier and Type	Method and Description
static Formula	Satisfies.andFormula(java.util.Vector<Formula> formulas) Combine formulas by conjunction.
static void	Simplification.collect(Simplification.Tag tag, Formula formula, java.util.Collection<Formula> result) Decompose formula into subformulas if it is of denoted formula type.
Formula	ExpressionLogic.deriveFormula(ValueExpression exp, java.util.Vector<Formula> pre) Translate a program expression to an equivalent logic formula.
Selector[]	ExpressionLogic.deriveSelector(Term base, Selector sel, java.util.Vector<Formula> pre) Convert program selector to one or two logic selectors.
Term	ExpressionLogic.deriveTerm(ValueExpression exp, java.util.Vector<Formula> pre) Translate a program expression to an equivalent logic term.
static void	Propagator.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.
static void	Propagator.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.

Constructors in fmrisc.ProgramExplorer.Judgements with parameters of type Formula

Constructor and Description
StatJudgement(Formula precondition, Formula formula, boolean executes, boolean continues, boolean breaks, boolean returns, java.util.Set<ClassSymbol> exceptions, java.util.Set<VariableSymbol> variables) Construct a command specification.

Uses of Formula in fmrisc.ProgramExplorer.Parser

Methods in fmrisc.ProgramExplorer.Parser that return Formula

Modifier and Type	Method and Description
Formula	SpecLangParser.formula()
Formula	SpecLangParser.formula10()
Formula	SpecLangParser.formula100()
Formula	SpecLangParser.formula20()
Formula	SpecLangParser.formula30()
Formula	SpecLangParser.formula40()
Formula	SpecLangParser.formula50()
Formula	SpecLangParser.formula60()
Formula	SpecLangParser.formula70()
Formula	SpecLangParser.formulaEOF()

Uses of Formula in fmrisc.ProgramExplorer.Proving

Methods in fmrisc.ProgramExplorer.Proving that return Formula

Modifier and Type	Method and Description
Formula	ClassicalProblem.getGoal() Get the goal.

Constructors in fmrisc.ProgramExplorer.Proving with parameters of type Formula

Constructor and Description
ClassicalProblem(Declaration[] decls, Formula goal, ErrorStream out) Construct a proving problem.
StateProblem(Declaration[] decls, Formula goal, java.util.Map<Symbol,Symbol> map, StateType stateType, Type stringType, java.util.Collection<VariableSymbol> variables, java.util.Collection<ClassSymbol> exceptions, ErrorStream out) Construct a proving problem.

Uses of Formula in fmrisc.ProgramExplorer.Semantics

Methods in fmrisc.ProgramExplorer.Semantics that return Formula

Modifier and Type	Method and Description
Formula	FormulaSymbol.getFormula() Get formula.
Formula	ClassSymbol.getInitFormula() Get the formula representing the initial values of the object variables.

Methods in fmrisc.ProgramExplorer.Semantics that return types with arguments of type Formula

Modifier and Type	Method and Description
java.util.Map<Statement,Formula>	ParamSymbol.getPreMap() Get mapping of body statements to prestate knowledge.

Methods in fmrisc.ProgramExplorer.Semantics with parameters of type Formula

Modifier and Type	Method and Description
void	TCCGenerator.assume(Formula formula) Create an assumption.
static AxiomSymbol	AxiomSymbol.construct(Identifier name, Formula formula, AxiomDefinition decl, TheorySymbol theory) Construct axiom symbol.
static FormulaSymbol	FormulaSymbol.construct(Identifier name, Formula formula, FormulaDefinition decl, TheorySymbol theory) Construct formula symbol.
boolean	LogicChecking.process(Formula formula) Type-check formula in current theory.
boolean	LogicChecking.processFormula(Formula formula) Process formula and create type-checking conditions in context set up by setStateContext().
void	TCCGenerator.prove(java.lang.String name, SourcePosition position, Formula formula, StateType resultType, Name[] stateVars, Name[] stateExcs) Create a new task to prove the given formula.
FormulaSymbol	LogicEnvironment.putFormula(Identifier name, Formula formula, FormulaDefinition decl, TheorySymbol theory) Attempts to put formula into value table
void	ClassSymbol.setInitFormula(Formula formula) Set the formula representing the initial values of the object variables.
void	LogicChecking.setStateContext(Formula pre, StateType type, Name[] vars, Name[] excs, TaskFolder folder) Set the current program state context.

Method parameters in fmrisc.ProgramExplorer.Semantics with type arguments of type Formula

Modifier and Type	Method and Description
void	ParamSymbol.setPreMap(java.util.Map<Statement,Formula> preMap) Set mapping of body statements to prestate knowledge.

Uses of Formula in fmrisc.ProgramExplorer.SWT

Methods in fmrisc.ProgramExplorer.SWT with parameters of type Formula

Modifier and Type	Method and Description
void	TopWindow.propagateCondition(ParamSymbol method, Statement statement, Formula formula, boolean pre) Propagate condition through method body.

Uses of Formula in fmrisc.ProgramExplorer.Syntax.Logic

Subinterfaces of Formula in fmrisc.ProgramExplorer.Syntax.Logic

Modifier and Type	Interface and Description
interface	ProgramVariable Interface to any expression denoting a storage location.

Classes in fmrisc.ProgramExplorer.Syntax.Logic that implement Formula

Modifier and Type	Class and Description
class	AndFormula A logical conjunction.
class	AtomicFormula An atomic formula.
class	BinaryAtomicFormula Base class of atomic formulas with binary operators.
class	BinaryFormula Base class of binary formulas.
class	BooleanLiteral A logical (i.e.
class	EqualsFormula An equality.
class	EquivalentFormula A logical equivalence.
class	ExistsFormula An existentially quantified formula.
class	False A literal denoting the boolean value "false".
class	ForallFormula A universally quantified formula.
class	FormulaBase Base class of a logical formula.
class	GreaterEqualFormula An is-greater-than-or-equal formula.
class	GreaterFormula An is-greater-than formula.
class	IfThenElseFormula Base class of a conditional formula.
class	ImpliesFormula A logical implication.
class	LessEqualFormula An is-less-than-or-equal formula.
class	LessFormula An is-less-than formula.
class	LetFormula A formula with local value definitions.
class	NotEqualsFormula An equality.
class	NotEquivalentFormula An exclusive disjunction.
class	NotFormula A logical negation.
class	OrFormula A logical disjunction.
class	PostfixFormula A postfix application of a predicate.
class	PostVariable A reference to a program variable in the post-state.
class	PreVariable A reference to a program variable in the pre-state.
class	ProgramVariableBase Base class of a reference to a program variable.
class	QuantifiedFormula Base class of quantified formulas.
class	ReadsOnlyFormula A formula that states that no program variable may change.
class	Reference A reference to a logical variable (or constant).
class	SelectionTerm A term from which a component is selected.
class	SimilarFormula A state similarity (equality up to result value).
class	StateBreaks The statement that a state is "breaking".
class	StateContinues The statement that a state is "continuing".
class	StateExecutes The statement that a state is "executing".
class	StateReturns The statement that a state is "returning".
class	StateThrows The statement that a state is "throwing".
class	StateThrowsException The statement that a state throws a particular exception.
class	StateValue A reference to the return value captured by the current state.
class	True A literal denoting the boolean value "true".
class	UnaryFormula Base class of unary formulas.
class	WritesOnlyFormula A formula that states that only certain program variables may change.

Methods in fmrisc.ProgramExplorer.Syntax.Logic that return Formula

Modifier and Type	Method and Description
Formula	UnaryFormula.getBase() Get base formula.
Formula	LetFormula.getBody() Get body.
Formula	QuantifiedFormula.getBody() Get the body of the formula.
Formula	LambdaFormula.getBody() Get the body of the term.
Formula	IfThenElseExpression.getCondition() Get condition.
Formula	IfThenElseFormula.getElseBranch() Get "else" branch.
Formula	BinaryFormula.getFirst() Get first subformula.
Formula	ValueDeclarationFormula.getFormula() Get value of the declaration.
Formula	BinaryFormula.getSecond() Get second subformula.
Formula	IfThenElseFormula.getThenBranch() Get "then" branch.
Formula	FormulaDefinition.getValue() Get the formula value.

Methods in fmrisc.ProgramExplorer.Syntax.Logic with parameters of type Formula

Modifier and Type	Method and Description
static NotFormula	NotFormula.construct(Formula base) Construct a logical negation.
static NotEquivalentFormula	NotEquivalentFormula.construct(Formula first, Formula second) Construct an exclusive disjunction.
static AndFormula	AndFormula.construct(Formula first, Formula second) Construct a conjunction.
static OrFormula	OrFormula.construct(Formula first, Formula second) Construct a disjunction.
static EquivalentFormula	EquivalentFormula.construct(Formula first, Formula second) Construct an equivalence.
static ImpliesFormula	ImpliesFormula.construct(Formula first, Formula second) Construct an implication.
static IfThenElseFormula	IfThenElseFormula.construct(Formula cond, Formula tbranch, Formula ebranch) Construct a conditional formula.
static IfThenElseTerm	IfThenElseTerm.construct(Formula cond, Term tbranch, Term ebranch) Construct a conditional term.
static FormulaDefinition	FormulaDefinition.construct(Identifier name, Formula formula) Create new declaration of a constant denoting a formula.
static AxiomDefinition	AxiomDefinition.construct(Identifier name, Formula formula) Create new declaration of a constant denoting a axiom.
static ValueDeclarationFormula	ValueDeclarationFormula.construct(Identifier name, Type type, Formula value) Create new declaration of a constant denoting a predicate.
static ExistsFormula	ExistsFormula.construct(TypedIdentifier[] vars, Formula body) Construct an existentially quantified formula.
static LambdaFormula	LambdaFormula.construct(TypedIdentifier[] vars, Formula body) Construct a function expression with a formula body.
static ForallFormula	ForallFormula.construct(TypedIdentifier[] vars, Formula body) Construct a universally quantified formula.
static LetFormula	LetFormula.construct(ValueDefinition[] d, Formula b) Construct formula with local value definitions.

Uses of Formula in fmrisc.ProgramExplorer.Syntax.Program

Methods in fmrisc.ProgramExplorer.Syntax.Program that return Formula

Modifier and Type	Method and Description
Formula	ForLoopStatement.getPrecondition() Get for-loop precondition.

Methods in fmrisc.ProgramExplorer.Syntax.Program with parameters of type Formula

Modifier and Type	Method and Description
void	ForLoopStatement.setPrecondition(Formula pre) Set for-loop precondition.

Uses of Formula in fmrisc.ProgramExplorer.Syntax.Spec

Methods in fmrisc.ProgramExplorer.Syntax.Spec that return Formula

Modifier and Type	Method and Description
Formula	StatementSpec.getAssertion() Get pre-state assertion.
Formula	ClassSpec.getClassInvariant() Get class invariant.
Formula	MethodSpec.getDivergesCondition() Get method diverges condition.
Formula	LoopSpec.getLoopInvariant() Get loop invariant.
Formula	MethodSpec.getPostCondition() Get method postcondition.
Formula	MethodSpec.getPreCondition() Get method precondition.

Methods in fmrisc.ProgramExplorer.Syntax.Spec with parameters of type Formula

Modifier and Type	Method and Description
void	StatementSpec.setAssertion(Formula ass) Set pre-state assertion
void	ClassSpec.setClassInvariant(Formula inv) Set class invariant.
void	MethodSpec.setDivergesCondition(Formula div) Set diverges condition.
void	LoopSpec.setLoopInvariant(Formula inv) Set loop invariant.
void	MethodSpec.setPostCondition(Formula post) Set postcondition.
void	MethodSpec.setPreCondition(Formula pre) Set precondition.

Uses of Formula in fmrisc.ProgramExplorer.Tasks

Fields in fmrisc.ProgramExplorer.Tasks declared as Formula

Modifier and Type	Field and Description
Formula	FlattenDeclarations.Result.goal

Methods in fmrisc.ProgramExplorer.Tasks with parameters of type Formula

Modifier and Type	Method and Description
static FlattenDeclarations.Result	FlattenDeclarations.flatten(java.util.Vector<TheorySymbol> theories, Declaration[][] decls, Formula goal, TheorySymbol theory) Flatten a task with nested declarations.

Method parameters in fmrisc.ProgramExplorer.Tasks with type arguments of type Formula

Modifier and Type	Method and Description
static void	PreconditionTasks.generate(ParamSymbol method, java.util.Map<Statement,Formula> preMap, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct the precondition tasks for a given method.

Constructors in fmrisc.ProgramExplorer.Tasks with parameters of type Formula

Constructor and Description
InvariantTask(ParamSymbol method, Statement stat, Formula goal, Formula invariant, SourcePosition pos, Formula cond, Formula body, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct an invariant verification task.
Result(Declaration[] decls, Formula goal, java.util.Map<Symbol,Symbol> map)
TerminationTask(java.lang.String kind, ParamSymbol method, Formula goal, Statement stat, java.lang.String tag, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct a termination verification task.
TypeCheckingTask(TheorySymbol tsymbol, java.lang.String name, SourcePosition position, java.io.File dir, StateType resultType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, Formula goal, ErrorStream out) Create task of proving a type-checking condition.