fmrisc.ProofNavigator.Proving

Class ProofUtil

java.lang.Object

fmrisc.ProofNavigator.Proving.ProofUtil

public final class ProofUtil
extends java.lang.Object

Proving utilities.

Constructor Summary

Constructors

Constructor and Description
ProofUtil()

Method Summary

Modifier and Type	Method and Description
static Expression	bind(ValueDeclIdentifier ident, Expression value, Expression body) Construct expression that binds ident to value in body.
static java.lang.String	hash(java.lang.String rep, int len) hash string representation of an object to a short word
static Expression	negate(Expression formula) return negated version of formula where negation is drawn innermost (to atomic formulas)
static Formula[]	toFormulaArray(java.util.Vector<Formula> v) converts vector v of Formula objects to Formula array
static ProofState[]	toProofStateArray(java.util.Vector<ProofState> v) converts vector v of ProofState objects to ProofState array

Methods inherited from class java.lang.Object

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

Constructor Detail

ProofUtil

public ProofUtil()

Method Detail

toFormulaArray

public static Formula[] toFormulaArray(java.util.Vector<Formula> v)

converts vector v of Formula objects to Formula array

Parameters:

v - a vector holding Formula objects

Returns:

an array holding these objects

toProofStateArray

public static ProofState[] toProofStateArray(java.util.Vector<ProofState> v)

converts vector v of ProofState objects to ProofState array

Parameters:

v - a vector holding ProofState objects

Returns:

an array holding these objects

hash

public static java.lang.String hash(java.lang.String rep,
                                    int len)

hash string representation of an object to a short word

Parameters:

rep - the string representation of the object

len - the length of the result word

Returns:

a hashed version of rep of length len consisting of letters and decimal digits.

negate

public static Expression negate(Expression formula)

return negated version of formula where negation is drawn innermost (to atomic formulas)

Parameters:

formula - a formula

Returns:

its negated and simplified version

bind

public static Expression bind(ValueDeclIdentifier ident,
                              Expression value,
                              Expression body)

Construct expression that binds ident to value in body.

Parameters:

ident - an identifier potentially referenced in body.

value - the value to bind the identifier to.

body - the body expression.

Returns:

a copy of body with the appropriate binding.