jack.plugin
Class JackJml2bConfiguration

java.lang.Object
  jack.plugin.JackJml2bConfiguration

All Implemented Interfaces:

IJml2bConfiguration

public class JackJml2bConfiguration

extends java.lang.Object

implements IJml2bConfiguration

This class represents a configuration extracted from the Jack plugin and used to compile, edit and prove jml files.

Author:

A. Requet, L. Burdy

Field Summary

static java.lang.String	EVERYTHING
static int	EXSURES_EXCEPTION_FALSE
static int	EXSURES_EXCEPTION_TRUE
static int	EXSURES_OTHER
static int	EXSURES_RUNTIMEEXCEPTION_FALSE
static java.lang.String	NOTHING

Constructor Summary

JackJml2bConfiguration(org.eclipse.core.resources.IProject prj)
Creates a new JackJml2bConfiguration suitable for use with the given project.

Method Summary

Expression	getDefaultEnsures() Returns the default ensures clause
java.util.Vector	getDefaultExsures() Returns the default exsures clause
boolean	getDefaultExternalFile()
static java.lang.String	getDefaultJmlEnsuresText(org.eclipse.core.resources.IProject project) Returns the default ensures clause for jml.
static java.lang.String[]	getDefaultJmlExsuresExceptions(org.eclipse.core.resources.IProject project)
static java.lang.String	getDefaultJmlExsuresOther(org.eclipse.core.resources.IProject project)
static int	getDefaultJmlExsuresType(org.eclipse.core.resources.IProject project) Return the default exsures type for the given project.
static java.lang.String	getDefaultJmlModifies(org.eclipse.core.resources.IProject project) Returns the default modifies clause for jml specifications.
static java.lang.String	getDefaultJmlRequiresText(org.eclipse.core.resources.IProject project) Returns the default requires clause for jml if it is not set to requires true.
ModifiesClause	getDefaultModifies() Returns the default modifies clause
Expression	getDefaultRequires() Returns the default requires clause
JmlPathEntry[]	getJmlPath() Returns the path where files have to be searched
java.io.File	getSubdirectory() Returns the directory where the files have to be read and write.
org.eclipse.swt.graphics.FontData	getViewerFont() Returns the font data to use to display to source code text
static boolean	isDefaultJmlEnsuresTrue(org.eclipse.core.resources.IProject project)
static boolean	isDefaultJmlRequiresTrue(org.eclipse.core.resources.IProject project) Indicate wether the default value for requires clauses is set to requires true or not.
boolean	isFileGenerated(java.lang.String name)
boolean	isObviousPoGenerated() Indicates whether obvious PO have to be generated or not
boolean	isObviousProver(java.lang.String name)
boolean	isViewShown(java.lang.String name) Indicates whether a view of the lemma have to be displayed or not.
boolean	isWellDefPoGenerated()
void	setDefaultExternalFile(boolean b)
static boolean	setDefaultJmlEnsuresText(org.eclipse.core.resources.IProject project, java.lang.String value)
static boolean	setDefaultJmlEnsuresTrue(org.eclipse.core.resources.IProject project, boolean value)
static boolean	setDefaultJmlExsuresExceptions(org.eclipse.core.resources.IProject project, java.lang.String[] exceptions)
static boolean	setDefaultJmlExsuresOther(org.eclipse.core.resources.IProject project, java.lang.String value)
static boolean	setDefaultJmlExsuresType(org.eclipse.core.resources.IProject project, int value)
static boolean	setDefaultJmlModifies(org.eclipse.core.resources.IProject project, java.lang.String value)
static boolean	setDefaultJmlRequiresText(org.eclipse.core.resources.IProject project, java.lang.String value)
static boolean	setDefaultJmlRequiresTrue(org.eclipse.core.resources.IProject project, boolean value)
void	setFileGenerated(java.lang.String name, boolean b)

Methods inherited from class java.lang.Object

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

Field Detail

EXSURES_EXCEPTION_FALSE

public static final int EXSURES_EXCEPTION_FALSE

See Also:

Constant Field Values

EXSURES_EXCEPTION_TRUE

public static final int EXSURES_EXCEPTION_TRUE

See Also:

Constant Field Values

EXSURES_RUNTIMEEXCEPTION_FALSE

public static final int EXSURES_RUNTIMEEXCEPTION_FALSE

See Also:

Constant Field Values

EXSURES_OTHER

public static final int EXSURES_OTHER

See Also:

Constant Field Values

EVERYTHING

public static final java.lang.String EVERYTHING

See Also:

Constant Field Values

NOTHING

public static final java.lang.String NOTHING

See Also:

Constant Field Values

Constructor Detail

JackJml2bConfiguration

public JackJml2bConfiguration(org.eclipse.core.resources.IProject prj)

Creates a new JackJml2bConfiguration suitable for use with the given project.

Parameters:

prj - the project this configuration corresponds to.

Method Detail

getSubdirectory

public java.io.File getSubdirectory()

Description copied from interface: IJml2bConfiguration

Returns the directory where the files have to be read and write. Those files are the jpo file and the generated files.

Specified by:

getSubdirectory in interface IJml2bConfiguration

getJmlPath

public JmlPathEntry[] getJmlPath()

Description copied from interface: IJml2bConfiguration

Returns the path where files have to be searched

Specified by:

getJmlPath in interface IJml2bConfiguration

Returns:

an array of path

getViewerFont

public org.eclipse.swt.graphics.FontData getViewerFont()

Description copied from interface: IJml2bConfiguration

Returns the font data to use to display to source code text

Specified by:

getViewerFont in interface IJml2bConfiguration

