Serialized Form

Package org.overturetool.vdmj.debug

Class org.overturetool.vdmj.debug.DBGPException extends java.lang.Exception implements Serializable

Serialized Fields

code

DBGPErrorCode code

reason

java.lang.String reason

Class org.overturetool.vdmj.debug.DBGPFeatures extends java.util.Properties implements Serializable

Package org.overturetool.vdmj.definitions

Class org.overturetool.vdmj.definitions.AccessSpecifier extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

isStatic

boolean isStatic

isAsync

boolean isAsync

access

Token access

Class org.overturetool.vdmj.definitions.AssignmentDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

expression

Expression expression

expType

Type expType

Class org.overturetool.vdmj.definitions.BUSClassDefinition extends ClassDefinition implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.definitions.ClassDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

supernames

LexNameList supernames

The names of the superclasses of this class.

definitions

DefinitionList definitions

The definitions in this class (excludes superclasses).

superInheritedDefinitions

DefinitionList superInheritedDefinitions

Definitions inherited from superclasses.

localInheritedDefinitions

DefinitionList localInheritedDefinitions

Definitions inherited, but accessed locally.

allInheritedDefinitions

DefinitionList allInheritedDefinitions

The combination of all inherited definitions.

supertypes

TypeList supertypes

A list of ClassTypes for the superclasses.

superdefs

ClassList superdefs

A list of ClassDefinitions for the superclasses.

classtype

Type classtype

This class' class type.

settingHierarchy

org.overturetool.vdmj.definitions.ClassDefinition.Setting settingHierarchy

typechecked

boolean typechecked

True if loaded from an object file (so type checked)

privateStaticValues

NameValuePairMap privateStaticValues

The private or protected static values in the class.

publicStaticValues

NameValuePairMap publicStaticValues

The public visible static values in the class.

staticInit

boolean staticInit

True if the class' static members are initialized.

staticValuesInit

boolean staticValuesInit

True if the class' static values are initialized.

invariant

ExplicitOperationDefinition invariant

The class invariant operation definition, if any.

invopvalue

OperationValue invopvalue

The class invariant operation value, if any.

invlistener

ClassInvariantListener invlistener

A listener for changes that require the class invariant to be checked.

isAbstract

boolean isAbstract

True if the class defines any abstract operations or functions.

gettingInheritable

boolean gettingInheritable

gettingInvDefs

boolean gettingInvDefs

Class org.overturetool.vdmj.definitions.ClassInvariantDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

expression

Expression expression

Class org.overturetool.vdmj.definitions.ClassList extends java.util.Vector<ClassDefinition> implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.definitions.CPUClassDefinition extends ClassDefinition implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.definitions.Definition extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the definition

name

LexNameToken name

The name of the object being defined.

nameScope

NameScope nameScope

The scope of the definition name.

pass

Pass pass

The pass to cover this definition in type checking.

used

boolean used

True if the definition has been used by the rest of the code.

accessSpecifier

AccessSpecifier accessSpecifier

A public/private/protected/static specifier, if any.

classDefinition

ClassDefinition classDefinition

A pointer to the enclosing class definition, if any.

Class org.overturetool.vdmj.definitions.DefinitionList extends java.util.Vector<Definition> implements Serializable

Class org.overturetool.vdmj.definitions.DefinitionSet extends java.util.HashSet<Definition> implements Serializable

Class org.overturetool.vdmj.definitions.EqualsDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

pattern

Pattern pattern

typebind

TypeBind typebind

setbind

SetBind setbind

test

Expression test

expType

Type expType

defs

DefinitionList defs

Class org.overturetool.vdmj.definitions.ExplicitFunctionDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

typeParams

LexNameList typeParams

type

FunctionType type

paramPatternList

java.util.List<E> paramPatternList

precondition

Expression precondition

postcondition

Expression postcondition

body

Expression body

isTypeInvariant

boolean isTypeInvariant

checkParamUsage

boolean checkParamUsage

measure

LexIdentifierToken measure

isCurried

boolean isCurried

predef

ExplicitFunctionDefinition predef

postdef

ExplicitFunctionDefinition postdef

paramDefinitionList

java.util.List<E> paramDefinitionList

expectedResult

Type expectedResult

actualResult

Type actualResult

isUndefined

boolean isUndefined

recursive

boolean recursive

measureLexical

int measureLexical

Class org.overturetool.vdmj.definitions.ExplicitOperationDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

type

OperationType type

parameterPatterns

PatternList parameterPatterns

precondition

Expression precondition

postcondition

Expression postcondition

body

Statement body

predef

ExplicitFunctionDefinition predef

postdef

ExplicitFunctionDefinition postdef

paramDefinitions

DefinitionList paramDefinitions

state

StateDefinition state

actualResult

Type actualResult

isConstructor

boolean isConstructor

Class org.overturetool.vdmj.definitions.ExternalDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

state

Definition state

readOnly

boolean readOnly

Class org.overturetool.vdmj.definitions.ImplicitFunctionDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

typeParams

LexNameList typeParams

parameterPatterns

java.util.List<E> parameterPatterns

result

PatternTypePair result

body

Expression body

precondition

Expression precondition

postcondition

Expression postcondition

measure

LexIdentifierToken measure

type

FunctionType type

predef

ExplicitFunctionDefinition predef

postdef

ExplicitFunctionDefinition postdef

recursive

boolean recursive

isUndefined

boolean isUndefined

measureLexical

int measureLexical

actualResult

Type actualResult

Class org.overturetool.vdmj.definitions.ImplicitOperationDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

parameterPatterns

java.util.List<E> parameterPatterns

result

PatternTypePair result

externals

java.util.List<E> externals

body

Statement body

precondition

Expression precondition

postcondition

Expression postcondition

errors

java.util.List<E> errors

