Serialized Form

Package jml2b.pog.util

Class jml2b.pog.util.ColoredInfo extends Profiler implements Serializable

serialVersionUID: -2308775037213438489l

Serialized Fields

index

int index

pi

ParsedItem pi

Parsed item that is colored.

comment

byte comment

comment indice of the item:

• -1 means no color displayed
• 0 means green color
• 1..2 means blue color
• 11..18 means red color
• 21..22 means blue color with associated informations

info

java.lang.String info

Informations associated with comment indices METHOD_CALL or NEW. This information is the specification of called method.

Class jml2b.pog.util.TemporaryField extends Field implements Serializable

serialVersionUID: -9198845858103042990l

Package jml2b.structure.statement

Class jml2b.structure.statement.ArrayInitializer extends Expression implements Serializable

serialVersionUID: 1890926686273759548l

Serialized Fields

listExp

ListExp listExp

The list of expressions. Those expression can be array initializer themseleves when a multi-dimensionnal array is parsed. It can be null if the array has an empty initialization

Class jml2b.structure.statement.BinaryExp extends Expression implements Serializable

serialVersionUID: 2767415478784994988l

Serialized Fields

left

Expression left

The left expression

right

Expression right

The right expression.

Class jml2b.structure.statement.Expression extends Statement implements Serializable

serialVersionUID: -5713906842836394348l

Serialized Fields

nodeType

int nodeType

Token defining the expression operator

nodeText

java.lang.String nodeText

Text corresponding to the expression operator

stateType

Type stateType

Type of the expression

Class jml2b.structure.statement.IsSubtypeOfExp extends Expression implements Serializable

serialVersionUID: -5719671282257637252l

Serialized Fields

subType

Expression subType

The tested subtype.

type

Expression type

The tested super type.

Class jml2b.structure.statement.MethodCallExp extends Expression implements Serializable

serialVersionUID: 7743883423438724253l

Serialized Fields

left

Expression left

The expression corresponding to the called method

right

Expression right

The arguments expression, it can be possibly null when the method is called without arguments.

Class jml2b.structure.statement.QuantifiedExp extends Expression implements Serializable

serialVersionUID: 3537501373084566514l

Serialized Fields

vars

QuantifiedVar vars

The list of quantified variable

body

Expression body

The quantified expression

Class jml2b.structure.statement.QuantifiedVar extends ParsedItem implements Serializable

serialVersionUID: -7810447303875024252l

Serialized Fields

field

Field field

The current quantified field

next

QuantifiedVar next

The next element of the list

Class jml2b.structure.statement.QuestionExp extends Expression implements Serializable

serialVersionUID: -5341421445214593422l

Serialized Fields

cond

Expression cond

The condition

left

Expression left

The value of the expression when the condition is true

right

Expression right

The value of the expression when the condition is false

Class jml2b.structure.statement.StAssert extends Statement implements Serializable

serialVersionUID: -3959347360206595623l

Serialized Fields

exp

Expression exp

The asserted predicate

Class jml2b.structure.statement.Statement extends ParsedItem implements Serializable

serialVersionUID: -5713906842836394348l

Class jml2b.structure.statement.StBlock extends Statement implements Serializable

serialVersionUID: 7877759894682929151l

Serialized Fields

body

Statement body

The encapsulated statement

Class jml2b.structure.statement.StControlFlowBreak extends Statement implements Serializable

serialVersionUID: -193895196844984447l

Serialized Fields

nodeType

int nodeType

The node type can be LITERAL_return, LITERAL_break, LITERAL_continue, LITERAL_throw.

exp

Expression exp

The expression of this statement. It can be the expression returned, the expression thrown or the label for a break or a continue. It can be null except for a throw.

Class jml2b.structure.statement.StDoWhile extends StLoops implements Serializable

serialVersionUID: 4201715476535858046l

Serialized Fields

exp

Expression exp

The conditional expression

Class jml2b.structure.statement.StFor extends StLoops implements Serializable

serialVersionUID: -2170236617582111769l

Serialized Fields

init

Statement init

The initialization statement of the loop

test

Expression test

The test statement of the loop

updater

Statement updater

The updater statement of the loop

Class jml2b.structure.statement.StIf extends Statement implements Serializable

serialVersionUID: 5726202833367464956l

Serialized Fields

cond

Expression cond

The condition

thenTk

Statement thenTk

The statement corresponding to the then branch.

