| java.lang.Object de.uka.ilkd.key.proof.mgt.AbstractContract de.uka.ilkd.key.proof.mgt.DefaultOperationContract
All known Subclasses: de.uka.ilkd.key.proof.mgt.DLMethodContract, de.uka.ilkd.key.proof.mgt.JMLMethodContract,
Method Summary | |
abstract protected Term | getAdditionalAxioms() | abstract public CatchAllStatement | getCatchAllStatement() | public InstantiatedMethodContract | instantiate(MethodContractInstantiation insts, Proof proof) | abstract protected void | instantiateAtPreSymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables) | abstract protected void | instantiateAuxiliarySymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables, Services services) | protected ProgramVariable | instantiateCatchAllStatement(CatchAllStatement ca, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables, Services services) | abstract protected void | instantiateMethodParameters(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables) | abstract protected void | instantiateMethodReceiver(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables) | abstract protected void | instantiateMethodReturnVariable(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables) |
getAdditionalAxioms | abstract protected Term getAdditionalAxioms()(Code) | | |
instantiateAtPreSymbols | abstract protected void instantiateAtPreSymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | | |
instantiateAuxiliarySymbols | abstract protected void instantiateAuxiliarySymbols(Map replacementMap, Namespace localFunctions, Namespace localProgramVariables, Services services)(Code) | | |
instantiateMethodParameters | abstract protected void instantiateMethodParameters(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | | Parameters: insts - Parameters: replacementMap - Parameters: localProgramVariables - Parameters: localFunctions - |
instantiateMethodReceiver | abstract protected void instantiateMethodReceiver(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | | Parameters: insts - Parameters: replacementMap - Parameters: localProgramVariables - Parameters: localFunctions - |
instantiateMethodReturnVariable | abstract protected void instantiateMethodReturnVariable(MethodContractInstantiation insts, Map replacementMap, Namespace localFunctions, Namespace localProgramVariables)(Code) | | Parameters: insts - Parameters: replacementMap - Parameters: localProgramVariables - Parameters: localFunctions - |
|
|