org.overturetool.vdmj.expressions
Class UnaryExpression

java.lang.Object
  org.overturetool.vdmj.expressions.Expression
      org.overturetool.vdmj.expressions.UnaryExpression

All Implemented Interfaces:

java.io.Serializable

Direct Known Subclasses:

AbsoluteExpression, CardinalityExpression, DistConcatExpression, DistIntersectExpression, DistMergeExpression, DistUnionExpression, FloorExpression, HeadExpression, IndicesExpression, LenExpression, MapDomainExpression, MapInverseExpression, MapRangeExpression, NotExpression, PowerSetExpression, ReverseExpression, TailExpression, UnaryMinusExpression, UnaryPlusExpression

public abstract class UnaryExpression
extends Expression

See Also:

Serialized Form

Field Summary

Expression

exp

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

breakpoint, location

Constructor Summary

UnaryExpression(LexLocation location, Expression exp)

Method Summary

Expression	findExpression(int lineno) Find an expression starting on the given line.
ProofObligationList	getProofObligations(POContextStack ctxt) Get a list of proof obligations from the expression.

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

abort, abort, concern, detail, detail, detail2, detail2, eval, getPreName, kind, report, toString, typeCheck, warning

Methods inherited from class java.lang.Object

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

Field Detail

exp

public final Expression exp

Constructor Detail

UnaryExpression

public UnaryExpression(LexLocation location,
                       Expression exp)

Method Detail

findExpression

public Expression findExpression(int lineno)

Description copied from class: Expression

Find an expression starting on the given line. Single expressions just compare their location to lineno, but expressions with sub-expressions iterate over their branches.

Overrides:

findExpression in class Expression

Parameters:

lineno - The line number to locate.

Returns:

An expression starting on the line, or null.

getProofObligations

public ProofObligationList getProofObligations(POContextStack ctxt)

Description copied from class: Expression

Get a list of proof obligations from the expression.

Overrides:

getProofObligations in class Expression

Parameters:

ctxt - The call context.

Returns:

The list of proof obligations.