| |
|
| java.lang.Object de.uka.ilkd.key.proof.init.ModifiesCheckProofOblInput
All known Subclasses: de.uka.ilkd.key.proof.init.AssignableCheckProofOblInput,
ModifiesCheckProofOblInput | public class ModifiesCheckProofOblInput implements ProofOblInput(Code) | | represents a proof obligation originating from a given Modifies Clause
as input for the prover.
|
Constructor Summary | |
public | ModifiesCheckProofOblInput(String name, ModelMethod aMethRepr) creates a new representation of a proof obligation from a Modifies
Clause with the given name, originating from a representation of a model
method and having the given String as text of the Modifies Clause. |
currentClassAttributes | protected Set currentClassAttributes(Code) | | |
modifiesElements | protected SetOfTerm modifiesElements(Code) | | |
occuringClasses | protected Set occuringClasses(Code) | | |
ModifiesCheckProofOblInput | public ModifiesCheckProofOblInput(String name, ModelMethod aMethRepr)(Code) | | creates a new representation of a proof obligation from a Modifies
Clause with the given name, originating from a representation of a model
method and having the given String as text of the Modifies Clause.
The given XMI file name can be used to read the underlying model.
|
askUserForEnvironment | public boolean askUserForEnvironment()(Code) | | returns false, that is the input never asks the user which
environment he prefers
|
createProofStart | protected Term createProofStart()(Code) | | |
getModifiesElements | public SetOfTerm getModifiesElements()(Code) | | |
name | public String name()(Code) | | returns the name of the modifies check proof obligation input.
|
readProblem | public void readProblem(ModStrategy mod)(Code) | | generates the proof obligation
|
readSpecs | public void readSpecs()(Code) | | |
setInitConfig | public void setInitConfig(InitConfig conf)(Code) | | sets the initial configuration that is used to read the OCL
input and that is used to be modified during reading.
|
startProtocol | public void startProtocol()(Code) | | |
|
|
|