jml2b.structure.java
Class Class

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem
          jml2b.structure.java.NamedNode
              jml2b.structure.java.AClass
                  jml2b.structure.java.Class

All Implemented Interfaces:

jml.JmlDeclParserTokenTypes, Linkable, java.io.Serializable, TypeCheckable

public class Class

extends AClass

implements Linkable, java.io.Serializable, TypeCheckable

Internal representation of classes.

Author:

A. Requet, L. Burdy.

See Also:

Serialized Form

Field Summary

java.util.Vector	constructors Constructors defined by the current class.
java.util.Vector	fields Fields defined by the class.
java.util.Vector	methods Methods defined by the current class.
java.util.Vector	staticFinalFieldInvariants Static final fields declaration of the class.
Proofs	staticInitLemmas
java.util.Vector	staticInvariants Static invariants of the class.
Proofs	wellDefInvLemmas

Fields inherited from class jml2b.structure.java.NamedNode

garbage, nameIndex

Fields inherited from interface jml2b.link.Linkable

STATE_LINKED, STATE_LINKED_STATEMENTS, STATE_LINKED_TYPE_CHECKED, STATE_UNLINKED

Fields inherited from interface jml.JmlDeclParserTokenTypes

ABRUPT_BEHAVIOR, ACCESSIBLE, ACCESSIBLE_KEYWORD, ACCESSIBLE_REDUNDANTLY, ACCESSIBLE_SEQ, ADDITIVE_ASSIGNMENT_OP, ADDITIVE_OP, AFFIRM_KEYWORD, ALSO, AND, ARRAY_DECLARATOR, ASGNABLE_SEQ, ASSERT, ASSERT_REDUNDANTLY, ASSIGN, ASSIGNABLE, ASSIGNABLE_KEYWORD, ASSIGNABLE_REDUNDANTLY, ASSUME, ASSUME_KEYWORD, ASSUME_REDUNDANTLY, AXIOM, BACKWARD_IMPLIES, BADCHAR, BAND, BAND_ASSIGN, BEHAVIOR, BITWISE_ASSIGNMENT_OP, BITWISE_OP, BNOT, BOR, BOR_ASSIGN, BREAKS, BREAKS_KEYWORD, BREAKS_REDUNDANTLY, BREAKS_SEQ, BSR, BSR_ASSIGN, BXOR, BXOR_ASSIGN, CALLABLE, CALLABLE_KEYWORD, CALLABLE_REDUNDANTLY, CALLABLE_SEQ, CASE, CAST, CHAR_LITERAL, CHOOSE, CHOOSE_IF, COLON, COMMA, CONJOINABLE_SPEC, CONSTRAINT, CONSTRAINT_KEYWORD, CONSTRAINT_REDUNDANTLY, CONSTRUCTOR, CONT_SEQ, CONTINUES, CONTINUES_KEYWORD, CONTINUES_REDUNDANTLY, DEC, DECREASES, DECREASES_REDUNDANTLY, DECREASING, DECREASING_KEYWORD, DECREASING_REDUNDANTLY, DEPENDS, DEPENDS_KEYWORD, DEPENDS_REDUNDANTLY, DIM_EXPRS, DIMS, DINFORMALLY, DIV, DIV_ASSIGN, DIV_SEQ, DIVERGES, DIVERGES_KEYWORD, DIVERGES_REDUNDANTLY, DOC_ATSIGN, DOC_ATSIGN_KEYWORD, DOC_AUTHOR, DOC_COMMENT, DOC_COMMENT_START, DOC_DEPRECATED, DOC_EXCEPTION, DOC_JML_SPECS, DOC_NL_WS, DOC_NON_EMPTY_TEXTLINE, DOC_NON_NL_WS, DOC_PARAM, DOC_RETURN, DOC_SEE, DOC_SERIAL, DOC_SERIALDATA, DOC_SERIALFIELD, DOC_SINCE, DOC_THROWS, DOC_UNKNOWN_KEYWORD, DOC_VERSION, DOT, DOT_DOT, ELSE, ENS_SEQ, ENSURES, ENSURES_KEYWORD, ENSURES_REDUNDANTLY, EOF, EQUAL, EQUALITY_OP, EQUIV, EQUIVALENCE_OP, ESC, EXAMPLE, EXCEPTIONAL_BEHAVIOR, EXCEPTIONAL_EXAMPLE, EXPONENT, EXSURES, EXSURES_REDUNDANTLY, EXT_ALSO, EXT_AND, FLOAT_SUFFIX, FOR, FOR_EXAMPLE, FOR_INIT, FOR_TEST, FOR_UPDATER, FORALL, GE, GHOST, GT, HENCE_BY, HENCE_BY_KEYWORD, HENCE_BY_REDUNDANTLY, HEX_DIGIT, IDENT, IGNORED_AT_IN_COMMENT, IMPLICATION_OP, IMPLIES_THAT, INC, INFORMAL_DESCRIPTION, INIT, INITIALIZER, INITIALLY, INSTANCE, INSTANCE_INIT, INVARIANT, INVARIANT_KEYWORD, INVARIANT_REDUNDANTLY, IS_SUBTYPE_OF, JAVA_BUILTIN_TYPE, JAVA_MODIFIER, JML_BACKSLASH_SEQUENCE, JML_MODIFIER, L_ARROW, LABEL, LABEL_KEYWORD, LAND, LBRACK, LCURLY, LCURLY_VBAR, LE, LET, LETOLD_KEYWORD, LIMPLIES, LITERAL_abstract, LITERAL_assert, LITERAL_boolean, LITERAL_break, LITERAL_byte, LITERAL_case, LITERAL_catch, LITERAL_char, LITERAL_class, LITERAL_const, LITERAL_continue, LITERAL_default, LITERAL_do, LITERAL_double, LITERAL_else, LITERAL_extends, LITERAL_false, LITERAL_final, LITERAL_finally, LITERAL_float, LITERAL_for, LITERAL_if, LITERAL_implements, LITERAL_import, LITERAL_instanceof, LITERAL_int, LITERAL_interface, LITERAL_long, LITERAL_native, LITERAL_new, LITERAL_null, LITERAL_package, LITERAL_private, LITERAL_protected, LITERAL_public, LITERAL_return, LITERAL_short, LITERAL_static, LITERAL_strictfp, LITERAL_super, LITERAL_switch, LITERAL_synchronized, LITERAL_this, LITERAL_throw, LITERAL_throws, LITERAL_transient, LITERAL_true, LITERAL_try, LITERAL_void, LITERAL_volatile, LITERAL_while, LNOT, LOGICAL_OP, LOOP_ASGNABLE_SEQ, LOOP_ASSIGNABLE_KEYWORD, LOOP_EXSURES, LOOP_INV_SEQ, LOOP_INVARIANT, LOOP_INVARIANT_REDUNDANTLY, LOOP_MODIFIES, LOOP_SIG_SEQ, LOR, LPAREN, LT, MAINTAINING, MAINTAINING_KEYWORD, MAINTAINING_REDUNDANTLY, MEASURED_BY, MEASURED_BY_KEYWORD, MEASURED_BY_REDUNDANTLY, METH, MINUS, MINUS_ASSIGN, ML_COMMENT, MOD, MOD_ASSIGN, MODEL, MODEL_PROGRAM, MODIFIABLE, MODIFIABLE_REDUNDANTLY, MODIFIER_SET, MODIFIES, MODIFIES_REDUNDANTLY, MONITORED, MONITORED_BY, MULTIPLICATIVE_ASSIGNMENT_OP, MULTIPLICATIVE_OP, NESTED_CLASS, NL_WS, NON_NL_WS, NON_NULL, NORMAL_BEHAVIOR, NORMAL_EXAMPLE, NOT_EQUAL, NOT_EQUIV, NOWARN_LABEL, NOWARN_LABEL_LIST, NULL_TREE_LOOKAHEAD, NUM_FLOAT, NUM_INT, OLD, OR, PARAM, PLUS, PLUS_ASSIGN, POST, POST_DEC, POST_INC, POST_INCREMENT_OP, POST_REDUNDANTLY, PRE, PRE_INCREMENT_OP, PRE_REDUNDANTLY, PRIVACY_MODIFIER, PURE, QUANT_VARS, QUANTIFIED_EXPR, QUANTIFIER_TOKEN, QUESTION, R_ARROW, RBRACK, RCURLY, READABLE_IF, REFINE, RELATIONAL_OP, REPLACE, REPRESENTS, REPRESENTS_KEYWORD, REPRESENTS_REDUNDANTLY, REQUIRES, REQUIRES_KEYWORD, REQUIRES_REDUNDANTLY, RETURNS, RETURNS_KEYWORD, RETURNS_REDUNDANTLY, RETURNS_SEQ, RPAREN, SEMI, SET, SET_COMPR, SHIFT_ASSIGNMENT_OP, SHIFT_OP, SIG_SEQ, SIGNALS, SIGNALS_KEYWORD, SIGNALS_REDUNDANTLY, SL, SL_ASSIGN, SL_COMMENT, SPEC_CASE, SPEC_PROTECTED, SPEC_PUBLIC, SPEC_SL_COMMENT, SPEC_STATEMENT, SR, SR_ASSIGN, STAR, STAR_ASSIGN, STAR_ELEMS, STATIC_INITIALIZER, STRING_LITERAL, SUBCLASSING_CONTRACT, T_ELEMTYPE, T_EVERYTHING, T_EXISTS, T_FIELDS_OF, T_FORALL, T_FRESH, T_INVARIANT_FOR, T_IS_INITIALIZED, T_LBLNEG, T_LBLPOS, T_LOCKSET, T_MAX, T_MIN, T_NONNULLELEMENTS, T_NOT_MODIFIED, T_NOT_SPECIFIED, T_NOTHING, T_NUM_OF, T_OLD, T_OTHER, T_PRODUCT, T_REACH, T_RESULT, T_SUCH_THAT, T_SUM, T_TYPE, T_TYPEOF, T_TYPEOFALLTYPES, UNARY_NUMERIC_OP, UNINITIALIZED, UNREACHABLE, VAR_DECL, VBAR_RCURLY, VF_SEQ, VOCAB, WEAKLY, WHEN, WHEN_KEYWORD, WHEN_REDUNDANTLY, WS