elseTk

Statement elseTk

The statement corresponding to the else branch, if there is no else branh, the statement is initialized with skip

Class jml2b.structure.statement.StImplementsLabel extends Statement implements Serializable

serialVersionUID: 5276356605510345886l

Serialized Fields

labels

java.util.Vector labels

The set of implemented labels

Class jml2b.structure.statement.StLabel extends Statement implements Serializable

serialVersionUID: -4097123075430569195l

Serialized Fields

label

Expression label

The label

body

Statement body

The labeled statement

Class jml2b.structure.statement.StLoops extends Statement implements Serializable

serialVersionUID: -2538988515269093588l

Serialized Fields

nodeType

int nodeType

The node type of the loop. It can be LITERAL_for, LITERAL_do or LITERAL_while

body

Statement body

The body of the loop

loop_invariant

Expression loop_invariant

The loop invariant

loop_variant

Expression loop_variant

The loop variant

loop_modifies

ModifiesClause loop_modifies

The loop modifies clause

loop_exsures

java.util.Vector loop_exsures

The loop exsures clause

line

int line

Class jml2b.structure.statement.StSequence extends Statement implements Serializable

serialVersionUID: 3977087978296856377l

Serialized Fields

left

Statement left

The first statement

right

Statement right

The second statement. It is never null. It can be skip.

Class jml2b.structure.statement.StSkip extends Statement implements Serializable

serialVersionUID: 5018200138214163139l

Class jml2b.structure.statement.StSpecBlock extends Statement implements Serializable

serialVersionUID: 1332238792450955606l

Serialized Fields

sp

SpecCase sp

The JML specification of the block

block

StBlock block

The block statement

startLine

int startLine

endLine

int endLine

Class jml2b.structure.statement.StSwitch extends Statement implements Serializable

serialVersionUID: 2677107039781057404l

Serialized Fields

exp

Expression exp

The tested expression

switchDefault

Statement switchDefault

The default statement. It can not be null. If no default statement is declared, the statement is intialized with skip.

switchCase1

CasesList switchCase1

The list of cases that appear before the default statement. This list is possibly null.

switchCase2

CasesList switchCase2

The list of cases that appear after the default statement. This list is possibly null.

Class jml2b.structure.statement.StTry extends Statement implements Serializable

serialVersionUID: 1158908701372304229l

Serialized Fields

tryTk

Statement tryTk

The try statement

catchTk

CatchList catchTk

The list of catch statements, it can be null.

finallyTk

Statement finallyTk

The finally statement, it can be null.

Class jml2b.structure.statement.StVarDecl extends Statement implements Serializable

serialVersionUID: -5757089589800261606l

Serialized Fields

localVariables

java.util.Vector localVariables

The set of declared Field

Class jml2b.structure.statement.TerminalExp extends Expression implements Serializable

serialVersionUID: -8295372047797723108l

Serialized Fields

ident

Identifier ident

The identifier corresponding to this expression. It can be null if the expression is a constant.

subident

boolean subident

End of an expression created from an identifier and a string. This is used to create expression like c_my_class_an_instance. The part c_my_class comes from an class identifier and _an_instance is the postfix part.

Class jml2b.structure.statement.TTypeExp extends Expression implements Serializable

serialVersionUID: -7191104311045926981l

Serialized Fields

type

Type type

The type encapsulated in this expression

Class jml2b.structure.statement.UnaryExp extends Expression implements Serializable

serialVersionUID: -7603371494507794174l

Serialized Fields

exp

Expression exp

The sub expression of the current expression.

Class jml2b.structure.statement.WithTypeExp extends Expression implements Serializable

serialVersionUID: -7901462666342789890l

Serialized Fields

type

Type type

The type used in the expression. It cannot be null.

exp

Expression exp

The expression can be

• the parameter of a constructor call
• an array intialiazer
• a casted expression
• a tested with instanceof expression

dim

DimExpr dim

The dimensions of created arrays.

ident

Identifier ident

The identifier corresponding to the called constructor. It is only valid for an object created and is evaluated during the link.

Package jml2b.languages.java

Class jml2b.languages.java.JavaBinaryForm extends BinaryForm implements Serializable

Class jml2b.languages.java.JavaModifiedFieldForm extends ModifiedFieldForm implements Serializable

Class jml2b.languages.java.JavaQuantifiedForm extends QuantifiedForm implements Serializable

