| java.lang.Object
 de.uka.ilkd.key.rule.Taclet
de.uka.ilkd.key.rule.NoFindTaclet
| NoFindTaclet | | public class NoFindTaclet extends Taclet (Code) | | Used to implement a Taclet that has no find part. This kind of taclet
is not attached to term or formula, but to a complete sequent. A typical
representant is the cut rule.
|
| Constructor Summary | |
| public | NoFindTaclet(Name name, TacletApplPart applPart, ListOfTacletGoalTemplate goalTemplates, ListOfRuleSet ruleSets, Constraint constraint, TacletAttributes attrs, MapFromSchemaVariableToTacletPrefix prefixMap, SetOfChoice choices)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters. |
| NoFindTaclet | | public NoFindTaclet(Name name, TacletApplPart applPart, ListOfTacletGoalTemplate goalTemplates, ListOfRuleSet ruleSets, Constraint constraint, TacletAttributes attrs, MapFromSchemaVariableToTacletPrefix prefixMap, SetOfChoice choices)(Code) | | creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
Parameters:
name - the name of the Taclet
Parameters:
applPart - contains the application part of an Taclet that isthe if-sequent, the variable conditions
Parameters:
goalTemplates - the ListOfTacletGoalTemplate containg all goal descriptions of the taclet to be created
Parameters:
ruleSets - a list of rule sets for the Taclet
Parameters:
constraint - the Constraint under which the Taclet is valid
Parameters:
attrs - attributes for the Taclet; these are boolean values
Parameters:
prefixMap - a MapFromSchemaVariableToTacletPrefix that contains theprefix for each SchemaVariable in the Taclet
Parameters:
choices - the SetOfChoices to which this taclet belongs to |
| apply | | public ListOfGoal apply(Goal goal, Services services, RuleApp ruleApp)(Code) | | the rule is applied on the given goal using the
information of rule application.
Parameters:
goal - the goal that the rule application should refer to.
Parameters:
services - the Services encapsulating all java information
Parameters:
ruleApp - the taclet application that is executed |
| applyAdd | | protected void applyAdd(Sequent add, Goal goal, Services services, MatchConditions matchCond)(Code) | | adds the sequent of the add part of the Taclet to the goal sequent
Parameters:
add - the Sequent to be added
Parameters:
goal - the Goal to be updated
Parameters:
services - the Services encapsulating all java information
Parameters:
matchCond - the MatchConditions with all required instantiations |
| getBoundVariablesHelper | | protected SetOfQuantifiableVariable getBoundVariablesHelper()(Code) | | the empty set as a no find taclet has no other entities where
variables cann occur bound than in the goal templates
empty set |
| getIfFindVariables | | public SetOfSchemaVariable getIfFindVariables()(Code) | | Set of schemavariables of the if and the (optional)find part |
| Methods inherited from de.uka.ilkd.key.rule.Taclet | protected void addToAntec(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code)(Java Doc)
protected void addToSucc(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code)(Java Doc)
public SetOfSchemaVariable addedRuleNameVars()(Code)(Java Doc)
public boolean admissible(boolean interactive, ListOfRuleSet ruleSets)(Code)(Java Doc)
protected boolean admissibleAutomatic(ListOfRuleSet ruleSets)(Code)(Java Doc)
protected boolean admissibleInteractive(ListOfRuleSet ruleSets)(Code)(Java Doc)
abstract public ListOfGoal apply(Goal goal, Services services, RuleApp tacletApp)(Code)(Java Doc)
protected void applyAddProgVars(SetOfSchemaVariable pvs, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)(Code)(Java Doc)
protected void applyAddrule(ListOfTaclet rules, Goal goal, Services services, MatchConditions matchCond)(Code)(Java Doc)
protected void cacheMatchInfo()(Code)(Java Doc)
public MatchConditions checkConditions(MatchConditions cond, Services services)(Code)(Java Doc)
protected ListOfGoal checkIfGoals(Goal p_goal, ListOfIfFormulaInstantiation p_list, MatchConditions p_matchCond, int p_numberOfNewGoals)(Code)(Java Doc)
public MatchConditions checkVariableConditions(SchemaVariable var, SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services)(Code)(Java Doc)
public boolean closeGoal()(Code)(Java Doc)
public Constraint constraint()(Code)(Java Doc)
public String displayName()(Code)(Java Doc)
public boolean equals(Object o)(Code)(Java Doc)
public SetOfQuantifiableVariable getBoundVariables()(Code)(Java Doc)
abstract protected SetOfQuantifiableVariable getBoundVariablesHelper()(Code)(Java Doc)
public SetOfChoice getChoices()(Code)(Java Doc)
abstract public SetOfSchemaVariable getIfFindVariables()(Code)(Java Doc)
protected SetOfSchemaVariable getIfVariables()(Code)(Java Doc)
public SchemaVariable getNameCorrespondent(SchemaVariable p)(Code)(Java Doc)
public TacletPrefix getPrefix(SchemaVariable sv)(Code)(Java Doc)
public ListOfRuleSet getRuleSets()(Code)(Java Doc)
public IteratorOfVariableCondition getVariableConditions()(Code)(Java Doc)
public ListOfTacletGoalTemplate goalTemplates()(Code)(Java Doc)
public boolean hasReplaceWith()(Code)(Java Doc)
public int hashCode()(Code)(Java Doc)
public String helpText()(Code)(Java Doc)
public Sequent ifSequent()(Code)(Java Doc)
public boolean isContextInPrefix()(Code)(Java Doc)
protected MatchConditions match(Term term, Term template, boolean ignoreUpdates, MatchConditions matchCond, Services services, Constraint userConstraint)(Code)(Java Doc)
protected MatchConditions match(Term term, Term template, MatchConditions matchCond, Services services, Constraint userConstraint)(Code)(Java Doc)
public IfMatchResult matchIf(IteratorOfIfFormulaInstantiation p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
public MatchConditions matchIf(IteratorOfIfFormulaInstantiation p_toMatch, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)(Code)(Java Doc)
final protected MatchConditions matchJavaBlock(Term term, Term template, MatchConditions matchCond, Services services)(Code)(Java Doc)
public Name name()(Code)(Java Doc)
public boolean noninteractive()(Code)(Java Doc)
public ListOfName oldNames()(Code)(Java Doc)
public MapFromSchemaVariableToTacletPrefix prefixMap()(Code)(Java Doc)
public ListOfSchemaVariable readSet()(Code)(Java Doc)
protected void replaceAtPos(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code)(Java Doc)
public IteratorOfRuleSet ruleSets()(Code)(Java Doc)
abstract protected Taclet setName(String s)(Code)(Java Doc)
protected Taclet setName(String s, TacletBuilder b)(Code)(Java Doc)
protected void setRestrictedMetavariables(Goal p_goal, MatchConditions p_matchCond)(Code)(Java Doc)
protected Term syntacticalReplace(Term term, Services services, MatchConditions mc)(Code)(Java Doc)
public String toString()(Code)(Java Doc)
StringBuffer toStringAttribs(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringGoalTemplates(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringIf(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringRuleSets(StringBuffer sb)(Code)(Java Doc)
StringBuffer toStringVarCond(StringBuffer sb)(Code)(Java Doc)
public NewVarcond varDeclaredNew(SchemaVariable var)(Code)(Java Doc)
protected boolean varIsBound(SchemaVariable v)(Code)(Java Doc)
public ListOfNewVarcond varsNew()(Code)(Java Doc)
public IteratorOfNewDependingOn varsNewDependingOn()(Code)(Java Doc)
public IteratorOfNotFreeIn varsNotFreeIn()(Code)(Java Doc)
public ListOfSchemaVariable writeSet()(Code)(Java Doc)
|
|
|