type

OperationType type

predef

ExplicitFunctionDefinition predef

postdef

ExplicitFunctionDefinition postdef

state

StateDefinition state

actualResult

Type actualResult

stateDefinition

Definition stateDefinition

isConstructor

boolean isConstructor

Class org.overturetool.vdmj.definitions.ImportedDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

def

Definition def

Class org.overturetool.vdmj.definitions.InheritedDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

superdef

Definition superdef

oldname

LexNameToken oldname

Class org.overturetool.vdmj.definitions.InstanceVariableDefinition extends AssignmentDefinition implements Serializable

serialVersionUID: 1L

Serialized Fields

oldname

LexNameToken oldname

Class org.overturetool.vdmj.definitions.LocalDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

Class org.overturetool.vdmj.definitions.MultiBindListDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

bindings

java.util.List<E> bindings

defs

DefinitionList defs

Class org.overturetool.vdmj.definitions.MutexSyncDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

operations

LexNameList operations

Class org.overturetool.vdmj.definitions.NamedTraceDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

pathname

java.util.List<E> pathname

terms

java.util.List<E> terms

state

StateDefinition state

Class org.overturetool.vdmj.definitions.PerSyncDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

opname

LexNameToken opname

guard

Expression guard

Class org.overturetool.vdmj.definitions.RenamedDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

def

Definition def

Class org.overturetool.vdmj.definitions.StateDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

fields

java.util.List<E> fields

invPattern

Pattern invPattern

invExpression

Expression invExpression

initPattern

Pattern initPattern

initExpression

Expression initExpression

recordDefinition

LocalDefinition recordDefinition

invdef

ExplicitFunctionDefinition invdef

invfunc

FunctionValue invfunc

initdef

ExplicitFunctionDefinition initdef

initfunc

FunctionValue initfunc

statedefs

DefinitionList statedefs

recordType

Type recordType

moduleState

State moduleState

Class org.overturetool.vdmj.definitions.ThreadDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

statement

Statement statement

operationName

LexNameToken operationName

operationDef

ExplicitOperationDefinition operationDef

Class org.overturetool.vdmj.definitions.TypeDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

invPattern

Pattern invPattern

invExpression

Expression invExpression

invdef

ExplicitFunctionDefinition invdef

infinite

boolean infinite

Class org.overturetool.vdmj.definitions.UntypedDefinition extends Definition implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.definitions.ValueDefinition extends Definition implements Serializable

serialVersionUID: 1L

Serialized Fields

pattern

Pattern pattern

type

Type type

exp

Expression exp

defs

DefinitionList defs

expType

Type expType

Package org.overturetool.vdmj.expressions

Class org.overturetool.vdmj.expressions.AbsoluteExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.AndExpression extends BooleanBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.ApplyExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

root

Expression root

args

ExpressionList args

type

Type type

argtypes

TypeList argtypes

recursive

Definition recursive

Class org.overturetool.vdmj.expressions.BinaryExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

left

Expression left

right

Expression right

op

LexToken op

ltype

Type ltype

rtype

Type rtype

Class org.overturetool.vdmj.expressions.BooleanBinaryExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.BooleanLiteralExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexBooleanToken value

Class org.overturetool.vdmj.expressions.BreakpointExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

bp

Breakpoint bp

cond

BreakpointCondition cond

arg

long arg

Class org.overturetool.vdmj.expressions.CardinalityExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.CaseAlternative extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

cexp

Expression cexp

plist

PatternList plist

result

Expression result

defs

DefinitionList defs

Class org.overturetool.vdmj.expressions.CasesExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

exp

Expression exp

cases

java.util.List<E> cases

others

Expression others

expType

Type expType

Class org.overturetool.vdmj.expressions.CharLiteralExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexCharacterToken value

Class org.overturetool.vdmj.expressions.CompExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DefExpression extends LetDefExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DistConcatExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DistIntersectExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DistMergeExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DistUnionExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DivExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DivideExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DomainResByExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.DomainResToExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.ElementsExpression extends SetExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

exp

Expression exp

Class org.overturetool.vdmj.expressions.ElseIfExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

elseIfExp

Expression elseIfExp

thenExp

Expression thenExp

Class org.overturetool.vdmj.expressions.EqualsExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.EquivalentExpression extends BooleanBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.Exists1Expression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

bind

Bind bind

predicate

Expression predicate

def

Definition def

Class org.overturetool.vdmj.expressions.ExistsExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

bindList

java.util.List<E> bindList

predicate

Expression predicate

Class org.overturetool.vdmj.expressions.Expression extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the expression.

breakpoint

Breakpoint breakpoint

The expression's breakpoint, if any.

Class org.overturetool.vdmj.expressions.ExpressionList extends java.util.Vector<Expression> implements Serializable

Class org.overturetool.vdmj.expressions.FieldExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

object

Expression object

field

LexIdentifierToken field

memberName

LexNameToken memberName

Class org.overturetool.vdmj.expressions.FieldNumberExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

tuple

Expression tuple

field

LexIntegerToken field

type

Type type

Class org.overturetool.vdmj.expressions.FloorExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.ForAllExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

bindList

java.util.List<E> bindList

predicate

Expression predicate

Class org.overturetool.vdmj.expressions.FuncInstantiationExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

function

Expression function

actualTypes

TypeList actualTypes

type

FunctionType type

expdef

ExplicitFunctionDefinition expdef

impdef

ImplicitFunctionDefinition impdef

Class org.overturetool.vdmj.expressions.GreaterEqualExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.GreaterExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.HeadExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.HistoryExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

hop

Token hop

opnames

LexNameList opnames

Class org.overturetool.vdmj.expressions.IfExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

ifExp

