org.overturetool.vdmj.definitions
Class PerSyncDefinition

java.lang.Object
  org.overturetool.vdmj.definitions.Definition
      org.overturetool.vdmj.definitions.PerSyncDefinition

All Implemented Interfaces:

java.io.Serializable

public class PerSyncDefinition
extends Definition

See Also:

Serialized Form

Field Summary

Expression	guard
LexNameToken	opname

Fields inherited from class org.overturetool.vdmj.definitions.Definition

accessSpecifier, classDefinition, location, name, nameScope, pass, used

Constructor Summary

PerSyncDefinition(LexLocation location, LexNameToken opname, Expression guard)

Method Summary

Definition	findName(LexNameToken sought, NameScope scope) Find whether this Definition contains a definition of a name.
DefinitionList	getDefinitions() Return a list of all the definitions created by this definition.
Expression	getExpression()
Type	getType() Return the static type of the definition.
LexNameList	getVariableNames() Return a list of variable names that would be defined by the definition.
java.lang.String	kind() A string with the informal kind of the definition, like "operation".
java.lang.String	toString()
void	typeCheck(Environment base, NameScope scope) Perform a static type check of this definition.

Methods inherited from class org.overturetool.vdmj.definitions.Definition

abort, abort, abort, detail, detail2, equals, findExpression, findStatement, findType, getNamedValues, getProofObligations, getSelfDefinition, hashCode, implicitDefinitions, isAccess, isCallableOperation, isFunctionOrOperation, isInstanceVariable, isRuntime, isStatic, isTypeDefinition, isValueDefinition, markUsed, report, setAccessSpecifier, setClassDefinition, typeResolve, unusedCheck, warning

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

opname

public final LexNameToken opname

guard

public final Expression guard

Constructor Detail

PerSyncDefinition

public PerSyncDefinition(LexLocation location,
                         LexNameToken opname,
                         Expression guard)

Method Detail

getDefinitions

public DefinitionList getDefinitions()

Description copied from class: Definition

Return a list of all the definitions created by this definition. A definition may create lower level definitions if it defines more than one "name" which can be used in its scope. For example, a function may define pre and post conditions, which cause implicit functions to be defined in addition to the main definition for the function itself.

Specified by:

getDefinitions in class Definition

Returns:

A list of definitions.

getType

public Type getType()

Description copied from class: Definition

Return the static type of the definition. For example, the type of a function or operation definition would be its parameter/result signature; the type of a value definition would be that value's type; the type of a type definition is the underlying type being defined.

Note that for Definitions which define multiple inner definitions (see Definition.getDefinitions()), this method returns the primary type - eg. the type of a function, not the types of its pre/post definitions.

Specified by:

getType in class Definition

Returns:

The primary type of this definition.

getVariableNames

public LexNameList getVariableNames()

Description copied from class: Definition

Return a list of variable names that would be defined by the definition.

Specified by:

getVariableNames in class Definition

kind

public java.lang.String kind()

Description copied from class: Definition

A string with the informal kind of the definition, like "operation".

Specified by:

kind in class Definition

toString

public java.lang.String toString()

Specified by:

toString in class Definition

findName

public Definition findName(LexNameToken sought,
                           NameScope scope)

Description copied from class: Definition

Find whether this Definition contains a definition of a name. Since some definitions contain inner definitions (eg. function definitions contain further definitions for their pre and post conditions), this cannot in general compare the name passed with the name of this object. This method is used for finding Definitions that are not types. That can include constants, functions, operations and state definitions. The TypeDefinition implementation of this method checks for any type invariant function definition that it has created, but does not return a match for the name of the type itself. The findType method is used for this. The implementation in the base class compares the name with this.name, setting the "used" flag if the names match. Subclasses perform a similar check on any extra definitions they have created. Definitions which include state fields are sometimes in scope (from within operation bodies) and sometimes not (in function bodies). So the scope parameter is used to indicate what sorts of definitions should be considered in the lookup. The StateDefinition subclass uses this to decide whether to consider its state definitions as in scope.

Overrides:

findName in class Definition

Parameters:

sought - The name of the definition sought.

scope - The sorts of definitions which may be considered.

Returns:

A definition object, or null if not found.

typeCheck

public void typeCheck(Environment base,
                      NameScope scope)

Description copied from class: Definition

Perform a static type check of this definition. The actions performed depend on the type of definition and are entirely defined in the subclass. The type checker is passed an Environment object which contains a list of other definitions, and a scope which indicates what sort of names from the environment can be used (state etc).

Specified by:

typeCheck in class Definition

Parameters:

base - Named definitions potentially in scope

scope - The types of names in scope

getExpression

public Expression getExpression()