|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Object fmrisc.Proving.ProofUtil
public final class ProofUtil
Proving utilities.
Constructor Summary | |
---|---|
ProofUtil()
|
Method Summary | |
---|---|
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 v)
converts vector v of Formula objects to Formula array |
static ProofState[] |
toProofStateArray(java.util.Vector 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 |
---|
public ProofUtil()
Method Detail |
---|
public static Formula[] toFormulaArray(java.util.Vector v)
v
- a vector holding Formula objects
public static ProofState[] toProofStateArray(java.util.Vector v)
v
- a vector holding ProofState objects
public static java.lang.String hash(java.lang.String rep, int len)
rep
- the string representation of the objectlen
- the length of the result word
public static Expression negate(Expression formula)
formula
- a formula
public static Expression bind(ValueDeclIdentifier ident, Expression value, Expression body)
ident
- an identifier potentially referenced in body.value
- the value to bind the identifier to.body
- the body expression.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |