fmrisc.ProgramExplorer.Judgements

Class ExpressionLogic

java.lang.Object

fmrisc.ProgramExplorer.Judgements.ExpressionLogic

public final class ExpressionLogic
extends java.lang.Object

Field Summary

Fields

Modifier and Type	Field and Description
static boolean	baseFunctions

Constructor Summary

Constructors

Constructor and Description
ExpressionLogic(TheorySymbol baseTheory) Create judgement processor.

Method Summary

Modifier and Type	Method and Description
static BooleanLiteral	booleanFormula(boolean value) Convert boolean to truth formula.
static Term	booleanTerm(boolean value) Convert boolean to constant term.
Formula	deriveFormula(ValueExpression exp, java.util.Vector<Formula> pre) Translate a program expression to an equivalent logic formula.
Selector[]	deriveSelector(Term base, Selector sel, java.util.Vector<Formula> pre) Convert program selector to one or two logic selectors.
Term	deriveTerm(ValueExpression exp, java.util.Vector<Formula> pre) Translate a program expression to an equivalent logic term.
static IntLiteral	intLiteral(java.lang.String digits) Construct integer literal.
Formula	notNullFormula(Term term) Create formula that term of object/array type is not null.
static Formula	notNullFormula(Term term, Type booleanType) Create formula that term of object/array type is not null.
Formula	nullFormula(Term term) Create formula that term of object/array type is null.
static Formula	nullFormula(Term term, Type booleanType) Create formula that term of object/array type is null.

Methods inherited from class java.lang.Object

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

Field Detail

baseFunctions

public static boolean baseFunctions

Constructor Detail

ExpressionLogic

public ExpressionLogic(TheorySymbol baseTheory)

Create judgement processor.

Parameters:

baseTheory - the base theory

Method Detail

deriveTerm

public Term deriveTerm(ValueExpression exp,
                       java.util.Vector<Formula> pre)

Translate a program expression to an equivalent logic term.

Parameters:

exp - the program expression.

pre - the vector to which to add preconditions (may be null)

Returns:

the equivalent logic term.

deriveFormula

public Formula deriveFormula(ValueExpression exp,
                             java.util.Vector<Formula> pre)

Translate a program expression to an equivalent logic formula.

Parameters:

exp - the program expression.

pre - the vector to which to add preconditions (may be null)

Returns:

the equivalent logic formula.

deriveSelector

public Selector[] deriveSelector(Term base,
                                 Selector sel,
                                 java.util.Vector<Formula> pre)

Convert program selector to one or two logic selectors.

Parameters:

base - the logic form of the base expression.

sel - the program selector.

pre - the vector to which to add preconditions (may be null)

Returns:

the corresponding logic selectors (null, if none, i.e. selector can be dropped)

booleanTerm

public static Term booleanTerm(boolean value)

Convert boolean to constant term.

Parameters:

value - a boolean value.

Returns:

the corresponding constant term.

booleanFormula

public static BooleanLiteral booleanFormula(boolean value)

Convert boolean to truth formula.

Parameters:

value - a boolean value.

Returns:

the corresponding truth formula.

intLiteral

public static IntLiteral intLiteral(java.lang.String digits)

Construct integer literal.

Parameters:

digits - the digits of the literal.

Returns:

the literal.

nullFormula

public Formula nullFormula(Term term)

Create formula that term of object/array type is null.

Parameters:

term - the term.

Returns:

the formula.

notNullFormula

public Formula notNullFormula(Term term)

Create formula that term of object/array type is not null.

Parameters:

term - the term.

Returns:

the formula.

nullFormula

public static Formula nullFormula(Term term,
                                  Type booleanType)

Create formula that term of object/array type is null.

Parameters:

term - the term.

booleanType - the boolean type to be used.

Returns:

the formula.

notNullFormula

public static Formula notNullFormula(Term term,
                                     Type booleanType)

Create formula that term of object/array type is not null.

Parameters:

term - the term.

booleanType - the boolean type to be used.

Returns:

the formula.