Constructor Summary

Class()

Class(JmlFile jf, antlr.collections.AST tree, Package class_package, Modifiers mods, boolean external)
Creates a new class in package class_package, with the given modifiers.

Class(java.lang.String name, Proofs lemmas, Proofs wellDefInvLemmas, java.util.Vector constructors, java.util.Vector methods)
Creates a new class.

Method Summary

void	addFields(Field fi)
void	addGhost(Field f)
static void	clearAll() Clear all classes that could have been instanciated.
java.lang.String	emit(IJml2bConfiguration config)
boolean	equals(java.lang.String fqn) Return true iff the class "this" is equals to the class denoted by the given fully qualified name.
java.util.Enumeration	getAccessibleDepends()
java.util.Vector	getAccessibleFields()
static Class	getArray(IJml2bConfiguration config) Return the class that is used to represent arrays.
java.util.Enumeration	getConstraints()
AMethod	getConstructor(IJml2bConfiguration config, java.util.Vector param_types) Returns the constructor matching the given parameter types.
Method	getConstructor(Parameters p)
java.util.Enumeration	getConstructors() Returns an enumeration of the constructors defined by this class.
AMethod	getDefaultConstructor() Returns the default constructor for this class, if the class defines one.
java.util.Enumeration	getDepends() Returns an enumeration of the represents clauses defined in this class.
AField	getField(java.lang.String name, AClass from) Gets the field named name if it is visible from the given class.
java.util.Enumeration	getFields() Returns an enumeration of the fields defined by the current class.
java.util.Vector	getFieldsV()
int	getFirstLine()
java.lang.String	getFullyQualifiedName()
Formula	getGlobalMemberInvariant(IJml2bConfiguration config)
SimpleLemma	getGlobalMemberInvariantProof(IJml2bConfiguration config)
java.util.Vector	getGlobalStaticInvariant() Returns the global static invariant.
java.util.Enumeration	getImplements() Returns an enumeration of the implemented interfaces.
java.util.Vector	getInstanceConstraints()
java.util.Enumeration	getInvariants() Returns an enumeration of the invariants defined by this class.
java.util.Enumeration	getMemberInvariants() Returns an enumeration of the member invariants.
AMethod	getMethod(java.lang.String name, Parameters p) Searches for a method with the given name and parameters in the current class.
java.util.Enumeration	getMethods() Returns an enumeration of the methods declared by the current class.
IModifiers	getModifiers() Returns the modifiers associated to the current class.
java.lang.String	getName() Returns the name of the class.
java.util.Vector	getOwnFields() Returns a vector containing all the fields defined by the current class and its super classes.
Package	getPackage() Returns the package this class belongs to.
java.util.Enumeration	getRepresents() Returns an enumeration of the represents clauses defined in this class.
java.util.Vector	getStaticConstraints()
java.util.Enumeration	getStaticFinalFieldsInvariant() Returns an enumeration of the invariants corresponding to static final fields.
Expression	getStaticFinalFieldsInvariants()
Proofs	getStaticInitLemmas()
java.util.Enumeration	getStaticInvariants() Returns an enumeration of the static invariants defined by this class.
Proofs	getWellDefInvLemmas()
boolean	isExternal() Returns true if the current class is an "external" class.
boolean	isInterface()
void	link(IJml2bConfiguration config, LinkContext f) Link the externally visible parts of the class.
int	linkStatements(IJml2bConfiguration config, LinkContext f) Link the parts that cannot be directly referenced from the outside.
AMethod	lookupMethodCurrentClass(IJml2bConfiguration config, java.lang.String mth_name, java.util.Vector param_types, AMethod candidate) Search for a method looking only in the current class (or interface).
void	mergeWith(Class[] classes)
int	nbPo()
int	nbPoProved()
int	nbPoProved(java.lang.String prover)
antlr.collections.AST	parse(JmlFile jmlFile, antlr.collections.AST tree) Initialise the content of the class from the given AST tree.
void	save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) .jpo file
Type	typeCheck(IJml2bConfiguration config, LinkContext f)

