jpov
Class PartialJpoFile

java.lang.Object
  jpov.PartialJpoFile

public class PartialJpoFile

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

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

Method Summary

static PartialJpoFile	getJpo(org.eclipse.jdt.core.ICompilationUnit c)
java.lang.String	getName()
PartialJmlFile	getPartialJmlFile() Returns the associated JML file

Methods inherited from class java.lang.Object

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

Constructor Detail

PartialJpoFile

public PartialJpoFile(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

getJpo

public static PartialJpoFile getJpo(org.eclipse.jdt.core.ICompilationUnit c)

getPartialJmlFile

public PartialJmlFile getPartialJmlFile()

Returns the associated JML file

Returns:

jmlfile

getName

public java.lang.String getName()

Returns: