public interface ProofOblInput
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() |
java.lang.String name()
void readProblem() throws ProofInputException
ProofInputException
ProofAggregate getPO() throws ProofInputException
ProofInputException
boolean implies(ProofOblInput po)
KeYJavaType getContainerType()
KeYJavaType
in which the proven element is contained in.KeYJavaType
in which the proven element is contained in or null
if not available.