Class jml2b.languages.java.JavaTerminalForm extends TerminalForm implements Serializable

Class jml2b.languages.java.JavaTriaryForm extends TriaryForm implements Serializable

Class jml2b.languages.java.JavaTTypeForm extends TTypeForm implements Serializable

Class jml2b.languages.java.JavaType extends Type implements Serializable

Class jml2b.languages.java.JavaUnaryForm extends UnaryForm implements Serializable

Package jml2b.formula

Class jml2b.formula.BinaryForm extends Formula implements Serializable

serialVersionUID: 6458770229124292163l

Serialized Fields

left

Formula left

The left part of the binary formula.

right

Formula right

The right part of the binary formula.

Class jml2b.formula.ElementsForm extends TerminalForm implements Serializable

Serialized Fields

nameSuffix

int nameSuffix

Suffix number of the current formula.

tag

int tag

Tag corresponding to the type tag of the xxx type.

Class jml2b.formula.Formula extends Profiler implements Serializable

serialVersionUID: 2912250853358401101l

Serialized Fields

nodeType

byte nodeType

token describing this formula.

Class jml2b.formula.ModifiedFieldForm extends TerminalForm implements Serializable

Serialized Fields

m

IModifiesField m

Class jml2b.formula.QuantifiedForm extends Formula implements Serializable

serialVersionUID: 5392132877428547506l

Serialized Fields

vars

QuantifiedVarForm vars

The set of quantified variables

body

Formula body

The quantified formula

Class jml2b.formula.TerminalForm extends Formula implements Serializable

serialVersionUID: -5569956314641460620l

Serialized Fields

box

ParsedItem box

Parsed item corresponding to the terminal formula.

nodeText

java.lang.String nodeText

String corresponding to the formula. It can be empty if the formula corresponds to an identifier.

ident

Identifier ident

Identifier corresponding to the formula. It can be null if the formula does not correspond to an identifier.

postfix

boolean postfix

End of a formula create from an identifier and a string. This is used to create formula like c_my_class_an_instance. The part c_my_class comes from a class identifier and _an_instance is the postfix part.

Class jml2b.formula.TriaryForm extends Formula implements Serializable

Serialized Fields

f1

Formula f1

The condition or the restriction formula

left

Formula left

The formula corresponding to a valid condition or the left restricted formula

right

Formula right

The formula corresponding to a unvalid condition or the right restricted formula

Class jml2b.formula.TTypeForm extends Formula implements Serializable

serialVersionUID: 4552616253638519125l

Serialized Fields

nodeText

java.lang.String nodeText

String corresponding to this formula, when it corresponds to a loaded formula from a jpo file.

type

Type type

Type corresponding to this formula.

Class jml2b.formula.UnaryForm extends Formula implements Serializable

serialVersionUID: -5114454662274275537l

Serialized Fields

exp

Formula exp

The leaf formula.

Package jml2b.structure

Class jml2b.structure.AField extends Declaration implements Serializable

Class jml2b.structure.AMethod extends Declaration implements Serializable

Package jml2b.exceptions

Class jml2b.exceptions.ClassLoadException extends Jml2bException implements Serializable

Class jml2b.exceptions.InternalError extends java.lang.Error implements Serializable

Class jml2b.exceptions.Jml2bException extends java.lang.Exception implements Serializable

Class jml2b.exceptions.LanguageException extends java.lang.Exception implements Serializable

Class jml2b.exceptions.LinkException extends Jml2bException implements Serializable

Serialized Fields

line

int line

column

int column

errorMessage

java.lang.String errorMessage

Class jml2b.exceptions.LoadException extends java.lang.Exception implements Serializable

Class jml2b.exceptions.ParseException extends Jml2bException implements Serializable

Class jml2b.exceptions.PogException extends java.lang.Exception implements Serializable

Class jml2b.exceptions.TokenException extends ParseException implements Serializable

Class jml2b.exceptions.TranslationException extends LanguageException implements Serializable

Class jml2b.exceptions.TypeCheckException extends Jml2bException implements Serializable

Serialized Fields

line

int line

column

int column

errorMessage

java.lang.String errorMessage

Class jml2b.exceptions.WrongLabelException extends java.lang.Exception implements Serializable

Package jml2b.util

Class jml2b.util.JmlEntryFile extends JmlSourceEntryFile implements Serializable

serialVersionUID: -3266071808733837898l

