org.overturetool.vdmj.expressions
Class PlusPlusExpression

java.lang.Object
  org.overturetool.vdmj.expressions.Expression
      org.overturetool.vdmj.expressions.BinaryExpression
          org.overturetool.vdmj.expressions.PlusPlusExpression

All Implemented Interfaces:

java.io.Serializable

public class PlusPlusExpression
extends BinaryExpression

See Also:

Serialized Form

Field Summary

Fields inherited from class org.overturetool.vdmj.expressions.BinaryExpression

left, ltype, op, right, rtype

Fields inherited from class org.overturetool.vdmj.expressions.Expression

breakpoint, location

Constructor Summary

PlusPlusExpression(Expression left, LexToken op, Expression right)

Method Summary

Value	eval(Context ctxt) Evaluate the expression in the given runtime context.
ProofObligationList	getProofObligations(POContextStack ctxt) Get a list of proof obligations from the expression.
java.lang.String	kind() A short descriptive string for the expression.
Type	typeCheck(Environment env, TypeList qualifiers, NameScope scope) Perform a type check of the expression.

Methods inherited from class org.overturetool.vdmj.expressions.BinaryExpression

binaryCheck, findExpression, toString

Methods inherited from class org.overturetool.vdmj.expressions.Expression

abort, abort, concern, detail, detail, detail2, detail2, getPreName, report, warning

Methods inherited from class java.lang.Object

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

Constructor Detail

PlusPlusExpression

public PlusPlusExpression(Expression left,
                          LexToken op,
                          Expression right)

Method Detail

typeCheck

public Type typeCheck(Environment env,
                      TypeList qualifiers,
                      NameScope scope)

Description copied from class: Expression

Perform a type check of the expression. The method returns the Type of the expression it checked, and is used recursively across an expression tree. For example, a boolean "and" expression would type check its left and right hand sides, check that the types returned were both compatible with BooleanType and then return a BooleanType (regardless of any errors).

The qualifiers argument is passed when checking function and operation application. It contains the list of argument types of the application, and is used to choose between overloaded function/operation definitions.

Specified by:

typeCheck in class Expression

Parameters:

env - The static environment for resolving names.

qualifiers - The argument type qualifiers for overloading.

scope - The scope of applicable names from the environment.

Returns:

The type of the expression.

eval

public Value eval(Context ctxt)

Description copied from class: Expression

Evaluate the expression in the given runtime context. The Value object returned can hold any type of value (int, bool, sequences, sets etc).

Specified by:

eval in class Expression

Parameters:

ctxt - The context in which to evaluate the expression.

Returns:

The value of the expression.

getProofObligations

public ProofObligationList getProofObligations(POContextStack ctxt)

Description copied from class: Expression

Get a list of proof obligations from the expression.

Overrides:

getProofObligations in class BinaryExpression

Parameters:

ctxt - The call context.

Returns:

The list of proof obligations.

kind

public java.lang.String kind()

Description copied from class: Expression

A short descriptive string for the expression. An example would be "forall" or "map comprehension".

Specified by:

kind in class Expression

Returns:

A short name for the expression.