org.overturetool.vdmj.statements
Class CallObjectStatement

java.lang.Object
  org.overturetool.vdmj.statements.Statement
      org.overturetool.vdmj.statements.CallObjectStatement

All Implemented Interfaces:

java.io.Serializable

public class CallObjectStatement
extends Statement

See Also:

Serialized Form

Field Summary

ExpressionList	args
java.lang.String	classname
ObjectDesignator	designator
boolean	explicit
java.lang.String	fieldname

Fields inherited from class org.overturetool.vdmj.statements.Statement

breakpoint, location

Constructor Summary

CallObjectStatement(ObjectDesignator designator, java.lang.String classname, java.lang.String fieldname, ExpressionList args)

Method Summary

Value	eval(Context ctxt) Evaluate the statement in the context given.
TypeSet	exitCheck() Return a list of exit types which can be thrown by the statement.
Expression	findExpression(int lineno)
ProofObligationList	getProofObligations(POContextStack ctxt) Get a list of proof obligations from the statement.
java.lang.String	kind() A string name of the statement type, (eg "if").
java.lang.String	toString()
Type	typeCheck(Environment env, NameScope scope) Type check the statement and return its type.

Methods inherited from class org.overturetool.vdmj.statements.Statement

abort, abort, detail, detail2, findStatement, hasSideEffects, report, warning

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

designator

public final ObjectDesignator designator

classname

public java.lang.String classname

fieldname

public final java.lang.String fieldname

args

public final ExpressionList args

explicit

public final boolean explicit

Constructor Detail

CallObjectStatement

public CallObjectStatement(ObjectDesignator designator,
                           java.lang.String classname,
                           java.lang.String fieldname,
                           ExpressionList args)

Method Detail

toString

public java.lang.String toString()

Specified by:

toString in class Statement

kind

public java.lang.String kind()

Description copied from class: Statement

A string name of the statement type, (eg "if").

Specified by:

kind in class Statement

typeCheck

public Type typeCheck(Environment env,
                      NameScope scope)

Description copied from class: Statement

Type check the statement and return its type.

Specified by:

typeCheck in class Statement

exitCheck

public TypeSet exitCheck()

Description copied from class: Statement

Return a list of exit types which can be thrown by the statement.

Overrides:

exitCheck in class Statement

Returns:

A possibly empty list of exit types.

eval

public Value eval(Context ctxt)

Description copied from class: Statement

Evaluate the statement in the context given.

Specified by:

eval in class Statement

findExpression

public Expression findExpression(int lineno)

Overrides:

findExpression in class Statement

getProofObligations

public ProofObligationList getProofObligations(POContextStack ctxt)

Description copied from class: Statement

Get a list of proof obligations from the statement.

Overrides:

getProofObligations in class Statement

Parameters:

ctxt - The call context.

Returns:

The list of proof obligations.