Serialized Fields

absolutePath

java.lang.String absolutePath

Class jml2b.util.JmlEntryFileInJar extends JmlSourceEntryFile implements Serializable

serialVersionUID: 9045845756306025043l

Serialized Fields

ze

java.lang.String ze

zf

java.lang.String zf

Package jml2b.structure.java

Class jml2b.structure.java.AClass extends NamedNode implements Serializable

Serialized Fields

superClass

Type superClass

The superclass of this class (or interface). This field should not be null after the class is linked. In the case of the class java.lang.Object, the super class of java.lang.Object is set to java.lang.Object.

Class jml2b.structure.java.Class extends AClass implements Serializable

serialVersionUID: 4656487665386572390l

Serialized Fields

linkedState

int linkedState

The link state the class is in.

classPackage

Package classPackage

The package the class belongs to.

modifiers

Modifiers modifiers

The modifiers of the class (i.e. public, protected, etc...).

name

java.lang.String name

(short) name of the class.

interfaceModifier

boolean interfaceModifier

True if the class is an interface, false otherwise.

implementedInterfaces

java.util.Vector implementedInterfaces

Identifiers of implemented interfaces. Vector of Type elements.

See Also:

Type

fields

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

memberInvariants

java.util.Vector memberInvariants

Member invariants defined by the class. (Vector of jml2b.Invariants).

staticConstraints

java.util.Vector staticConstraints

instanceConstraints

java.util.Vector instanceConstraints

staticInvariants

java.util.Vector staticInvariants

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

See Also:

Invariant

staticFinalFieldInvariants

java.util.Vector staticFinalFieldInvariants

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

See Also:

Invariant

allInvariants

java.util.Vector allInvariants

All the invariants of the class. That is, the static invariants as well as the member invariants.

allConstraints

java.util.Vector allConstraints

depends

java.util.Vector depends

Set of depends clause. The elements contained within this vector are of type Depends

See Also:

Depends.

represents

java.util.Vector represents

Set of represents clause. The elements contained within this vector are of type Represents

See Also:

Represents.

methods

java.util.Vector methods

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

See Also:

Method

constructors

java.util.Vector constructors

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

See Also:

Method

externalClass

boolean externalClass

Boolean indicating wether the 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.

firstLine

int firstLine

Class jml2b.structure.java.Constraint extends Invariant implements Serializable

Class jml2b.structure.java.Constructor extends Method implements Serializable

serialVersionUID: -8652681423258987194l

Serialized Fields

saved

java.util.Vector saved

Class jml2b.structure.java.Declaration extends NamedNode implements Serializable

Serialized Fields

modifiers

Modifiers modifiers

The modifiers corresponding to the declaration.

definingClass

AClass definingClass

The class that contains the declaration.

Class jml2b.structure.java.Field extends AField implements Serializable

serialVersionUID: -7938980969842210873l

Serialized Fields

assign

Expression assign

AST containing potential assign clauses

name

java.lang.String name

Name of the field

type

Type type

Type of the field.

Class jml2b.structure.java.Identifier extends Profiler implements Serializable

serialVersionUID: -4315232328155671622l

Serialized Fields

name

java.lang.String name

idType

int idType

cl

AClass cl

mth

AMethod mth

pkg

Package pkg

field

AField field

Class jml2b.structure.java.Invariant extends Declaration implements Serializable

serialVersionUID: -953617783874540221l

Serialized Fields

property

Expression property

Expression corresponding to the invariant.

Class jml2b.structure.java.JmlFile extends java.lang.Object implements Serializable

serialVersionUID: -4142771309661361450l

Serialized Fields

fileName

JmlFileEntry fileName

FileName of the corresponding file (if any)

classes

java.util.Vector classes

Vector containing the different classes defined in this file. All the elements stored are of type Class.

importedPackages

java.util.Vector importedPackages

Vector containing the imported packages. That is, the packages P. imported as import P.*;

importedClasses

java.util.Map importedClasses

Vector containing the classes imported from other packages. It maps String (corresponding to the short name of the class to Package)

filePackage

Package filePackage

Package this files belongs to. It is set to root if the package is unnamed.

depends

java.util.Vector depends

Set of files name from witch this jml file depends.

langNames

java.lang.String[] langNames

externalFile

boolean externalFile

Boolean indicating wether the file is external to the parsed package.

Class jml2b.structure.java.Method extends AMethod implements Serializable