Methods inherited from class jml2b.structure.java.AClass

addSuperFields, getField, getSuper, getSuperClass, getSuperDefaultConstructor, implementsInterface, isObject, isSubclassOf, lookupMethod, lookupMethodClass, lookupMethodInterface

Methods inherited from class jml2b.structure.java.NamedNode

clearName, getBName, hasBName, newName

Methods inherited from class jml2b.structure.java.ParsedItem

change, change, getColumn, getJmlFile, getLine, save, setBox

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Field Detail

fields

public java.util.Vector fields

Fields defined by the class. (Vector of JmlFields). Note that Those fields do not include fields defined by the superclass.

See Also:

Field

staticInvariants

public java.util.Vector staticInvariants

Static invariants of the class. (Vector of jml2b.structure.Invariants).

See Also:

Invariant

staticFinalFieldInvariants

public java.util.Vector staticFinalFieldInvariants

Static final fields declaration of the class. (Vector of jml2b.structure.Invariants).

See Also:

Invariant

methods

public java.util.Vector methods

Methods defined by the current class. Vector of Method elements.

See Also:

Method

constructors

public java.util.Vector constructors

Constructors defined by the current class. Vector of Method elements.

See Also:

Method

staticInitLemmas

public transient Proofs staticInitLemmas

wellDefInvLemmas