Expression ifExp

thenExp

Expression thenExp

elseList

java.util.List<E> elseList

elseExp

Expression elseExp

Class org.overturetool.vdmj.expressions.ImpliesExpression extends BooleanBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.IndicesExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.InSetExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.IntegerLiteralExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexIntegerToken value

Class org.overturetool.vdmj.expressions.IotaExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

bind

Bind bind

predicate

Expression predicate

Class org.overturetool.vdmj.expressions.IsExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

basictype

Type basictype

typename

LexNameToken typename

test

Expression test

typedef

Definition typedef

Class org.overturetool.vdmj.expressions.IsOfBaseClassExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

baseclass

LexNameToken baseclass

exp

Expression exp

Class org.overturetool.vdmj.expressions.IsOfClassExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

classname

LexNameToken classname

exp

Expression exp

Class org.overturetool.vdmj.expressions.LambdaExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

bindList

java.util.List<E> bindList

expression

Expression expression

type

FunctionType type

paramPatterns

PatternList paramPatterns

paramDefinitions

DefinitionList paramDefinitions

Class org.overturetool.vdmj.expressions.LenExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.LessEqualExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.LessExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.LetBeStExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

bind

MultipleBind bind

suchThat

Expression suchThat

value

Expression value

def

MultiBindListDefinition def

Class org.overturetool.vdmj.expressions.LetDefExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

localDefs

DefinitionList localDefs

expression

Expression expression

Class org.overturetool.vdmj.expressions.MapCompExpression extends MapExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

first

Expression first

bindings

java.util.List<E> bindings

predicate

Expression predicate

maptype

Type maptype

Class org.overturetool.vdmj.expressions.MapDomainExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.MapEnumExpression extends MapExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

members

java.util.List<E> members

domtypes

TypeList domtypes

rngtypes

TypeList rngtypes

Class org.overturetool.vdmj.expressions.MapExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.MapInverseExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

type

MapType type

Class org.overturetool.vdmj.expressions.MapletExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.MapRangeExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.MapUnionExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.MkBasicExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

arg

Expression arg

Class org.overturetool.vdmj.expressions.MkTypeExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

typename

LexNameToken typename

args

ExpressionList args

recordType

RecordType recordType

argTypes

TypeList argTypes

Class org.overturetool.vdmj.expressions.ModExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.MuExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

record

Expression record

modifiers

java.util.List<E> modifiers

recordType

RecordType recordType

modTypes

TypeList modTypes

Class org.overturetool.vdmj.expressions.NewExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

classname

LexIdentifierToken classname

args

ExpressionList args

classdef

ClassDefinition classdef

ctorDefinition

Definition ctorDefinition

Class org.overturetool.vdmj.expressions.NilExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.NotEqualExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.NotExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.NotInSetExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.NotYetSpecifiedExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.NumericBinaryExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.OrExpression extends BooleanBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.PlusExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.PlusPlusExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.PostOpExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

opname

LexNameToken opname

expression

Expression expression

state

StateDefinition state

Class org.overturetool.vdmj.expressions.PowerSetExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.PreExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

function

Expression function

args

ExpressionList args

Class org.overturetool.vdmj.expressions.PreOpExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

opname

LexNameToken opname

expression

Expression expression

state

StateDefinition state

Class org.overturetool.vdmj.expressions.ProperSubsetExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.QuoteLiteralExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

type

LexQuoteToken type

Class org.overturetool.vdmj.expressions.RangeResByExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.RangeResToExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.RealLiteralExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexRealToken value

Class org.overturetool.vdmj.expressions.RecordModifier extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

tag

LexIdentifierToken tag

value

Expression value

Class org.overturetool.vdmj.expressions.RemExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.ReverseExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SameBaseClassExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

left

Expression left

right

Expression right

Class org.overturetool.vdmj.expressions.SameClassExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

left

Expression left

right

Expression right

Class org.overturetool.vdmj.expressions.SelfExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

Class org.overturetool.vdmj.expressions.SeqCompExpression extends SeqExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

first

Expression first

setbind

SetBind setbind

predicate

Expression predicate

Class org.overturetool.vdmj.expressions.SeqConcatExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SeqEnumExpression extends SeqExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

members

ExpressionList members

types

TypeList types

Class org.overturetool.vdmj.expressions.SeqExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SetCompExpression extends SetExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

first

Expression first

bindings

java.util.List<E> bindings

predicate

Expression predicate

settype

SetType settype

Class org.overturetool.vdmj.expressions.SetDifferenceExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SetEnumExpression extends SetExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

members

ExpressionList members

types

TypeList types

Class org.overturetool.vdmj.expressions.SetExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SetIntersectExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SetRangeExpression extends SetExpression implements Serializable

serialVersionUID: 1L

Serialized Fields

first

Expression first

last

Expression last

ftype

Type ftype

ltype

Type ltype

Class org.overturetool.vdmj.expressions.SetUnionExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.StarStarExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.StateInitExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

state

StateDefinition state

Class org.overturetool.vdmj.expressions.StringLiteralExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexStringToken value

Class org.overturetool.vdmj.expressions.SubclassResponsibilityExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SubseqExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

seq

Expression seq

from

Expression from

to

Expression to

ftype

Type ftype

ttype

Type ttype

Class org.overturetool.vdmj.expressions.SubsetExpression extends BinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.SubtractExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.TailExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.ThreadIdExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.TimeExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.TimesExpression extends NumericBinaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.TupleExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

args

ExpressionList args

types

TypeList types

Class org.overturetool.vdmj.expressions.UnaryExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

exp

Expression exp

