org.overturetool.vdmj.pog
Class FuncPostConditionObligation

java.lang.Object
  org.overturetool.vdmj.pog.ProofObligation
      org.overturetool.vdmj.pog.FuncPostConditionObligation

public class FuncPostConditionObligation
extends ProofObligation

Field Summary

Fields inherited from class org.overturetool.vdmj.pog.ProofObligation

kind, location, name, value

Constructor Summary

FuncPostConditionObligation(ExplicitFunctionDefinition func, POContextStack ctxt)

FuncPostConditionObligation(ImplicitFunctionDefinition func, POContextStack ctxt)

Method Summary

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

getValue, getVar, toString

Methods inherited from class java.lang.Object

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

Constructor Detail

FuncPostConditionObligation

public FuncPostConditionObligation(ExplicitFunctionDefinition func,
                                   POContextStack ctxt)

FuncPostConditionObligation

public FuncPostConditionObligation(ImplicitFunctionDefinition func,
                                   POContextStack ctxt)