public transient Proofs wellDefInvLemmas

Constructor Detail

Class

public Class()

Class

public Class(JmlFile jf,
             antlr.collections.AST tree,
             Package class_package,
             Modifiers mods,
             boolean external)

Creates a new class in package class_package, with the given modifiers.

Parameters:

jf - the file that defines the class.

tree - the AST tree corresponding to the class.

class_package - the package this class belongs to.

mods - the modifiers of this class.

external - indicate wether the class correspond to an "external" class, and so if the package/private fields must be ignored

Class

public Class(java.lang.String name,
             Proofs lemmas,
             Proofs wellDefInvLemmas,
             java.util.Vector constructors,
             java.util.Vector methods)

Creates a new class.

Parameters:

name - the name of the class.

lemmas - the lemmas associated to this class.

constructors - vector of Method elements corresponding to the constructors defined by this class.

methods - vector of Method elements corresponding to the methods defined by this class.

See Also:

Method

Method Detail

getDefaultConstructor

public AMethod getDefaultConstructor()

Returns the default constructor for this class, if the class defines one.

Specified by:

getDefaultConstructor in class AClass

Returns:

Method the default constructor or null if the class does not define a default constructor.

isExternal

public boolean isExternal()

Returns true if the current class is an "external" class. An external class is a class that is defined in a different package than the package of the file whose proof obligations are generated.

Returns:

boolean true if the class is an external class, false otherwise.

getPackage

public Package getPackage()

Returns the package this class belongs to.

Specified by:

getPackage in class AClass

Returns:

Package the package this class belongs to.

isInterface

public boolean isInterface()

Specified by:

isInterface in class AClass

getModifiers

public IModifiers getModifiers()

Returns the modifiers associated to the current class.

Specified by:

getModifiers in class AClass

Returns:

Modifiers the modifies associated to the current class.

getName

public java.lang.String getName()

Returns the name of the class.

Specified by:

getName in class AClass

Returns:

