| java.lang.Object
 de.uka.ilkd.key.proof.mgt.DLHoareTriplePO
| DLHoareTriplePO | | public class DLHoareTriplePO implements ProofOblInput(Code) | | represents a proof obligation input to the prover for a DLMethodContract
|
| askUserForEnvironment | | public boolean askUserForEnvironment()(Code) | | |
| getJavaPath | | public String getJavaPath()(Code) | | returns the path to the Java model.
|
| getObjectOfContract | | public Contractable[] getObjectOfContract()(Code) | | returns the object for which this proof obligation proves a contract on.
In this case we assume that the first program element of the second
subterm of the
proof obligation is a method body statement of which the according program
method is returned.
|
| getPO | | public ProofAggregate getPO()(Code) | | 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.
|
| initContract | | public boolean initContract(Contract ct)(Code) | | initialises the contract, that is, it adds the proof created by this PO input
to the contract if the given contract is the same as that of the PO. Then true
is returned. Otherwise nothing is done and false is returned.
|
| name | | public String name()(Code) | | returns the name of the proof obligation input.
|
| readProblem | | public void readProblem(ModStrategy mod) throws ProofInputException(Code) | | starts reading the input and modifies the InitConfig of this
object with respect to the given modification
strategy.
|
| readSpecs | | public void readSpecs()(Code) | | |
| setInitConfig | | public void setInitConfig(InitConfig i)(Code) | | set the initial configuration used to read an input. It may become
modified during reading depending on the modification strategy used
for reading.
|
| startProtocol | | public void startProtocol()(Code) | | |
|
|