Class org.overturetool.vdmj.expressions.UnaryMinusExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.UnaryPlusExpression extends UnaryExpression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.UndefinedExpression extends Expression implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.expressions.VariableExpression extends Expression implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

vardef

Definition vardef

original

java.lang.String original

Package org.overturetool.vdmj.lex

Class org.overturetool.vdmj.lex.LexBooleanToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

value

boolean value

Class org.overturetool.vdmj.lex.LexCharacterToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

unicode

char unicode

Class org.overturetool.vdmj.lex.LexException extends LocatedException implements Serializable

Class org.overturetool.vdmj.lex.LexIdentifierToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

name

java.lang.String name

old

boolean old

Class org.overturetool.vdmj.lex.LexIntegerToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

value

long value

Class org.overturetool.vdmj.lex.LexKeywordToken extends LexToken implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.lex.LexLocation extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

executable

boolean executable

True if the location is executable.

file

java.io.File file

The filename of the token.

module

java.lang.String module

The module/class name of the token.

startLine

int startLine

The line number of the start of the token.

startPos

int startPos

The character position of the start of the token.

endLine

int endLine

The last line of the token.

endPos

int endPos

The character position of the end of the token.

hits

long hits

The number of times the location has been executed.

Class org.overturetool.vdmj.lex.LexNameList extends java.util.Vector<LexNameToken> implements Serializable

Class org.overturetool.vdmj.lex.LexNameToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

module

java.lang.String module

name

java.lang.String name

old

boolean old

explicit

boolean explicit

typeQualifier

TypeList typeQualifier

hashcode

int hashcode

Class org.overturetool.vdmj.lex.LexQuoteToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

value

java.lang.String value

Class org.overturetool.vdmj.lex.LexRealToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

value

double value

Class org.overturetool.vdmj.lex.LexStringToken extends LexToken implements Serializable

serialVersionUID: 1L

Serialized Fields

value

java.lang.String value

Class org.overturetool.vdmj.lex.LexToken extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the token.

type

Token type

The basic type of the token.

Package org.overturetool.vdmj.messages

Class org.overturetool.vdmj.messages.InternalException extends java.lang.RuntimeException implements Serializable

Serialized Fields

number

int number

Class org.overturetool.vdmj.messages.LocatedException extends NumberedException implements Serializable

Serialized Fields

location

LexLocation location

Class org.overturetool.vdmj.messages.NumberedException extends java.lang.Exception implements Serializable

Serialized Fields

number

int number

Class org.overturetool.vdmj.messages.VDMErrorsException extends java.lang.Exception implements Serializable

Serialized Fields

errors

java.util.List<E> errors

Package org.overturetool.vdmj.modules

Class org.overturetool.vdmj.modules.DLModule extends Module implements Serializable

serialVersionUID: 1L

Serialized Fields

library

LexStringToken library

The name of the uselib library.

Class org.overturetool.vdmj.modules.Export extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the export statement.

Class org.overturetool.vdmj.modules.ExportAll extends Export implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.modules.ExportedFunction extends Export implements Serializable

serialVersionUID: 1L

Serialized Fields

nameList

LexNameList nameList

type

Type type

Class org.overturetool.vdmj.modules.ExportedOperation extends Export implements Serializable

serialVersionUID: 1L

Serialized Fields

nameList

LexNameList nameList

type

Type type

Class org.overturetool.vdmj.modules.ExportedType extends Export implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

struct

boolean struct

Class org.overturetool.vdmj.modules.ExportedValue extends Export implements Serializable

serialVersionUID: 1L

Serialized Fields

nameList

LexNameList nameList

type

Type type

Class org.overturetool.vdmj.modules.Import extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the import declaration.

name

LexNameToken name

The name of the object being imported.

renamed

LexNameToken renamed

The renamed name of the object being imported.

from

Module from

The Module imported from.

Class org.overturetool.vdmj.modules.ImportAll extends Import implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.modules.ImportedFunction extends ImportedValue implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.modules.ImportedOperation extends ImportedValue implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.modules.ImportedType extends Import implements Serializable

serialVersionUID: 1L

Serialized Fields

def

TypeDefinition def

Class org.overturetool.vdmj.modules.ImportedValue extends Import implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

Class org.overturetool.vdmj.modules.ImportFromModule extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexIdentifierToken name

signatures

java.util.List<E> signatures

Class org.overturetool.vdmj.modules.Module extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexIdentifierToken name

The module name.

imports

ModuleImports imports

A list of import declarations.

exports

ModuleExports exports

A list of export declarations.

defs

DefinitionList defs

A list of definitions created in the module.

exportdefs

DefinitionList exportdefs

Those definitions which are exported.

importdefs

DefinitionList importdefs

Definitions of imported objects from other modules.

typechecked

boolean typechecked

True if the module was loaded from an object file.

Class org.overturetool.vdmj.modules.ModuleExports extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

exports

java.util.List<E> exports

Class org.overturetool.vdmj.modules.ModuleImports extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexIdentifierToken name

imports

java.util.List<E> imports

Class org.overturetool.vdmj.modules.ModuleList extends java.util.Vector<Module> implements Serializable

Package org.overturetool.vdmj.patterns

Class org.overturetool.vdmj.patterns.Bind extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the bind.

pattern

Pattern pattern

The pattern of the bind.

Class org.overturetool.vdmj.patterns.BooleanPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexBooleanToken value

Class org.overturetool.vdmj.patterns.CharacterPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexCharacterToken value

Class org.overturetool.vdmj.patterns.ConcatenationPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

left

Pattern left

right

Pattern right

Class org.overturetool.vdmj.patterns.ExpressionPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

exp

Expression exp

Class org.overturetool.vdmj.patterns.IdentifierPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

