jpov.structure
Class JmlFile

java.lang.Object
  jpov.structure.TreeObject
      jpov.structure.JmlFile

All Implemented Interfaces:

IJmlFile

public class JmlFile

extends TreeObject

implements IJmlFile

This class implements the root node of the tree.

Author:

L. Burdy

Method Summary

boolean	dependsContains(java.lang.String element)
void	finalizeLoad()
void	freeLemmas()
Class[]	getClasses() Returns the array of classes.
java.lang.String[]	getDepends()
java.io.File	getFileName() Returns the currently displayed file
java.util.List	getGoals()
java.io.File	getJpoFile()
java.lang.String[]	getLangNames()
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.
static JmlFile	loadJmlFile(IJml2bConfiguration config, java.io.File jpoFile, JpoInputStream s) Loads the root node from a .jpo file
void	save(IJml2bConfiguration config, JpoOutputStream s) Saves the JML file into a .jpo file
void	selectAll()
void	setChecked() Sets the node and its children to checked.
void	setUnchecked() Sets the node and its children to unchecked
void	unprove() Sets all the goals of this JML file to unprove.
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

Method Detail

loadJmlFile

public static JmlFile loadJmlFile(IJml2bConfiguration config,
                                  java.io.File jpoFile,
                                  JpoInputStream s)
                           throws java.io.IOException,
                                  LoadException

Loads the root node from a .jpo file

Parameters:

s - The input stream corresponding to the JPO file

Returns:

The constructed root node.

Throws:

LoadException - when the file format is not correct.

java.io.IOException

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

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

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

updateStatus

public void updateStatus()

save

public void save(IJml2bConfiguration config,
                 JpoOutputStream s)
          throws java.io.IOException

Saves the JML file into a .jpo file

Parameters:

s - The output stream representing the jpo file

Throws:

java.io.IOException

unprove

public void unprove()

Sets all the goals of this JML file to unprove.

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 file name

getFileName

public java.io.File getFileName()

Returns the currently displayed file

Returns:

fileName

getClasses

public Class[] getClasses()

Returns the array of classes.

Returns:

classes

getLangNames

public java.lang.String[] getLangNames()

Specified by:

getLangNames in interface IJmlFile

Returns:

freeLemmas

public void freeLemmas()

getJpoFile

public java.io.File getJpoFile()

Returns:

getDepends

public java.lang.String[] getDepends()

Returns:

dependsContains

public boolean dependsContains(java.lang.String element)

Parameters:

element -

Returns:

getGoals

public java.util.List getGoals()

finalizeLoad

public void finalizeLoad()

selectAll

public void selectAll()