Pandora
Class Justification

java.lang.Object
  Pandora.Justification

All Implemented Interfaces:

java.io.Serializable

public class Justification
extends java.lang.Object
implements java.io.Serializable

Implements the Justification for a line in a proof.

See Also:

Serialized Form

Constructor Summary

Justification(java.lang.String type)
Constructs a Justification.

Justification(java.lang.String type, java.util.List<ProofLine> input)
Constructs a Justification.

Method Summary

java.lang.String	display() Returns a String which can be used to display the Justification in the Proofline.
java.util.List<ProofLine>	getExtraLines() Returns the extra lines contained in the justification.
java.util.List<ProofLine>	getLines() Returns the lines contained in the Justification.
java.lang.String	getSymbol() Returns the String representing the type of the Justification.
void	setExtraLines(java.util.List<ProofLine> extraLines) Sets the extra lines of the justification.
void	setLines(java.util.List<ProofLine> lines) Sets the lines of the justification

Methods inherited from class java.lang.Object

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

Constructor Detail

Justification

public Justification(java.lang.String type)

Constructs a Justification.
Used to construct justifications that do not require line references.
e.g. given, goal, ass.

Parameters:

type - Uses Types class to create a Justification of the given type

Justification

public Justification(java.lang.String type,
                     java.util.List<ProofLine> input)

Constructs a Justification.
Used to contruct justifications that require line references.
e.g. ->E(1,4).

Parameters:

type - Uses Types class to create a Justification of the given type

input - A list of lines that are used in the Justification

Method Detail

display

public java.lang.String display()

Returns a String which can be used to display the Justification in the Proofline.

getSymbol

public java.lang.String getSymbol()

Returns the String representing the type of the Justification.
The String will be of type Types.

getLines

public java.util.List<ProofLine> getLines()

Returns the lines contained in the Justification.

setLines

public void setLines(java.util.List<ProofLine> lines)

Sets the lines of the justification

getExtraLines

public java.util.List<ProofLine> getExtraLines()

Returns the extra lines contained in the justification.
Used in Raptor.

setExtraLines

public void setExtraLines(java.util.List<ProofLine> extraLines)

Sets the extra lines of the justification.
Used in Raptor.