Class org.overturetool.vdmj.patterns.IgnorePattern extends Pattern implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.patterns.IntegerPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexIntegerToken value

Class org.overturetool.vdmj.patterns.MultipleBind extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the bind.

plist

PatternList plist

The list of patterns for this bind.

Class org.overturetool.vdmj.patterns.MultipleSetBind extends MultipleBind implements Serializable

serialVersionUID: 1L

Serialized Fields

set

Expression set

Class org.overturetool.vdmj.patterns.MultipleTypeBind extends MultipleBind implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

Class org.overturetool.vdmj.patterns.Pattern extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The textual location of the pattern.

resolved

boolean resolved

A flag to prevent recursive type resolution problems.

Class org.overturetool.vdmj.patterns.PatternBind extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

pattern

Pattern pattern

bind

Bind bind

defs

DefinitionList defs

Class org.overturetool.vdmj.patterns.PatternList extends java.util.Vector<Pattern> implements Serializable

Class org.overturetool.vdmj.patterns.QuotePattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexQuoteToken value

Class org.overturetool.vdmj.patterns.RealPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexRealToken value

Class org.overturetool.vdmj.patterns.RecordPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

typename

LexNameToken typename

plist

PatternList plist

type

Type type

Class org.overturetool.vdmj.patterns.SeqPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

plist

PatternList plist

Class org.overturetool.vdmj.patterns.SetBind extends Bind implements Serializable

serialVersionUID: 1L

Serialized Fields

set

Expression set

Class org.overturetool.vdmj.patterns.SetPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

plist

PatternList plist

Class org.overturetool.vdmj.patterns.StringPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

value

LexStringToken value

Class org.overturetool.vdmj.patterns.TuplePattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

plist

PatternList plist

Class org.overturetool.vdmj.patterns.TypeBind extends Bind implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

Class org.overturetool.vdmj.patterns.UnionPattern extends Pattern implements Serializable

serialVersionUID: 1L

Serialized Fields

left

Pattern left

right

Pattern right

Package org.overturetool.vdmj.pog

Class org.overturetool.vdmj.pog.POContextStack extends java.util.Stack<POContext> implements Serializable

Class org.overturetool.vdmj.pog.ProofObligationList extends java.util.Vector<ProofObligation> implements Serializable

Package org.overturetool.vdmj.runtime

Class org.overturetool.vdmj.runtime.Breakpoint extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The location of the breakpoint.

number

int number

The number of the breakpoint.

parsed

Expression parsed

The condition or trace expression, in parsed form.

trace

java.lang.String trace

The condition or trace expression, in raw form.

hits

long hits

The number of times this breakpoint has been reached.

Class org.overturetool.vdmj.runtime.ClassContext extends RootContext implements Serializable

Serialized Fields

classdef

ClassDefinition classdef

Class org.overturetool.vdmj.runtime.Context extends java.util.HashMap<LexNameToken,Value> implements Serializable

Serialized Fields

location

LexLocation location

The location of the context.

title

java.lang.String title

The name of the location.

outer

Context outer

A link to a lower level context, if present.

threadState

ThreadState threadState

The thread state associated with this context.

Class org.overturetool.vdmj.runtime.ContextException extends java.lang.RuntimeException implements Serializable

Serialized Fields

location

LexLocation location

ctxt

Context ctxt

number

int number

Class org.overturetool.vdmj.runtime.DebuggerException extends java.lang.RuntimeException implements Serializable

Class org.overturetool.vdmj.runtime.ExitException extends ContextException implements Serializable

Serialized Fields

value

Value value

Class org.overturetool.vdmj.runtime.ObjectContext extends RootContext implements Serializable

Serialized Fields

self

ObjectValue self

Class org.overturetool.vdmj.runtime.PatternMatchException extends LocatedException implements Serializable

Class org.overturetool.vdmj.runtime.RootContext extends Context implements Serializable

Class org.overturetool.vdmj.runtime.RTException extends java.lang.RuntimeException implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.runtime.StateContext extends RootContext implements Serializable

Serialized Fields

stateCtxt

Context stateCtxt

The state context, if any.

Class org.overturetool.vdmj.runtime.StopException extends java.lang.RuntimeException implements Serializable

Serialized Fields

location

LexLocation location

ctxt

Context ctxt

Class org.overturetool.vdmj.runtime.Stoppoint extends Breakpoint implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.runtime.Tracepoint extends Breakpoint implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.runtime.ValueException extends NumberedException implements Serializable

Serialized Fields

ctxt

Context ctxt

Package org.overturetool.vdmj.statements

Class org.overturetool.vdmj.statements.AlwaysStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

always

Statement always

body

Statement body

Class org.overturetool.vdmj.statements.AssignmentStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

exp

Expression exp

target

StateDesignator target

targetType

Type targetType

expType

Type expType

classInvExists

boolean classInvExists

Class org.overturetool.vdmj.statements.AtomicStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

assignments

java.util.List<E> assignments

statedef

StateDefinition statedef

classdef

ClassDefinition classdef

Class org.overturetool.vdmj.statements.BlockStatement extends SimpleBlockStatement implements Serializable

serialVersionUID: 1L

Serialized Fields

assignmentDefs

DefinitionList assignmentDefs

Class org.overturetool.vdmj.statements.CallObjectStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

designator

ObjectDesignator designator

classname

java.lang.String classname

fieldname

java.lang.String fieldname

args

ExpressionList args

explicit

boolean explicit

field

LexNameToken field

Class org.overturetool.vdmj.statements.CallStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

args

ExpressionList args

Class org.overturetool.vdmj.statements.CasesStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

exp

Expression exp

cases

java.util.List<E> cases

others

Statement others

expType

Type expType

Class org.overturetool.vdmj.statements.CaseStmtAlternative extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

