jml2b.pog.proofobligation
Class ProofObligation

java.lang.Object
  jml2b.util.Profiler
      jml2b.pog.proofobligation.ProofObligation

Direct Known Subclasses:

SourceProofObligation

public abstract class ProofObligation

extends Profiler

This abstract class describes a proof obligation and facilities to calculate them.

Author:

L. Burdy

Constructor Summary

ProofObligation()

Method Summary

abstract java.lang.String	getDisplayedName()
abstract void	pog(IJml2bConfiguration config) Process the WP calculus on the proof obligations.
abstract void	proveObvious(boolean prove) Proves the obvious goals if asked.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

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

Constructor Detail

ProofObligation

public ProofObligation()

Method Detail

pog

public abstract void pog(IJml2bConfiguration config)
                  throws Jml2bException,
                         PogException

Process the WP calculus on the proof obligations.

Parameters:

config - The current configuration

Throws:

PogException

Jml2bException

proveObvious

public abstract void proveObvious(boolean prove)

Proves the obvious goals if asked. Cast all the remaining lemmas in SimpleLemma. This task is performed at the end of the WP calculus.

Parameters:

prove - indicate whether obvious goals should be suppressed from the theorems

getDisplayedName

public abstract java.lang.String getDisplayedName()

Returns:

the name to display in the progress monitor.