org.overturetool.vdmj.pog
Class ProofObligation

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

Direct Known Subclasses:

CasesExhaustiveObligation, FiniteMapObligation, FiniteSetObligation, FuncComposeObligation, FuncIterationObligation, FuncPostConditionObligation, FunctionApplyObligation, InvariantObligation, LetBeExistsObligation, MapApplyObligation, MapCompatibleObligation, MapComposeObligation, MapIterationObligation, MapSeqOfCompatibleObligation, MapSetOfCompatibleObligation, NonEmptySeqObligation, NonEmptySetObligation, NonZeroObligation, OperationPostConditionObligation, ParameterPatternObligation, RecursiveObligation, SatisfiabilityObligation, SeqApplyObligation, SeqModificationObligation, StateInvariantObligation, SubTypeObligation, TupleSelectObligation, UniqueExistenceObligation, ValueBindingObligation, WhileLoopObligation

public abstract class ProofObligation
extends java.lang.Object

Field Summary

POType	kind
LexLocation	location
java.lang.String	name
java.lang.String	value

Constructor Summary

ProofObligation(LexLocation location, POType kind, POContextStack ctxt)

Method Summary

java.lang.String	getValue()
protected java.lang.String	getVar(java.lang.String root)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

location

public final LexLocation location

kind

public final POType kind

name

public final java.lang.String name

value

public java.lang.String value

Constructor Detail

ProofObligation

public ProofObligation(LexLocation location,
                       POType kind,
                       POContextStack ctxt)

Method Detail

getValue

public java.lang.String getValue()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getVar

protected java.lang.String getVar(java.lang.String root)