plist

PatternList plist

statement

Statement statement

defs

DefinitionList defs

Class org.overturetool.vdmj.statements.ClassInvariantStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

invdefs

DefinitionList invdefs

Class org.overturetool.vdmj.statements.CyclesStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

cycles

Expression cycles

statement

Statement statement

Class org.overturetool.vdmj.statements.DefStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

equalsDefs

DefinitionList equalsDefs

statement

Statement statement

Class org.overturetool.vdmj.statements.DurationStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

duration

Expression duration

statement

Statement statement

step

long step

Class org.overturetool.vdmj.statements.ElseIfStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

elseIfExp

Expression elseIfExp

thenStmt

Statement thenStmt

Class org.overturetool.vdmj.statements.ErrorStatement extends Statement implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.statements.ExitStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

expression

Expression expression

exptype

Type exptype

Class org.overturetool.vdmj.statements.ExternalClause extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

mode

LexToken mode

identifiers

LexNameList identifiers

type

Type type

Class org.overturetool.vdmj.statements.FieldDesignator extends StateDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

object

StateDesignator object

field

LexIdentifierToken field

objectfield

LexNameToken objectfield

Class org.overturetool.vdmj.statements.ForAllStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

pattern

Pattern pattern

set

Expression set

statement

Statement statement

setType

Type setType

Class org.overturetool.vdmj.statements.ForIndexStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

var

LexNameToken var

from

Expression from

to

Expression to

by

Expression by

statement

Statement statement

Class org.overturetool.vdmj.statements.ForPatternBindStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

patternBind

PatternBind patternBind

reverse

boolean reverse

exp

Expression exp

statement

Statement statement

seqType

SeqType seqType

Class org.overturetool.vdmj.statements.IdentifierDesignator extends StateDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

Class org.overturetool.vdmj.statements.IfStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

ifExp

Expression ifExp

thenStmt

Statement thenStmt

elseList

java.util.List<E> elseList

elseStmt

Statement elseStmt

Class org.overturetool.vdmj.statements.LetBeStStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

bind

MultipleBind bind

suchThat

Expression suchThat

statement

Statement statement

def

MultiBindListDefinition def

Class org.overturetool.vdmj.statements.LetDefStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

localDefs

DefinitionList localDefs

statement

Statement statement

Class org.overturetool.vdmj.statements.MapSeqDesignator extends StateDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

mapseq

StateDesignator mapseq

exp

Expression exp

mapType

MapType mapType

seqType

SeqType seqType

Class org.overturetool.vdmj.statements.NonDeterministicStatement extends SimpleBlockStatement implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.statements.NotYetSpecifiedStatement extends Statement implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.statements.ObjectApplyDesignator extends ObjectDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

object

ObjectDesignator object

args

ExpressionList args

Class org.overturetool.vdmj.statements.ObjectDesignator extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

Class org.overturetool.vdmj.statements.ObjectFieldDesignator extends ObjectDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

object

ObjectDesignator object

classname

java.lang.String classname

fieldname

java.lang.String fieldname

field

LexNameToken field

Class org.overturetool.vdmj.statements.ObjectIdentifierDesignator extends ObjectDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

expression

VariableExpression expression

Class org.overturetool.vdmj.statements.ObjectNewDesignator extends ObjectDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

expression

NewExpression expression

Class org.overturetool.vdmj.statements.ObjectSelfDesignator extends ObjectDesignator implements Serializable

serialVersionUID: 1L

Serialized Fields

self

LexNameToken self

Class org.overturetool.vdmj.statements.PeriodicStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

opname

LexNameToken opname

args

ExpressionList args

Class org.overturetool.vdmj.statements.ReturnStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

expression

Expression expression

Class org.overturetool.vdmj.statements.SimpleBlockStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

statements

java.util.List<E> statements

Class org.overturetool.vdmj.statements.SkipStatement extends Statement implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.statements.SpecificationStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

externals

java.util.List<E> externals

precondition

Expression precondition

postcondition

Expression postcondition

errors

java.util.List<E> errors

Class org.overturetool.vdmj.statements.StartStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

objects

Expression objects

Class org.overturetool.vdmj.statements.StateDesignator extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

Class org.overturetool.vdmj.statements.Statement extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The location of the statement.

breakpoint

Breakpoint breakpoint

The statement's breakpoint, if any.

Class org.overturetool.vdmj.statements.SubclassResponsibilityStatement extends Statement implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.statements.TixeStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

traps

java.util.List<E> traps

body

Statement body

Class org.overturetool.vdmj.statements.TraceStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

tracedef

NamedTraceDefinition tracedef

Class org.overturetool.vdmj.statements.TrapStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

patternBind

PatternBind patternBind

with

Statement with

body

Statement body

Class org.overturetool.vdmj.statements.WhileStatement extends Statement implements Serializable

serialVersionUID: 1L

Serialized Fields

exp

Expression exp

statement

Statement statement

Package org.overturetool.vdmj.syntax

Class org.overturetool.vdmj.syntax.ParserException extends LocatedException implements Serializable

Serialized Fields

depth

int depth

Class org.overturetool.vdmj.syntax.SystemDefinition extends ClassDefinition implements Serializable

serialVersionUID: 1L

Package org.overturetool.vdmj.traces

Class org.overturetool.vdmj.traces.CallSequence extends java.util.Vector<Statement> implements Serializable

Serialized Fields

ctxt

Context ctxt

needsContext

boolean needsContext

hashes

java.util.List<E> hashes

filtered

int filtered

Class org.overturetool.vdmj.traces.TestSequence extends java.util.Vector<CallSequence> implements Serializable

Class org.overturetool.vdmj.traces.TraceApplyExpression extends TraceCoreDefinition implements Serializable

