| java.lang.Object de.uka.ilkd.key.rule.BuiltInRuleApp
All known Subclasses: de.uka.ilkd.key.rule.MethodContractRuleApp,
BuiltInRuleApp | public class BuiltInRuleApp implements RuleApp(Code) | | this class represents an application of a built in rule
application
|
complete | public boolean complete()(Code) | | returns true if all variables are instantiated
true if all variables are instantiated |
constraint | public Constraint constraint()(Code) | | returns the constraint under which a rule is applicable
|
execute | public ListOfGoal execute(Goal goal, Services services)(Code) | | applies the specified rule at the specified position
if all schema variables have been instantiated
Parameters: goal - the Goal where to apply the rule Parameters: services - the Services encapsulating all java information list of new created goals |
posInOccurrence | public PosInOccurrence posInOccurrence()(Code) | | returns the PositionInOccurrence (representing a ConstrainedFormula and
a position in the corresponding formula) of this rule application
|
rule | public Rule rule()(Code) | | returns the rule of this rule application
|
userConstraint | public Constraint userConstraint()(Code) | | returns the user constraint
|
|
|