jpov.structure
Class Lemma

java.lang.Object
  jpov.structure.TreeObject
      jpov.structure.Lemma

public class Lemma

extends TreeObject

This class implements a node tree corresponding to a case.

Author:

L. Burdy

Method Summary

void	addGoals(java.util.ArrayList al)
java.lang.String	getCaseNum() Returns the case number into its englobing method.
Box[]	getFlow() Returns the array of boxes.
Goal[]	getGoals() Returns the array of goals
VirtualFormula[]	getHyp() Returns the array of hypothesis.
java.lang.String	getName() Returns the name of the method to which this case belongs.
int	getNbCheckedPo()
int	getNbPo() Returns the number of proof obligations for this node.
int	getNbPoProved() Returns the number of proved proof obligations for this node.
int	getNbPoProved(java.lang.String prover) Returns the number of proved proof obligations for this node.
int	getNum()
java.lang.String	getText(int type) Returns the displayed text for this node.
void	selectAll()
void	setChecked() Sets the node and its children to checked.
void	setText(java.lang.String parent)
void	setUnchecked() Sets the node and its children to unchecked

Methods inherited from class jpov.structure.TreeObject

getParent, isChecked, isProved, percentProved

Methods inherited from class java.lang.Object

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

Method Detail

setChecked

public void setChecked()

Description copied from class: TreeObject

Sets the node and its children to checked.

Specified by:

setChecked in class TreeObject

setUnchecked

public void setUnchecked()

Description copied from class: TreeObject

Sets the node and its children to unchecked

Specified by:

setUnchecked in class TreeObject

getNbPo

public int getNbPo()

Description copied from class: TreeObject

Returns the number of proof obligations for this node.

Specified by:

getNbPo in class TreeObject

Returns:

the number of proof obligations for this node

getNbPoProved

public int getNbPoProved()

Description copied from class: TreeObject

Returns the number of proved proof obligations for this node.

Specified by:

getNbPoProved in class TreeObject

Returns:

the number of proved proof obligations for this node

getNbPoProved

public int getNbPoProved(java.lang.String prover)

Description copied from class: TreeObject

Returns the number of proved proof obligations for this node.

Specified by:

getNbPoProved in class TreeObject

Returns:

the number of proved proof obligations for this node

getNbCheckedPo

public int getNbCheckedPo()

getText

public java.lang.String getText(int type)

Description copied from class: TreeObject

Returns the displayed text for this node.

Specified by:

getText in class TreeObject

Returns:

Case xx

getCaseNum

public java.lang.String getCaseNum()

Returns the case number into its englobing method.

Returns:

caseNum

getGoals

public Goal[] getGoals()

Returns the array of goals

Returns:

goals

getName

public java.lang.String getName()

Returns the name of the method to which this case belongs.

Returns:

name

getFlow

public Box[] getFlow()

Returns the array of boxes.

Returns:

flow

getHyp

public VirtualFormula[] getHyp()

Returns the array of hypothesis.

Returns:

hyp

setText

public void setText(java.lang.String parent)

getNum

public int getNum()

Returns:

addGoals

public void addGoals(java.util.ArrayList al)

selectAll

public void selectAll()