jpov.structure
Class Method

java.lang.Object
  jpov.structure.TreeObject
      jpov.structure.Method

public class Method

extends TreeObject

This class implements a node tree corresponding to a method.

Author:

L. Burdy

Constructor Summary

Method(IJml2bConfiguration config, IJmlFile fi, JpoInputStream s)
Constructs a method from a loaded .jpo file

Method Summary

void	addGoals(java.util.ArrayList al)
void	freeLemmas()
int	getFirstLine() Returns the firstLine.
Proofs	getLemmas() Returns the lemmas.
java.lang.String	getName()
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	getPmiName() Returns the method pmi name
java.lang.String	getText(int type) Returns the displayed text for this node.
Proofs	getWellDefinednessLemmas()
boolean	isConstructor()
boolean	isStatic()
void	selectAll()
void	setChecked() Sets the node and its children to checked.
void	setUnchecked() Sets the node and its children to unchecked
void	updateStatus()

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

Constructor Detail

Method

public Method(IJml2bConfiguration config,
              IJmlFile fi,
              JpoInputStream s)
       throws java.io.IOException,
              LoadException

Constructs a method from a loaded .jpo file

Parameters:

s - The input stream corresponding to the JPO file

Method Detail

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 name plus the signature of the method

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

getPmiName

public java.lang.String getPmiName()

Returns the method pmi name

Returns:

pmiName

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

getFirstLine

public int getFirstLine()

Returns the firstLine.

Returns:

firstLine

getLemmas

public Proofs getLemmas()

Returns the lemmas.

Returns:

lemmas

getWellDefinednessLemmas

public Proofs getWellDefinednessLemmas()

isConstructor

public boolean isConstructor()

Returns:

isStatic

public boolean isStatic()

Returns:

freeLemmas

public void freeLemmas()

getName

public java.lang.String getName()

Returns:

updateStatus

public void updateStatus()

addGoals

public void addGoals(java.util.ArrayList al)

selectAll

public void selectAll()