Raptor
Class Justification

java.lang.Object
  Raptor.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 pType)
Constructs a Justification.

Justification(java.lang.String pType, java.util.List<ProofLine> pInput)
Constructs a Justification.

Justification(java.lang.String pType, ProgramLine pProg, java.util.List<ProofLine> pInput)
Constructs a Justification.

Justification(java.lang.String pType, ProgramLine pProg, java.util.List<ProofLine> pInput1, java.util.List<ProofLine> pInput2)
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.
ProgramLine	getProgramLine() Returns the program line contained in the justification.
java.lang.String	getSymbol() Returns the String representing the type of the Justification.
void	setExtraLines(java.util.List<ProofLine> pExtraLines) Sets the extra lines of the justification.
void	setLines(java.util.List<ProofLine> pLines) Sets the lines of the justification
java.util.List<ProofLine>	sort(java.util.List<ProofLine> pInput) Used to sort the list of referenced lines by line number and return the sorted list.

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 pType)

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

Parameters:

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

Justification

public Justification(java.lang.String pType,
                     java.util.List<ProofLine> pInput)

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

Parameters:

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

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

Justification

public Justification(java.lang.String pType,
                     ProgramLine pProg,
                     java.util.List<ProofLine> pInput)

Constructs a Justification.
Used to construct justifications that require a program line reference.
e.g. for assg.

Parameters:

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

pProg - the ProgramLine that is used in the justification

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

Justification

public Justification(java.lang.String pType,
                     ProgramLine pProg,
                     java.util.List<ProofLine> pInput1,
                     java.util.List<ProofLine> pInput2)

Constructs a Justification.
Used to construct justifications that require extra line references and a program line reference.
e.g. for semi.

Parameters:

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

pProg - the ProgramLine that is used in the justification

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

pInput2 - 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> pLines)

Sets the lines of the justification

getExtraLines

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

Returns the extra lines contained in the justification.

setExtraLines

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

Sets the extra lines of the justification.

getProgramLine

public ProgramLine getProgramLine()

Returns the program line contained in the justification.

sort

public java.util.List<ProofLine> sort(java.util.List<ProofLine> pInput)

Used to sort the list of referenced lines by line number and return the sorted list.