| de.uka.ilkd.key.proof.init.ProofOblInput
All known Subclasses: de.uka.ilkd.key.proof.init.NonInterferencePO, de.uka.ilkd.key.proof.init.KeYUserProblemFile, de.uka.ilkd.key.proof.init.AbstractPO, de.uka.ilkd.key.proof.init.TacletSoundnessPO, de.uka.ilkd.key.proof.init.ModifiesCheckProofOblInput, de.uka.ilkd.key.visualdebugger.DebuggerPO, de.uka.ilkd.key.proof.init.OCLProofOblInput, de.uka.ilkd.key.proof.mgt.DLHoareTriplePO, de.uka.ilkd.key.proof.init.JavaInput,
| ProofOblInput | | public interface ProofOblInput (Code) | | 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. An instance can be called to set an initial configuration,
that is modified during reading the input (using setInitConfig),
to get the read proof
obligation (using getProblemTerm). During reading the input
given initial configuration may become modified. The modification
can be controlled by a modification strategy.
|
| askUserForEnvironment | | boolean askUserForEnvironment()(Code) | | |
| getPO | | 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.
|
| name | | String name()(Code) | | returns the name of the proof obligation input.
|
| readSpecs | | void readSpecs()(Code) | | |
| setInitConfig | | void setInitConfig(InitConfig i)(Code) | | Set the initial configuration used to read the input. It may become
modified during reading depending on the modification strategy used
for reading. Must be called before calling any of the read* methods.
|
|
|