the name of the class.

getField

public AField getField(java.lang.String name,
                       AClass from)

Gets the field named name if it is visible from the given class. If the field is not found in the current class, its super classes are searched. Thus the returned field is not guaranted to be declared in the current class.

Specified by:

getField in class AClass

Parameters:

name - the name of the field

from - the class from wich the field should be visible.

Returns:

the field, if it is found, otherwise null.

getFields

public java.util.Enumeration getFields()

Returns an enumeration of the fields defined by the current class. The enumerated elements are of type Field. Note that only the fields defined by the class are returned. Fields defined by a super class of the current class are not returned.

Specified by:

getFields in class AClass

Returns:

Enumeration an enumeration of the fields defined by the current class.

See Also:

Field

getFieldsV

public java.util.Vector getFieldsV()

getOwnFields

public java.util.Vector getOwnFields()

Returns a vector containing all the fields defined by the current class and its super classes. The elements stored in the vector are of type Field

Specified by:

getOwnFields in class AClass

Returns:

Vector a vector containing all the fields defined by the current class and its super classes.

See Also:

Field

getInvariants

public java.util.Enumeration getInvariants()

Returns an enumeration of the invariants defined by this class. The enumerated elements are of type Invariant.

Returns:

Enumeration an enumeration of the invariants.

See Also:

Invariant

getConstraints

public java.util.Enumeration getConstraints()

getStaticInvariants

public java.util.Enumeration getStaticInvariants()

Returns an enumeration of the static invariants defined by this class. The enumerated elements are of type Invariant.

Specified by:

getStaticInvariants in class AClass

Returns:

Enumeration an enumeration of the invariants.

See Also:

Invariant

getRepresents

public java.util.Enumeration getRepresents()

Returns an enumeration of the represents clauses defined in this class. The enumerated elements are of type Represents.

Specified by:

getRepresents in class AClass

Returns:

Enumeration an enumeration of the represents clauses.

See Also:

Represents.

getDepends

public java.util.Enumeration getDepends()

Returns an enumeration of the represents clauses defined in this class. The enumerated elements are of type Depends.

Specified by:

getDepends in class AClass

Returns:

Enumeration an enumeration of the depends clauses.

See Also:

Depends.

getStaticFinalFieldsInvariant

public java.util.Enumeration getStaticFinalFieldsInvariant()

Returns an enumeration of the invariants corresponding to static final fields. The type of the enumerated elements is Invariant.

Specified by:

getStaticFinalFieldsInvariant in class AClass

Returns:

Enumeration an enumeration of the static final invariants.

See Also:

Invariant

getMemberInvariants

public java.util.Enumeration getMemberInvariants()

Returns an enumeration of the member invariants. Member invariants are invariants that refers member variables. The returned enumeration enumerates Invariant elements.

Specified by:

getMemberInvariants in class AClass

Returns:

Enumeration an enumeration of the member invariants.

See Also:

Invariant

getImplements

public java.util.Enumeration getImplements()

Returns an enumeration of the implemented interfaces. The elements returned by the enumeration are of class Type.

Specified by:

getImplements in class AClass

Returns:

Enumeration the implemented interfaces.

getMethods

public java.util.Enumeration getMethods()

Returns an enumeration of the methods declared by the current class. The enumerated elements are of type Method.

Returns:

Enumeration an enumeration of the method declared by the current class.

See Also:

Method

getMethod

public AMethod getMethod(java.lang.String name,
                         Parameters p)

Searches for a method with the given name and parameters in the current class. Note that the method is searched only in the current class, and that the parameters must be the same (a method with same name and compatible parameters will not be returned).

Specified by:

getMethod in class AClass

Parameters:

name - the name of the method

p - the parameters of the method.

Returns:

the method if it is found, null otherwise.

getConstructor

public Method getConstructor(Parameters p)

getConstructors

public java.util.Enumeration getConstructors()

Returns an enumeration of the constructors defined by this class. The enumerated elements are of type Method.

Returns:

Enumeration an enumeration of the constructors.

See Also:

Method

parse

public antlr.collections.AST parse(JmlFile jmlFile,
                                   antlr.collections.AST tree)
                            throws Jml2bException

Initialise the content of the class from the given AST tree. tree must have type modifier_set.

Parameters:

jmlFile - the file that declares the current class.

tree - the AST corresponding to the class declaration.

Returns:

the node next after the class declaration.

Throws:

Jml2bException - in the case where a parse error occur.