serialVersionUID: -5486363294234267483l

Serialized Fields

requires

Expression requires

The content of the requires clause.

jmlNormalized

boolean jmlNormalized

Boolean indicating wether the method is normalised or not.

body

Statement body

Body of the method.

specType

int specType

type of main specification of the method: behaviour, normal, ...

returnType

Type returnType

Return type of the method.

name

java.lang.String name

Name of the method.

signature

Parameters signature

exceptions

java.util.Vector exceptions

Vector of types corresponding to the content of the throws clause.

firstLine

int firstLine

The line in the file where the method begin.

specCases

java.util.Vector specCases

The different specification cases for the method. All the elements of this vector are of type SpecCase.

pmiName

java.lang.String pmiName

normalizedRequires

Expression normalizedRequires

isAnnotated

int isAnnotated

annotatedPrecondition

java.util.Vector annotatedPrecondition

annotatedPostcondition

java.util.Vector annotatedPostcondition

annotatedModifies

java.util.HashSet annotatedModifies

Class jml2b.structure.java.Modifiers extends Profiler implements Serializable

serialVersionUID: -1546518316935967328l

Serialized Fields

modifiers

int modifiers

Integer storing a bitmask of the flags corresponding to the modifiers.

Class jml2b.structure.java.NamedNode extends ParsedItem implements Serializable

serialVersionUID: 6128106779507407952l

Serialized Fields

nameIndex

int nameIndex

nameSuffix

int nameSuffix

garbage

boolean garbage

Class jml2b.structure.java.Package extends NamedNode implements Serializable

serialVersionUID: -4244945142001918487l

Serialized Fields

classMisses

java.util.Set classMisses

Set of classes that do not belongs to the package. this sets contains Strings corresponding to the name of the classes.

name

java.lang.String name

Short name of the package.

parent

Package parent

The parent package.

classes

java.util.Vector classes

Vector storing the classes defined in the package.

subPackages

java.util.Vector subPackages

Subpackages contained within this package.

keepPackage

boolean keepPackage

true if the package fields from this package should be kept when loading classes.

Class jml2b.structure.java.Parameters extends IAParameters implements Serializable

serialVersionUID: 8346824517287613664l

Serialized Fields

signature

java.util.Vector signature

vector containing fields corresponding to the signature

Class jml2b.structure.java.ParsedItem extends Profiler implements Serializable

serialVersionUID: -2308775037213438489l

Serialized Fields

line

int line

Line number where is located the item.

column

int column

Column number where the item is located.

length

int length

Length of the item.

jmlFile

JmlFile jmlFile

File where the item is located.

Class jml2b.structure.java.Type extends ParsedItem implements Serializable

serialVersionUID: -3537023320146708719l

Serialized Fields

tag

int tag

Tag describing the type of the Type (int, ref, refarray, etc...)

refType

AClass refType

Class of a reference type.

elemType

Type elemType

Type of elements stored in a reference array.

Package jml2b.structure.bytecode

Class jml2b.structure.bytecode.ClassDefaultConstructor extends ClassMethod implements Serializable

Class jml2b.structure.bytecode.ClassField extends AField implements Serializable

Serialized Fields

f

org.apache.bcel.classfile.Field f

t

Type t

definingClass

ClassFile definingClass

Class jml2b.structure.bytecode.ClassFile extends AClass implements Serializable

Serialized Fields

jc

org.apache.bcel.classfile.JavaClass jc

packg

Package packg

methods

ClassMethod[] methods

fields

ClassField[] fields

interfaces

AClass[] interfaces

Class jml2b.structure.bytecode.ClassMethod extends AMethod implements Serializable

Serialized Fields

m

org.apache.bcel.classfile.Method m

definingClass

ClassFile definingClass

returnType

Type returnType

cp

ClassParameters cp

Package jml2b.structure.jml

Class jml2b.structure.jml.Depends extends Declaration implements Serializable

Serialized Fields

abstractField

Modifies abstractField

The depends store ref

concreteFields

java.util.Vector concreteFields

The set of dependees

Class jml2b.structure.jml.Exsures extends Profiler implements Serializable

serialVersionUID: -1386643750550948016l

Serialized Fields

exceptionType

Type exceptionType

The type of the exception.

exceptionField

Field exceptionField

The field corresponding to the catched exception.

expression

Expression expression

The property ensured by this exsures clause.

