| java.lang.Object de.uka.ilkd.key.rule.UseMethodContractRule de.uka.ilkd.key.unittest.UseMethodContractRuleForTestGen
name | public Name name()(Code) | | returns the name of this rule
|
Methods inherited from de.uka.ilkd.key.rule.UseMethodContractRule | public ListOfGoal apply(Goal goal, Services services, RuleApp ruleApp)(Code)(Java Doc) public String displayName()(Code)(Java Doc) protected Term excPostFma(InstantiatedMethodContract iCt, MbsInfo mbsPos, UpdateFactory uf, Update u, Services services)(Code)(Java Doc) protected String getExceptionalLabel()(Code)(Java Doc) protected String getPostLabel()(Code)(Java Doc) protected String getPreLabel()(Code)(Java Doc) public boolean isApplicable(Goal goal, PosInOccurrence pos, Constraint userConstraint)(Code)(Java Doc) public Name name()(Code)(Java Doc) protected Term postFma(InstantiatedMethodContract iCt, MbsInfo mbsPos, UpdateFactory uf, Update u, Services services)(Code)(Java Doc) protected Term preFma(InstantiatedMethodContract iCt, MbsInfo mbsPos, UpdateFactory uf, Update u, Services services)(Code)(Java Doc) protected NonTerminalProgramElement replaceStatement(JavaNonTerminalProgramElement all, MbsInfo mbsPos, StatementBlock with)(Code)(Java Doc) public OldOperationContract selectContract(Proof proof, PosInOccurrence pos, ContractConfigurator cc)(Code)(Java Doc) public OldOperationContract selectExistingContract(Services services, PosInOccurrence pos, ContractConfigurator cc)(Code)(Java Doc) public String toString()(Code)(Java Doc)
|
|
|