| java.lang.Object
 de.uka.ilkd.key.rule.UseMethodContractRule
All known Subclasses: de.uka.ilkd.key.unittest.UseMethodContractRuleForTestGen,
| UseMethodContractRule | | public class UseMethodContractRule implements BuiltInRule(Code) | | implements the rule which inserts method contracts for a method body
statement
author:
andreas |
| Inner Class :protected static class MbsInfo | |
| Method Summary | |
| public ListOfGoal | apply(Goal goal, Services services, RuleApp ruleApp)
the rule is applied based on the information of the given rule application:
if the given rule application is a
MethodContractRuleApp then the contained method contract is applied,
otherwise a contract is selected based on the
AutomatedContractConfigurator . | | public String | displayName()
| | protected Term | excPostFma(InstantiatedMethodContract iCt, MbsInfo mbsPos, UpdateFactory uf, Update u, Services services)
| | protected String | getExceptionalLabel()
| | protected String | getPostLabel()
| | protected String | getPreLabel()
| | public boolean | isApplicable(Goal goal, PosInOccurrence pos, Constraint userConstraint)
returns true iff this rule is applicable at the given position, that is,
if there is a contract applicable for a method body statement at that
position in the specification repository belonging to the proof of the
given goal. | | public Name | name()
| | protected Term | postFma(InstantiatedMethodContract iCt, MbsInfo mbsPos, UpdateFactory uf, Update u, Services services)
| | protected Term | preFma(InstantiatedMethodContract iCt, MbsInfo mbsPos, UpdateFactory uf, Update u, Services services)
| | protected NonTerminalProgramElement | replaceStatement(JavaNonTerminalProgramElement all, MbsInfo mbsPos, StatementBlock with)
| | public OldOperationContract | selectContract(Proof proof, PosInOccurrence pos, ContractConfigurator cc)
calls the given contract configurator and returns the selected contract
or creates a new DLMethodContract from the results of the
configuration. | | public OldOperationContract | selectExistingContract(Services services, PosInOccurrence pos, ContractConfigurator cc)
calls the given contract configurator and returns the selected contract
or creates a new DLMethodContract from the results of the
configuration. | | public String | toString()
|
| UseMethodContractRule | | protected UseMethodContractRule()(Code) | | |
| apply | | public ListOfGoal apply(Goal goal, Services services, RuleApp ruleApp)(Code) | | the rule is applied based on the information of the given rule application:
if the given rule application is a
MethodContractRuleApp then the contained method contract is applied,
otherwise a contract is selected based on the
AutomatedContractConfigurator .
Parameters:
goal - the goal that the rule application should refer to
Parameters:
services - the Services with the necessary information about the java programs
Parameters:
ruleApp - the rule application that is executed. |
| displayName | | public String displayName()(Code) | | returns the display name of this rule
|
| getExceptionalLabel | | protected String getExceptionalLabel()(Code) | | |
| isApplicable | | public boolean isApplicable(Goal goal, PosInOccurrence pos, Constraint userConstraint)(Code) | | returns true iff this rule is applicable at the given position, that is,
if there is a contract applicable for a method body statement at that
position in the specification repository belonging to the proof of the
given goal. This does not necessarily mean that a rule application will
change the goal (this decision is made due to performance reasons)
|
| name | | public Name name()(Code) | | returns the name of this rule
|
| selectContract | | public OldOperationContract selectContract(Proof proof, PosInOccurrence pos, ContractConfigurator cc)(Code) | | calls the given contract configurator and returns the selected contract
or creates a new DLMethodContract from the results of the
configuration. The selected / configured contract suits to the given
position. It is added to the proof environment of the given proof.
|
| selectExistingContract | | public OldOperationContract selectExistingContract(Services services, PosInOccurrence pos, ContractConfigurator cc)(Code) | | calls the given contract configurator and returns the selected contract
or creates a new DLMethodContract from the results of the
configuration. The selected / configured contract suits to the given
position. It is added to the proof environment of the given proof.
|
|
|