Class jml2b.structure.jml.GuardedModifies extends ParsedItem implements Serializable

Serialized Fields

m

Modifies m

The modified store-ref

guardE

Expression guardE

The guard as an expression

Class jml2b.structure.jml.Modifies extends ParsedItem implements Serializable

Serialized Fields

stateType

Type stateType

The type of the modified variable.

Class jml2b.structure.jml.ModifiesClause extends ParsedItem implements Serializable

Class jml2b.structure.jml.ModifiesDot extends Modifies implements Serializable

serialVersionUID: -3809274145413661524l

Serialized Fields

leftE

Expression leftE

The instance on which the member field is applied.

m

ModifiesIdent m

The member field.

Class jml2b.structure.jml.ModifiesEverything extends ModifiesClause implements Serializable

serialVersionUID: 6457218174405239122l

Class jml2b.structure.jml.ModifiesIdent extends Modifies implements Serializable

serialVersionUID: -4877642697340175328l

Serialized Fields

ident

Identifier ident

The modified field

Class jml2b.structure.jml.ModifiesLbrack extends Modifies implements Serializable

serialVersionUID: -2052379372104415120l

Serialized Fields

sa

SpecArray sa

The indexes of modified element.

m

Modifies m

The array where element are modified

Class jml2b.structure.jml.ModifiesList extends ModifiesClause implements Serializable

serialVersionUID: -2459907009180805970l

Serialized Fields

gm

GuardedModifies gm

The current modified variable

next

ModifiesList next

The next modified variable of the modifies list.

Class jml2b.structure.jml.ModifiesNothing extends ModifiesClause implements Serializable

serialVersionUID: -2573792837984300742l

Class jml2b.structure.jml.Represents extends Declaration implements Serializable

Serialized Fields

depend

Modifies depend

The variable that is glued.

gluingInvariant

Expression gluingInvariant

The gluing invariant that can be a direct glue or a property.

Class jml2b.structure.jml.SpecArray extends ParsedItem implements Serializable

Class jml2b.structure.jml.SpecArrayDotDot extends SpecArray implements Serializable

serialVersionUID: -7820036551486276520l

Serialized Fields

e1

Expression e1

The low boundary mark as an expression

e2

Expression e2

The high boudary mark as an expression

Class jml2b.structure.jml.SpecArrayExpr extends SpecArray implements Serializable

serialVersionUID: -569168750574283801l

Serialized Fields

e

Expression e

The expression corresponding to the index

Class jml2b.structure.jml.SpecArrayStar extends SpecArray implements Serializable

serialVersionUID: -3630445878113787712l

Class jml2b.structure.jml.SpecCase extends ParsedItem implements Serializable

serialVersionUID: -6982092608895645311l

Serialized Fields

labels

java.util.Vector labels

Labels associated with this spec case. Labels are @see Expression.

requires

Expression requires

Content of the requires clause for this spec case.

ensures

Expression ensures

Content of the ensures clause for this spec case.

exsure

java.util.Vector exsure

Vector holding the content of the exsures clause for this spec case. All the elements of this vector are of type Exsures

modifies

ModifiesClause modifies

Content of the modifies clause. It can be null

modifiers

IModifiers modifiers

Visibility modifiers associated to this spec case. It can be null

Package jml2b.pog.lemma

Class jml2b.pog.lemma.ExceptionalProofs extends Proofs implements Serializable

Class jml2b.pog.lemma.Proofs extends java.lang.Object implements Serializable

serialVersionUID: -6703130784704083168l

Serialized Fields

locHyp

java.util.Vector locHyp

The set of hypothesis that are pointed by the theorems. The vector handles VirtualFormula.

locFlow

java.util.Vector locFlow

thl

TheoremList thl

The list of theorem. It may be null.

Class jml2b.pog.lemma.SimpleLemma extends Lemma implements Serializable

serialVersionUID: 3261667932288082895l

Serialized Fields

goals

java.util.Vector goals

The set of Goal

Class jml2b.pog.lemma.VariantLemma extends SimpleLemma implements Serializable

Class jml2b.pog.lemma.VirtualFormula extends Profiler implements Serializable

serialVersionUID: 4922534264367790116l

Serialized Fields

f

Formula f

The formula

flow

java.util.Vector flow

Set of colored informations associated with the formula

index

int index

Index of the formula (used to save the formula into jpo file)

origin

byte origin

The origin of the formula