| java.lang.Object
 de.uka.ilkd.key.proof.mgt.AbstractContract
de.uka.ilkd.key.proof.mgt.DefaultOperationContract
de.uka.ilkd.key.proof.mgt.DLMethodContract
| DLMethodContract | | public class DLMethodContract extends DefaultOperationContract (Code) | | represents a contract on the DynamicLogic level, that is pre-condition,
program, post-condition, and modifies clause. It is the starting point to
create both proof obligation (to ensure that the contract is valid) as well
as a taclet (that allows to use the contract in a proof). DLMethodContracts
are created from UserKeYProblemFiles using the \contract section. Moreover
they are created when a contract of another input like JML or OCL is
configured.
|
| Constructor Summary | |
| public | DLMethodContract(Term fma, SetOfLocationDescriptor modifies, String name, String displayName, Services services, NamespaceSet namespaces)
| | public | DLMethodContract(Term pre, Term post, Term extraPre, Collection atPreFunctions, Statement mbs, SetOfLocationDescriptor modifies, Modality modality, String name, String displayName, Services services, NamespaceSet namespaces)
Creates a DLMethodContract with separate parts and possible additional
preconditions which are not to be proven in the precondition branch of
the created proof. |
| Method Summary | |
| public void | addPost(Term t)
| | public void | addPre(Term t)
| | public boolean | applicableForModality(Modality mod)
| | public DLMethodContract | copy()
| | public DLMethodContract | createDLMethodContract(Proof proof)
| | public String | createProgramVarsSection()
| | public boolean | equals(Object cmp)
| | protected Term | getAdditionalAxioms()
| | public CatchAllStatement | getCatchAllStatement()
| | public String | getHTMLText()
| | public String | getHeader()
| | public MethodBodyStatement | getMethodBodyStatement()
| | public Modality | getModality()
| | public ModelMethod | getModelMethod()
| | public SetOfLocationDescriptor | getModifies()
| | public String | getModifiesText()
| | public String | getName()
| | public Object | getObjectOfContract()
returns the object on which this contract is, in this case it is the
program statement of the contract; or in case that this is a method body
statement the according program method is returned. | | public Term | getPost()
| | public String | getPostText()
| | public Term | getPre()
| | public String | getPreText()
| | public ProgramMethod | getProgramMethod()
| | public Namespace | getProgramVariables()
| | public ProofOblInput | getProofOblInput(Proof proof)
returns a proof obligation input needed to show the corretcness of this
contract. | | public Statement | getStatement()
| | public int | hashCode()
| | protected void | instantiateAtPreSymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)
| | protected void | instantiateAuxiliarySymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables, Services services)
| | protected void | instantiateMethodParameters(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)
| | protected void | instantiateMethodReceiver(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)
| | protected void | instantiateMethodReturnVariable(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)
| | public void | setHeader(String s)
| | public String | toString()
| | static Statement | unwrapBlocks(Statement s, boolean stopAtCatchAll)
|
| DLMethodContract | | public DLMethodContract(Term fma, SetOfLocationDescriptor modifies, String name, String displayName, Services services, NamespaceSet namespaces)(Code) | | Creates a DLMethodContract with one implication formula of the form
pre -> \ post and a modifies clause
Parameters:
fma - the implication formula
Parameters:
modifies - a set of location descriptors defining the modifies clause forthis DLMethodContract
Parameters:
name - a unique identifying name for a contract in the proof
Parameters:
displayName - the name displayed for this contract
Parameters:
services - the services object
Parameters:
namespaces - the namespaces for looking up atpre functions |
| DLMethodContract | | public DLMethodContract(Term pre, Term post, Term extraPre, Collection atPreFunctions, Statement mbs, SetOfLocationDescriptor modifies, Modality modality, String name, String displayName, Services services, NamespaceSet namespaces)(Code) | | Creates a DLMethodContract with separate parts and possible additional
preconditions which are not to be proven in the precondition branch of
the created proof.
Parameters:
pre - the precondition of the contract
Parameters:
post - the postcondition of the contract
Parameters:
extraPre - the additional preconditions
Parameters:
atPreFunctions - a Collection with all functions used to model @pre for function symbols
Parameters:
mbs - the statement of the proof, either this is a method bodystatement or a catch all statement
Parameters:
modifies - a set of location descriptors defining the modifies clause forthis DLMethodContract
Parameters:
name - a unique identifying name for a contract in the proof
Parameters:
displayName - the name displayed for this contract
Parameters:
services - the services object
Parameters:
namespaces - the namespaces for looking up atpre functions |
| applicableForModality | | public boolean applicableForModality(Modality mod)(Code) | | |
| createProgramVarsSection | | public String createProgramVarsSection()(Code) | | |
| getAdditionalAxioms | | protected Term getAdditionalAxioms()(Code) | | |
| getModifies | | public SetOfLocationDescriptor getModifies()(Code) | | |
| getObjectOfContract | | public Object getObjectOfContract()(Code) | | returns the object on which this contract is, in this case it is the
program statement of the contract; or in case that this is a method body
statement the according program method is returned.
|
| getProofOblInput | | public ProofOblInput getProofOblInput(Proof proof)(Code) | | returns a proof obligation input needed to show the corretcness of this
contract.
|
| hashCode | | public int hashCode()(Code) | | |
| instantiateAtPreSymbols | | protected void instantiateAtPreSymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | |
Parameters:
replacementMap -
Parameters:
localFunctions -
Parameters:
localProgramVariables - |
| instantiateMethodParameters | | protected void instantiateMethodParameters(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | |
Parameters:
insts -
Parameters:
replacementMap -
Parameters:
localProgramVariables -
Parameters:
localFunctions - |
| instantiateMethodReceiver | | protected void instantiateMethodReceiver(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | |
Parameters:
insts -
Parameters:
replacementMap -
Parameters:
localProgramVariables -
Parameters:
localFunctions - |
| instantiateMethodReturnVariable | | protected void instantiateMethodReturnVariable(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | |
Parameters:
insts -
Parameters:
replacementMap -
Parameters:
localProgramVariables -
Parameters:
localFunctions - |
| Methods inherited from de.uka.ilkd.key.proof.mgt.DefaultOperationContract | abstract protected Term getAdditionalAxioms()(Code)(Java Doc)
abstract public CatchAllStatement getCatchAllStatement()(Code)(Java Doc)
public InstantiatedMethodContract instantiate(MethodContractInstantiation insts, Proof proof)(Code)(Java Doc)
abstract protected void instantiateAtPreSymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code)(Java Doc)
abstract protected void instantiateAuxiliarySymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables, Services services)(Code)(Java Doc)
protected ProgramVariable instantiateCatchAllStatement(CatchAllStatement ca, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables, Services services)(Code)(Java Doc)
abstract protected void instantiateMethodParameters(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code)(Java Doc)
abstract protected void instantiateMethodReceiver(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code)(Java Doc)
abstract protected void instantiateMethodReturnVariable(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code)(Java Doc)
|
|
|