isObviousPoGenerated

public boolean isObviousPoGenerated()

Description copied from interface: IJml2bConfiguration

Indicates whether obvious PO have to be generated or not

Specified by:

isObviousPoGenerated in interface IJml2bConfiguration

isWellDefPoGenerated

public boolean isWellDefPoGenerated()

Specified by:

isWellDefPoGenerated in interface IJml2bConfiguration

isFileGenerated

public boolean isFileGenerated(java.lang.String name)

Specified by:

isFileGenerated in interface IJml2bConfiguration

setFileGenerated

public void setFileGenerated(java.lang.String name,
                             boolean b)

Specified by:

setFileGenerated in interface IJml2bConfiguration

isObviousProver

public boolean isObviousProver(java.lang.String name)

Specified by:

isObviousProver in interface IJml2bConfiguration

isViewShown

public boolean isViewShown(java.lang.String name)

Description copied from interface: IJml2bConfiguration

Indicates whether a view of the lemma have to be displayed or not.

Specified by:

isViewShown in interface IJml2bConfiguration

Parameters:

name - The name of the language

getDefaultRequires

public Expression getDefaultRequires()

Description copied from interface: IJml2bConfiguration

Returns the default requires clause

Specified by:

getDefaultRequires in interface IJml2bConfiguration

getDefaultModifies

public ModifiesClause getDefaultModifies()

Description copied from interface: IJml2bConfiguration

Returns the default modifies clause

Specified by:

getDefaultModifies in interface IJml2bConfiguration

getDefaultEnsures

public Expression getDefaultEnsures()

Description copied from interface: IJml2bConfiguration

Returns the default ensures clause

Specified by:

getDefaultEnsures in interface IJml2bConfiguration

getDefaultExsures

public java.util.Vector getDefaultExsures()

Description copied from interface: IJml2bConfiguration

Returns the default exsures clause

Specified by:

getDefaultExsures in interface IJml2bConfiguration

isDefaultJmlRequiresTrue

public static boolean isDefaultJmlRequiresTrue(org.eclipse.core.resources.IProject project)

Indicate wether the default value for requires clauses is set to requires true or not. In the case where it is not set to requires true, then the content of the clause is given by the getDefaultJmlRequiresText method.

Parameters:

project - the project whose property should be returned.

Returns:

boolean true if the default value for requires clauses is true, false if a special value is given.

See Also:

JackPlugin#getDefaultJmlRequiresText(IProject)

setDefaultJmlRequiresTrue

public static boolean setDefaultJmlRequiresTrue(org.eclipse.core.resources.IProject project,
                                                boolean value)

isDefaultJmlEnsuresTrue

public static boolean isDefaultJmlEnsuresTrue(org.eclipse.core.resources.IProject project)

setDefaultJmlEnsuresTrue

public static boolean setDefaultJmlEnsuresTrue(org.eclipse.core.resources.IProject project,
                                               boolean value)

setDefaultJmlRequiresText

public static boolean setDefaultJmlRequiresText(org.eclipse.core.resources.IProject project,
                                                java.lang.String value)

setDefaultJmlEnsuresText

public static boolean setDefaultJmlEnsuresText(org.eclipse.core.resources.IProject project,
                                               java.lang.String value)

setDefaultJmlExsuresExceptions

public static boolean setDefaultJmlExsuresExceptions(org.eclipse.core.resources.IProject project,
                                                     java.lang.String[] exceptions)

Parameters:

project -

exceptions - an array containing the fully qualifed name of the exceptions.

setDefaultJmlModifies

public static boolean setDefaultJmlModifies(org.eclipse.core.resources.IProject project,
                                            java.lang.String value)

getDefaultJmlRequiresText

public static java.lang.String getDefaultJmlRequiresText(org.eclipse.core.resources.IProject project)

Returns the default requires clause for jml if it is not set to requires true.

Parameters:

project - the project whose property should be returned

Returns:

the content of the default requires clause as a string. null if an error occured or if the property is not set.

getDefaultJmlEnsuresText

public static java.lang.String getDefaultJmlEnsuresText(org.eclipse.core.resources.IProject project)

Returns the default ensures clause for jml.

Parameters:

project - the project whose property should be returned

Returns:

the content of the default requires clause as a string. null if an error occured or if the property is not set.

getDefaultJmlExsuresType

public static int getDefaultJmlExsuresType(org.eclipse.core.resources.IProject project)

Return the default exsures type for the given project.

Parameters:

project -

setDefaultJmlExsuresType

public static boolean setDefaultJmlExsuresType(org.eclipse.core.resources.IProject project,
                                               int value)

getDefaultJmlExsuresOther

public static java.lang.String getDefaultJmlExsuresOther(org.eclipse.core.resources.IProject project)

setDefaultJmlExsuresOther

public static boolean setDefaultJmlExsuresOther(org.eclipse.core.resources.IProject project,
                                                java.lang.String value)

getDefaultJmlExsuresExceptions

public static java.lang.String[] getDefaultJmlExsuresExceptions(org.eclipse.core.resources.IProject project)

getDefaultJmlModifies

public static java.lang.String getDefaultJmlModifies(org.eclipse.core.resources.IProject project)

Returns the default modifies clause for jml specifications.

Parameters:

project - the project for which the default is set.

Returns:

String the value for modifies clauses that should be used when no specification is given.

getDefaultExternalFile

public boolean getDefaultExternalFile()

Specified by:

getDefaultExternalFile in interface IJml2bConfiguration

setDefaultExternalFile

public void setDefaultExternalFile(boolean b)

Parameters:

b -