serialVersionUID: 1L

Serialized Fields

statement

CallObjectStatement statement

Class org.overturetool.vdmj.traces.TraceBracketedExpression extends TraceCoreDefinition implements Serializable

serialVersionUID: 1L

Serialized Fields

terms

java.util.List<E> terms

Class org.overturetool.vdmj.traces.TraceCoreDefinition extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

Class org.overturetool.vdmj.traces.TraceDefinition extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

Class org.overturetool.vdmj.traces.TraceDefinitionTerm extends java.util.Vector<TraceDefinition> implements Serializable

Class org.overturetool.vdmj.traces.TraceLetBeStBinding extends TraceDefinition implements Serializable

serialVersionUID: 1L

Serialized Fields

bind

MultipleBind bind

stexp

Expression stexp

body

TraceDefinition body

def

MultiBindListDefinition def

Class org.overturetool.vdmj.traces.TraceLetDefBinding extends TraceDefinition implements Serializable

serialVersionUID: 1L

Serialized Fields

localDefs

java.util.List<E> localDefs

body

TraceDefinition body

Class org.overturetool.vdmj.traces.TraceRepeatDefinition extends TraceDefinition implements Serializable

serialVersionUID: 1L

Serialized Fields

core

TraceCoreDefinition core

from

long from

to

long to

Package org.overturetool.vdmj.typechecker

Class org.overturetool.vdmj.typechecker.TypeCheckException extends java.lang.RuntimeException implements Serializable

Serialized Fields

location

LexLocation location

Package org.overturetool.vdmj.types

Class org.overturetool.vdmj.types.BasicType extends Type implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.BooleanType extends BasicType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.BracketType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

Class org.overturetool.vdmj.types.CharacterType extends BasicType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.ClassType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

classdef

ClassDefinition classdef

name

LexNameToken name

Class org.overturetool.vdmj.types.Field extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

accessibility

AccessSpecifier accessibility

tagname

LexNameToken tagname

tag

java.lang.String tag

type

Type type

equalityAbstration

boolean equalityAbstration

Class org.overturetool.vdmj.types.FunctionType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

parameters

TypeList parameters

result

Type result

partial

boolean partial

Class org.overturetool.vdmj.types.InMapType extends MapType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.IntegerType extends NumericType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.InvariantType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

invdef

ExplicitFunctionDefinition invdef

Class org.overturetool.vdmj.types.MapType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

from

Type from

to

Type to

empty

boolean empty

Class org.overturetool.vdmj.types.NamedType extends InvariantType implements Serializable

serialVersionUID: 1L

Serialized Fields

typename

LexNameToken typename

type

Type type

Class org.overturetool.vdmj.types.NaturalOneType extends NumericType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.NaturalType extends NumericType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.NumericType extends BasicType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.OperationType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

parameters

TypeList parameters

result

Type result

Class org.overturetool.vdmj.types.OptionalType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

Class org.overturetool.vdmj.types.ParameterType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

Class org.overturetool.vdmj.types.PatternListTypePair extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

patterns

PatternList patterns

type

Type type

Class org.overturetool.vdmj.types.PatternTypePair extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

pattern

Pattern pattern

type

Type type

resolved

boolean resolved

Class org.overturetool.vdmj.types.ProductType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

types

TypeList types

Class org.overturetool.vdmj.types.QuoteType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

value

java.lang.String value

Class org.overturetool.vdmj.types.RationalType extends NumericType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.RealType extends NumericType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.RecordType extends InvariantType implements Serializable

serialVersionUID: 1L

Serialized Fields

name

LexNameToken name

fields

java.util.List<E> fields

infinite

boolean infinite

Class org.overturetool.vdmj.types.Seq1Type extends SeqType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.SeqType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

seqof

Type seqof

empty

boolean empty

Class org.overturetool.vdmj.types.SetType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

setof

Type setof

empty

boolean empty

Class org.overturetool.vdmj.types.TokenType extends BasicType implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.Type extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

The location of the type definition.

resolved

boolean resolved

True if the type's and its subtype's names have been resolved.

definitions

DefinitionList definitions

The type's possible definition(s) (if a named type)

inToString

boolean inToString

A flag to prevent recursive types from failing toString().

Class org.overturetool.vdmj.types.TypeList extends java.util.Vector<Type> implements Serializable

Class org.overturetool.vdmj.types.TypeSet extends java.util.TreeSet<Type> implements Serializable

Class org.overturetool.vdmj.types.UndefinedType extends Type implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.UnionType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

types

TypeSet types

setType

SetType setType

seqType

SeqType seqType

mapType

MapType mapType

recType

RecordType recType

numType

NumericType numType

prodType

ProductType prodType

funcType

FunctionType funcType

opType

OperationType opType

classType

ClassType classType

setDone

boolean setDone

seqDone

boolean seqDone

mapDone

boolean mapDone

recDone

boolean recDone

numDone

boolean numDone

funDone

boolean funDone

opDone

boolean opDone

classDone

boolean classDone

prodCard

int prodCard

expanded

boolean expanded

infinite

boolean infinite

Class org.overturetool.vdmj.types.UnknownType extends Type implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.UnresolvedType extends Type implements Serializable

serialVersionUID: 1L

Serialized Fields

typename

LexNameToken typename

Class org.overturetool.vdmj.types.VoidReturnType extends Type implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.types.VoidType extends Type implements Serializable

serialVersionUID: 1L

Package org.overturetool.vdmj.values

Class org.overturetool.vdmj.values.BooleanValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

value

boolean value

Class org.overturetool.vdmj.values.BUSValue extends ObjectValue implements Serializable

serialVersionUID: 1L

Serialized Fields

busNumber

int busNumber

policy

BUSPolicy policy

speed

