de.uka.ilkd.key.proof.init

Interface ProofOblInput

All Known Subinterfaces:

ContractPO, InfFlowCompositePO, InfFlowLeafPO, InfFlowPO, IPersistablePO

All Known Implementing Classes:

AbstractInfFlowPO, AbstractOperationPO, AbstractPO, BlockExecutionPO, DependencyContractPO, FunctionalBlockContractPO, FunctionalLoopContractPO, FunctionalOperationContractPO, InfFlowContractPO, KeYUserProblemFile, LoopInvExecutionPO, ProgramMethodPO, ProgramMethodSubsetPO, ProofStarter.UserProvidedInput, SymbolicExecutionPO, TacletProofObligationInput, WellDefinednessPO

public interface ProofOblInput

Represents something that produces an input proof obligation for the prover. A .key file or a proof obligation generated from a CASE tool may be instances.

Method Summary

Modifier and Type	Method and Description
KeYJavaType	getContainerType() Returns the KeYJavaType in which the proven element is contained in.
ProofAggregate	getPO() Returns the proof obligation term as result of the proof obligation input.
boolean	implies(ProofOblInput po) If true, then this PO implies the passed one.
java.lang.String	name() Returns the name of the proof obligation input.
void	readProblem()

Method Detail

name

java.lang.String name()

Returns the name of the proof obligation input.

readProblem

void readProblem()
          throws ProofInputException

Throws:

ProofInputException

getPO

ProofAggregate getPO()
              throws ProofInputException

Returns the proof obligation term as result of the proof obligation input. If there is still no input available because nothing has been read yet null is returned.

Throws:

ProofInputException

implies

boolean implies(ProofOblInput po)

If true, then this PO implies the passed one.

getContainerType

KeYJavaType getContainerType()

Returns the KeYJavaType in which the proven element is contained in.

Returns:

The KeYJavaType in which the proven element is contained in or null if not available.