link

public void link(IJml2bConfiguration config,
                 LinkContext f)
          throws Jml2bException

Link the externally visible parts of the class.

Specified by:

link in interface Linkable

Parameters:

config - the configuration that should be used.

f - the current link context.

Throws:

Jml2bException

typeCheck

public Type typeCheck(IJml2bConfiguration config,
                      LinkContext f)
               throws Jml2bException

Specified by:

typeCheck in interface TypeCheckable

Throws:

Jml2bException

linkStatements

public int linkStatements(IJml2bConfiguration config,
                          LinkContext f)
                   throws Jml2bException

Link the parts that cannot be directly referenced from the outside. Those parts includes statements, initialisation of fields and method body.

Specified by:

linkStatements in interface Linkable

Parameters:

config - the configuration that should be used

f - the current link context

Throws:

Jml2bException - in the case where identifier cannot be linked

InternalError

lookupMethodCurrentClass

public AMethod lookupMethodCurrentClass(IJml2bConfiguration config,
                                        java.lang.String mth_name,
                                        java.util.Vector param_types,
                                        AMethod candidate)
                                 throws Jml2bException

Search for a method looking only in the current class (or interface).

Specified by:

lookupMethodCurrentClass in class AClass

Parameters:

config - the configuration that should be used.

mth_name - the name of the searched method.

param_types - vector of Type elements containing the signature of the searched method.

candidate - the current best candidate method.

Returns:

the new best candidate method.

Throws:

Jml2bException

getConstructor

public AMethod getConstructor(IJml2bConfiguration config,
                              java.util.Vector param_types)
                       throws Jml2bException

Returns the constructor matching the given parameter types. It use the same lookup parameter matching strategy as the one used for methods

Specified by:

getConstructor in class AClass

Parameters:

config - the configuration that should be used.

param_types - vector of Type elements corresponding to the signature of the constructor.

Returns:

Constructor the searched constructor, null if no such constructor could be found.

Throws:

Jml2bException

getGlobalStaticInvariant

public java.util.Vector getGlobalStaticInvariant()

Returns the global static invariant. That is, the and of all the static invariants visible from this class. This is done by traversing the packages, and adding the content of static invariants that could be seen from this class. This has however the drawback of generating useless invariants (those that are not related to our class). Note that the value returned could be null if no invariants are defined or seen.

getStaticFinalFieldsInvariants

public Expression getStaticFinalFieldsInvariants()

Specified by:

getStaticFinalFieldsInvariants in class AClass

getFullyQualifiedName

public java.lang.String getFullyQualifiedName()

Specified by:

getFullyQualifiedName in class AClass

equals

public boolean equals(java.lang.String fqn)

Return true iff the class "this" is equals to the class denoted by the given fully qualified name.

getGlobalMemberInvariant

public Formula getGlobalMemberInvariant(IJml2bConfiguration config)
                                 throws Jml2bException,
                                        PogException

Throws:

Jml2bException

PogException

getAccessibleDepends

public java.util.Enumeration getAccessibleDepends()

getAccessibleFields

public java.util.Vector getAccessibleFields()

getGlobalMemberInvariantProof

public SimpleLemma getGlobalMemberInvariantProof(IJml2bConfiguration config)
                                          throws Jml2bException,
                                                 PogException

Throws:

Jml2bException

PogException

clearAll

public static void clearAll()

Clear all classes that could have been instanciated. This method is called by Package.clearAll();

getArray

public static Class getArray(IJml2bConfiguration config)
                      throws Jml2bException

Return the class that is used to represent arrays. This class currently does not belong to any package

Throws:

Jml2bException

nbPo

public int nbPo()

nbPoProved

public int nbPoProved(java.lang.String prover)

nbPoProved

public int nbPoProved()

mergeWith

public void mergeWith(Class[] classes)

emit

public java.lang.String emit(IJml2bConfiguration config)

getStaticInitLemmas

public Proofs getStaticInitLemmas()

Returns:

getWellDefInvLemmas

public Proofs getWellDefInvLemmas()

Returns:

addGhost

public void addGhost(Field f)

Parameters:

f -

getFirstLine

public int getFirstLine()

Returns:

addFields

public void addFields(Field fi)

Parameters:

fi -

getStaticConstraints

public java.util.Vector getStaticConstraints()

getInstanceConstraints

public java.util.Vector getInstanceConstraints()

save

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

.jpo file

Throws:

java.io.IOException