jpov
Class JpoFile

java.lang.Object
  jpov.JpoFile

public class JpoFile

extends java.lang.Object

This class defines a JPO file. That corresponds to a file and its associated informations stored into a JML file structure.

Author:

L. Burdy

Constructor Summary

JpoFile(IJml2bConfiguration config, java.lang.String name)
Constucts a JPO file from a given repository and a given name.

Method Summary

void	close()
void	finalizeLoad()
java.io.File	getDirectory() Returns the repository
JmlFile	getJmlFile() Returns the associated JML file
java.lang.String	getJpoName() Returns the JPO file name with the extension
java.lang.String	getName() Returns the JPO file name
int	getNumPos() Returns the number of proof obligations.
static JmlFile	loadJmlFile(IJml2bConfiguration configuration, java.lang.String name) Loads a JPO file
void	save() Saves the file into a .jpo file and save the proof status into a .pmi file.
void	unprove() Sets all the lemma to unprove

Methods inherited from class java.lang.Object

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

Constructor Detail

JpoFile

public JpoFile(IJml2bConfiguration config,
               java.lang.String name)
        throws java.io.IOException,
               LoadException

Constucts a JPO file from a given repository and a given name. Loads the file and store the informations into a JML file structure.

Parameters:

name - The file name

Method Detail

loadJmlFile

public static JmlFile loadJmlFile(IJml2bConfiguration configuration,
                                  java.lang.String name)
                           throws java.io.IOException,
                                  LoadException

Loads a JPO file

Parameters:

name - The name of the file without the .jpo extension

Returns:

the constructed JML file structure.

Throws:

java.io.IOException

LoadException

save

public void save()
          throws java.io.IOException

Saves the file into a .jpo file and save the proof status into a .pmi file.

Throws:

java.io.IOException

unprove

public void unprove()

Sets all the lemma to unprove

getNumPos

public int getNumPos()

Returns the number of proof obligations.

Returns:

the number of proof obligations

getJpoName

public java.lang.String getJpoName()

Returns the JPO file name with the extension

Returns:

the JPO file name with the extension

getName

public java.lang.String getName()

Returns the JPO file name

Returns:

mchName

getJmlFile

public JmlFile getJmlFile()

Returns the associated JML file

Returns:

jmlfile

getDirectory

public java.io.File getDirectory()

Returns the repository

Returns:

directory

close

public void close()
           throws java.io.IOException

Throws:

java.io.IOException

finalizeLoad

public void finalizeLoad()