jpov.structure
Class Proofs

java.lang.Object
  jpov.structure.TreeObject
      jpov.structure.Proofs

Direct Known Subclasses:

StaticInitProofs, WellDefinedMethodProofs, WellDefInvProofs

public class Proofs

extends TreeObject

This class implements a node in the tree corresponding to the static initialization. For the methods, it does not correspond to a node, it is overpassed to display lemmas. Nevertheless it contains the array of hypothesis that are cited in the methods lemmas

Author:

L. Burdy

Method Summary

void	addGoals(java.util.ArrayList al)
Lemma[]	getLemmas() Return the lemmas array
java.lang.Object[]	getLemmasWithPo(int type) Returns an array containing lemmas with almost one goal
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.
java.lang.String	getText(int type) Returns the displayed text for this node.
void	setChecked() Sets the node and its children to checked.
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

getLemmasWithPo

public java.lang.Object[] getLemmasWithPo(int type)

Returns an array containing lemmas with almost one goal

Returns:

a subarray of the lemmas array

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:

the displayed text for this node.

getLemmas

public Lemma[] getLemmas()

Return the lemmas array

Returns:

lemmas

addGoals

public void addGoals(java.util.ArrayList al)