double speed

cpus

ValueSet cpus

name

java.lang.String name

cq

ControlQueue cq

Class org.overturetool.vdmj.values.CharacterValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

unicode

char unicode

Class org.overturetool.vdmj.values.ClassInvariantListener extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

invopvalue

OperationValue invopvalue

doInvariantChecks

boolean doInvariantChecks

Class org.overturetool.vdmj.values.CompFunctionValue extends FunctionValue implements Serializable

serialVersionUID: 1L

Serialized Fields

ff1

FunctionValue ff1

ff2

FunctionValue ff2

Class org.overturetool.vdmj.values.CPUValue extends ObjectValue implements Serializable

serialVersionUID: 1L

Serialized Fields

cpuNumber

int cpuNumber

policy

SchedulingPolicy policy

cyclesPerSec

double cyclesPerSec

deployed

java.util.List<E> deployed

objects

java.util.Map<K,V> objects

name

java.lang.String name

runningThread

java.lang.Thread runningThread

switches

int switches

Class org.overturetool.vdmj.values.FieldMap extends java.util.Vector<FieldValue> implements Serializable

Class org.overturetool.vdmj.values.FieldValue extends java.lang.Object implements Serializable

serialVersionUID: 1L

Serialized Fields

name

java.lang.String name

value

Value value

comparable

boolean comparable

Class org.overturetool.vdmj.values.FunctionValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

location

LexLocation location

name

java.lang.String name

typeValues

NameValuePairList typeValues

type

FunctionType type

paramPatternList

java.util.List<E> paramPatternList

body

Expression body

precondition

FunctionValue precondition

postcondition

FunctionValue postcondition

freeVariables

Context freeVariables

checkInvariants

boolean checkInvariants

self

ObjectValue self

isStatic

boolean isStatic

classdef

ClassDefinition classdef

Class org.overturetool.vdmj.values.IntegerValue extends RationalValue implements Serializable

serialVersionUID: 1L

Serialized Fields

longVal

long longVal

Class org.overturetool.vdmj.values.InvariantValue extends ReferenceValue implements Serializable

serialVersionUID: 1L

Serialized Fields

type

NamedType type

Class org.overturetool.vdmj.values.IterFunctionValue extends FunctionValue implements Serializable

serialVersionUID: 1L

Serialized Fields

function

FunctionValue function

iterations

long iterations

Class org.overturetool.vdmj.values.MapValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

values

ValueMap values

Class org.overturetool.vdmj.values.NameValuePairList extends java.util.Vector<NameValuePair> implements Serializable

Class org.overturetool.vdmj.values.NameValuePairMap extends java.util.HashMap<LexNameToken,Value> implements Serializable

Class org.overturetool.vdmj.values.NaturalOneValue extends NaturalValue implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.NaturalValue extends IntegerValue implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.NilValue extends Value implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.NumericValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

value

double value

Class org.overturetool.vdmj.values.ObjectValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

objectReference

int objectReference

type

ClassType type

members

NameValuePairMap members

superobjects

java.util.List<E> superobjects

CPU

CPUValue CPU

inToString

boolean inToString

mycopy

ObjectValue mycopy

Class org.overturetool.vdmj.values.OperationValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

expldef

ExplicitOperationDefinition expldef

impldef

ImplicitOperationDefinition impldef

name

LexNameToken name

type

OperationType type

paramPatterns

PatternList paramPatterns

body

Statement body

precondition

FunctionValue precondition

postcondition

FunctionValue postcondition

state

StateDefinition state

classdef

ClassDefinition classdef

stateName

LexNameToken stateName

stateContext

Context stateContext

self

ObjectValue self

isConstructor

boolean isConstructor

isStatic

boolean isStatic

isAsync

boolean isAsync

guard

Expression guard

hashAct

int hashAct

hashFin

int hashFin

hashReq

int hashReq

priority

long priority

traceRT

boolean traceRT

Class org.overturetool.vdmj.values.ParameterValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

type

Type type

Class org.overturetool.vdmj.values.QuantifierList extends java.util.Vector<Quantifier> implements Serializable

Serialized Fields

count

int count

size

int[] size

next

int[] next

result

NameValuePairList result

done

boolean done

Class org.overturetool.vdmj.values.QuoteValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

value

java.lang.String value

Class org.overturetool.vdmj.values.RationalValue extends RealValue implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.RealValue extends NumericValue implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.RecordValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

type

RecordType type

fieldmap

FieldMap fieldmap

invariant

FunctionValue invariant

Class org.overturetool.vdmj.values.ReferenceValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

value

Value value

Class org.overturetool.vdmj.values.SeqValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

values

ValueList values

Class org.overturetool.vdmj.values.SetValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

values

ValueSet values

Class org.overturetool.vdmj.values.TokenValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

value

Value value

hash

int hash

Class org.overturetool.vdmj.values.TupleValue extends Value implements Serializable

serialVersionUID: 1L

Serialized Fields

values

ValueList values

Class org.overturetool.vdmj.values.UndefinedValue extends Value implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.UpdatableValue extends ReferenceValue implements Serializable

serialVersionUID: 1L

Serialized Fields

listener

ValueListener listener

Class org.overturetool.vdmj.values.Value extends java.lang.Object implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.ValueList extends java.util.Vector<Value> implements Serializable

Class org.overturetool.vdmj.values.ValueMap extends java.util.HashMap<Value,Value> implements Serializable

Class org.overturetool.vdmj.values.ValueSet extends java.util.Vector<Value> implements Serializable

Class org.overturetool.vdmj.values.VoidReturnValue extends VoidValue implements Serializable

serialVersionUID: 1L

Class org.overturetool.vdmj.values.VoidValue extends Value implements Serializable

serialVersionUID: 1L