org.overturetool.vdmj.pog
Class POFunctionResultContext

java.lang.Object
  org.overturetool.vdmj.pog.POContext
      org.overturetool.vdmj.pog.POFunctionResultContext

public class POFunctionResultContext
extends POContext

Field Summary

Expression	body
FunctionType	deftype
boolean	implicit
LexNameToken	name
Expression	precondition
PatternTypePair	result

Constructor Summary

POFunctionResultContext(ExplicitFunctionDefinition definition)

POFunctionResultContext(ImplicitFunctionDefinition definition)

Method Summary

java.lang.String

getContext()

Methods inherited from class org.overturetool.vdmj.pog.POContext

getName

Methods inherited from class java.lang.Object

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

Field Detail

name

public final LexNameToken name

deftype

public final FunctionType deftype

precondition

public final Expression precondition

body

public final Expression body

result

public final PatternTypePair result

implicit

public final boolean implicit

Constructor Detail

POFunctionResultContext

public POFunctionResultContext(ExplicitFunctionDefinition definition)

POFunctionResultContext

public POFunctionResultContext(ImplicitFunctionDefinition definition)

Method Detail

getContext

public java.lang.String getContext()

Specified by:

getContext in class POContext