fmrisc.Proving
Class Formula

java.lang.Object
  fmrisc.Proving.Formula

public final class Formula
extends java.lang.Object

A formula occuring in a proof state.

Constructor Summary

Formula(ProofState state, Expression formula, boolean isGoal)
construct a formula from an expression

Formula(ProofState state, Formula formula)
construct a copy of the given formula in the denoted state

Method Summary

Expression	getExpression() Get formula expression.
java.lang.String	getLabel() get formula label
ProofState	getState() Get proof state of formula.
boolean	isGoal() get formula isGoal
void	print(java.io.PrintWriter out) print formula on output stream as "[label] formula"
void	setExpression(Expression formula) Set formula expression.
static Formula[]	toArray(java.util.Vector v) converts vector v of Formula objects to array

Methods inherited from class java.lang.Object

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

Constructor Detail

Formula

public Formula(ProofState state,
               Expression formula,
               boolean isGoal)

construct a formula from an expression

Parameters:

state - the proof state in which the formula occurs

formula - the expression representing the formula

isGoal - true if formula is a goal, false, if it is an assumption.

Formula

public Formula(ProofState state,
               Formula formula)

construct a copy of the given formula in the denoted state

Parameters:

state - the proof state in which the new formula occurs

formula - a given formula

Method Detail

getState

public ProofState getState()

Get proof state of formula.

Returns:

the proof state to which the formula belongs.

getExpression

public Expression getExpression()

Get formula expression.

Returns:

the expression of the formula

setExpression

public void setExpression(Expression formula)

Set formula expression.

Parameters:

formula - the formula expression

getLabel

public java.lang.String getLabel()

get formula label

Returns:

a label by which the formula can be uniquely referenced within the current proof state

isGoal

public boolean isGoal()

get formula isGoal

Returns:

false if formula is assumption, true if it is goal

print

public void print(java.io.PrintWriter out)

print formula on output stream as "[label] formula"

Parameters:

out - the stream on which to print the formula

toArray

public static Formula[] toArray(java.util.Vector v)

converts vector v of Formula objects to array

Parameters:

v - a vector holding Formula objects

Returns:

an array holding these objects