| java.lang.Object
 de.uka.ilkd.key.rule.Taclet
All known Subclasses: de.uka.ilkd.key.rule.NoFindTaclet, de.uka.ilkd.key.rule.FindTaclet,
| Taclet | | abstract public class Taclet implements Rule,Named(Code) | | Taclets are the DL-extension of schematic theory specific rules. They are
used to describe rules of a logic (sequent) calculus. A typical taclet
definition looks similar to
taclet_name { if ( ... ) find ( ... ) goal_descriptions }
where the if-part must and the find-part can contain a sequent arrow, that
indicates, if a term has to occur at the top level and if so, on which side of
the sequent. The goal descriptions consists of lists of add and replacewith
constructs. They describe, how to construct a new goal out of the old one by
adding or replacing parts of the sequent. Each of these lists describe a new
goal, whereas if no such list exists, means that the goal is closed.
The find part of a taclet is used to attached the rule to a term in the
sequent of the current goal. Therefore the term of the sequent has to match
the schema as found in the taclet's find part. The taclet is then attached to
this term, more precise not the taclet itself, but an application object of
this taclet (see
de.uka.ilkd.key.rule.TacletApp TacletApp . When
this attached taclet application object is applied, the new goals are
constructed as described by the goal descriptions. For example
find (A | B ==>) replacewith ( A ==> ); replacewith(B ==>)
creates
two new goals, where the first has been built by replacing A | B
with A and the second one by replacing A | B with
B. For a complete description of the syntax and semantics of
taclets consult the KeY-Manual. The objects of this class serve different
purposes: First they represent the syntactical structure of a taclet, but
they also include the taclet interpreter isself. The taclet interpreter
knows two modes: the match and the execution mode. The match mode tries to
find a a mapping from schemavariables to a given term or formula. In the
execution mode, a given goal is manipulated in the manner as described by the
goal descriptions.
But an object of this class neither copies or split the goal, nor it
iterates through a sequent looking where it can be applied, these tasks have
to be done in advance. For example by one of the following classes
de.uka.ilkd.key.proof.RuleAppIndex RuleAppIndex or
de.uka.ilkd.key.proof.TacletAppIndex TacletAppIndex or
de.uka.ilkd.key.rule.TacletApp TacletApp
|
| Constructor Summary | |
| | Taclet(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. |
| Method Summary | |
| protected void | addToAntec(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)
adds ConstrainedFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent). | | protected void | addToSucc(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)
adds ConstrainedFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent). | | public SetOfSchemaVariable | addedRuleNameVars()
| | public boolean | admissible(boolean interactive, ListOfRuleSet ruleSets)
| | protected boolean | admissibleAutomatic(ListOfRuleSet ruleSets)
| | protected boolean | admissibleInteractive(ListOfRuleSet ruleSets)
| | abstract public ListOfGoal | apply(Goal goal, Services services, RuleApp tacletApp)
the rule is applied to 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:
tacletApp - the rule application that is executed. | | protected void | applyAddProgVars(SetOfSchemaVariable pvs, Goal goal, PosInOccurrence posOfFind, Services services, MatchConditions matchCond)
| | protected void | applyAddrule(ListOfTaclet rules, Goal goal, Services services, MatchConditions matchCond)
adds the given rules (i.e. | | protected void | cacheMatchInfo()
| | public MatchConditions | checkConditions(MatchConditions cond, Services services)
| | protected ListOfGoal | checkIfGoals(Goal p_goal, ListOfIfFormulaInstantiation p_list, MatchConditions p_matchCond, int p_numberOfNewGoals)
Search for formulas within p_list that have to be proved by an
explicit if goal, i.e. | | public MatchConditions | checkVariableConditions(SchemaVariable var, SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services)
| | public boolean | closeGoal()
| | public Constraint | constraint()
| | public String | displayName()
| | public boolean | equals(Object o)
return true if o is a taclet of the same name and
o and this contain no mutually exclusive
taclet options. | | public SetOfQuantifiableVariable | getBoundVariables()
computes and returns all variables that occur bound in the taclet
including the taclets defined in addrules sections. | | abstract protected SetOfQuantifiableVariable | getBoundVariablesHelper()
| | public SetOfChoice | getChoices()
| | abstract public SetOfSchemaVariable | getIfFindVariables()
| | protected SetOfSchemaVariable | getIfVariables()
| | public SchemaVariable | getNameCorrespondent(SchemaVariable p)
| | public TacletPrefix | getPrefix(SchemaVariable sv)
returns the computed prefix for the given schemavariable. | | public ListOfRuleSet | getRuleSets()
| | public IteratorOfVariableCondition | getVariableConditions()
| | public ListOfTacletGoalTemplate | goalTemplates()
returns an iterator over the goal descriptions. | | public boolean | hasReplaceWith()
returns true if one of the goal templates is a replacewith. | | public int | hashCode()
| | public String | helpText()
| | public Sequent | ifSequent()
returns the if-sequence of the application part of the Taclet. | | public boolean | isContextInPrefix()
returns true iff a context flag is set in one of the entries in
the prefix map. | | protected MatchConditions | match(Term term, Term template, boolean ignoreUpdates, MatchConditions matchCond, Services services, Constraint userConstraint)
returns a SVInstantiations object iff the given Term
template can be instantiated to
match the given Term term using the known instantiations stored in
svInst. | | protected MatchConditions | match(Term term, Term template, MatchConditions matchCond, Services services, Constraint userConstraint)
| | public IfMatchResult | matchIf(IteratorOfIfFormulaInstantiation p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)
Match the given template (which is probably a formula of the if
sequence) against a list of constraint formulas (probably the
formulas of the antecedent or the succedent), starting with the
given instantiations and constraint p_matchCond.
Parameters:
p_toMatch - list of constraint formulas to match p_template to
Parameters:
p_template - template formula as in "match"
Parameters:
p_matchCond - already performed instantiations
Parameters:
p_services - the Services object encapsulating informationabout the java datastructures like (static)types etc. | | public MatchConditions | matchIf(IteratorOfIfFormulaInstantiation p_toMatch, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)
Match the whole if sequent using the given list of
instantiations of all if sequent formulas, starting with the
instantiations given by p_matchCond. | | final protected MatchConditions | matchJavaBlock(Term term, Term template, MatchConditions matchCond, Services services)
| | public Name | name()
| | public boolean | noninteractive()
| | public ListOfName | oldNames()
| | public MapFromSchemaVariableToTacletPrefix | prefixMap()
| | public ListOfSchemaVariable | readSet()
| | protected void | replaceAtPos(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)
| | public IteratorOfRuleSet | ruleSets()
returns an iterator over the rule sets. | | abstract protected Taclet | setName(String s)
| | protected Taclet | setName(String s, TacletBuilder b)
| | protected void | setRestrictedMetavariables(Goal p_goal, MatchConditions p_matchCond)
| | protected Term | syntacticalReplace(Term term, Services services, MatchConditions mc)
| | public String | toString()
| | StringBuffer | toStringAttribs(StringBuffer sb)
| | StringBuffer | toStringGoalTemplates(StringBuffer sb)
| | StringBuffer | toStringIf(StringBuffer sb)
| | StringBuffer | toStringRuleSets(StringBuffer sb)
| | StringBuffer | toStringVarCond(StringBuffer sb)
| | public NewVarcond | varDeclaredNew(SchemaVariable var)
looks if a variable is declared as new and returns its sort to match
with or the schema variable it shares the match-sort with. | | protected boolean | varIsBound(SchemaVariable v)
| | public ListOfNewVarcond | varsNew()
returns an iterator over the variables that are new in the Taclet. | | public IteratorOfNewDependingOn | varsNewDependingOn()
| | public IteratorOfNotFreeIn | varsNotFreeIn()
returns an iterator over the variable pairs that indicate that are
new in the Taclet. | | public ListOfSchemaVariable | writeSet()
|
| addedRuleNameVars | | protected SetOfSchemaVariable addedRuleNameVars(Code) | | cache
|
| choices | | final protected SetOfChoice choices(Code) | | the set of taclet options for this taclet
|
| prefixMap | | final protected MapFromSchemaVariableToTacletPrefix prefixMap(Code) | | map from a schemavariable to its prefix. The prefix is used to test
correct instantiations of the schemavariables by resolving/avoiding
collisions. Mainly the prefix consists of a list of all variables that
may appear free in the instantiation of the schemavariable (a bit more
complicated for rewrite taclets, see paper of M:Giese)
|
| ruleSets | | final protected ListOfRuleSet ruleSets(Code) | | list of rulesets (formerly known as heuristica) the taclet belongs to
|
| Taclet | | Taclet(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-sequence, the variable conditions
Parameters:
goalTemplates - a list of goal descriptions.
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 valuesindicating a noninteractive or recursive use of the Taclet. |
| addToAntec | | protected void addToAntec(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code) | | adds ConstrainedFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent). Of course it has to be ensured that
the position information describes one occurrence in the
antecedent of the sequent.
Parameters:
semi - the Semisequent with the the ConstrainedFormulae to be added
Parameters:
goal - the Goal that knows the node the formulae have to be added
Parameters:
pos - the PosInOccurrence describing the place in thesequent or null for head of antecedent
Parameters:
services - the Services encapsulating all java information
Parameters:
matchCond - the MatchConditions containing in particularthe instantiations of the schemavariables |
| addToSucc | | protected void addToSucc(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code) | | adds ConstrainedFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent). Of course it has to be ensured that
the position information describes one occurrence in the
succedent of the sequent.
Parameters:
semi - the Semisequent with the the ConstrainedFormulae to be added
Parameters:
goal - the Goal that knows the node the formulae have to be added
Parameters:
pos - the PosInOccurrence describing the place in thesequent or null for head of antecedent
Parameters:
services - the Services encapsulating all java information
Parameters:
matchCond - the MatchConditions containing in particularthe instantiations of the schemavariables |
| addedRuleNameVars | | public SetOfSchemaVariable addedRuleNameVars()(Code) | | |
| admissible | | public boolean admissible(boolean interactive, ListOfRuleSet ruleSets)(Code) | | true iff this taclet may be applied for thegiven mode (interactive/non-interactive, activated rule sets) |
| admissibleAutomatic | | protected boolean admissibleAutomatic(ListOfRuleSet ruleSets)(Code) | | |
| admissibleInteractive | | protected boolean admissibleInteractive(ListOfRuleSet ruleSets)(Code) | | |
| apply | | abstract public ListOfGoal apply(Goal goal, Services services, RuleApp tacletApp)(Code) | | the rule is applied to 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:
tacletApp - the rule application that is executed. List of the goals created by the rule which have to beproved. If this is a close-goal-taclet ( this.closeGoal () ),the first goal of the return list is the goal that should beclosed (with the constraint this taclet is applied under). |
| applyAddrule | | protected void applyAddrule(ListOfTaclet rules, Goal goal, Services services, MatchConditions matchCond)(Code) | | adds the given rules (i.e. the rules to add according to the Taclet goal
template to the node of the given goal
Parameters:
rules - the rules to be added
Parameters:
goal - the goal describing the node where the rules should be added
Parameters:
services - the Services encapsulating all java information
Parameters:
matchCond - the MatchConditions containing in particularthe instantiations of the schemavariables |
| cacheMatchInfo | | protected void cacheMatchInfo()(Code) | | |
| checkIfGoals | | protected ListOfGoal checkIfGoals(Goal p_goal, ListOfIfFormulaInstantiation p_list, MatchConditions p_matchCond, int p_numberOfNewGoals)(Code) | | Search for formulas within p_list that have to be proved by an
explicit if goal, i.e. elements of type IfFormulaInstDirect.
an array with two goals if such formulas exist (thesecond goal is the if goal), otherwise an array consisting ofthe single element p_goal |
| checkVariableConditions | | public MatchConditions checkVariableConditions(SchemaVariable var, SVSubstitute instantiationCandidate, MatchConditions matchCond, Services services)(Code) | | checks if the conditions for a correct instantiation are satisfied
Parameters:
var - the SchemaVariable to be instantiated
Parameters:
instantiationCandidate - the SVSubstitute, which is acandidate for a possible instantiation of var
Parameters:
matchCond - the MatchConditions which have to be respectedfor the new match
Parameters:
services - the Services object encapsulating informationabout the Java type model the match conditions resulting from matchingvar with instantiationCandidate ornull if a match was not possible |
| closeGoal | | public boolean closeGoal()(Code) | | returns true iff the taclet contains a "close goal"-statement
true iff the taclet contains a "close goal"-statement |
| constraint | | public Constraint constraint()(Code) | | returns the Constraint under which the Taclet is
valid
|
| displayName | | public String displayName()(Code) | | returns the display name of the taclet, or, if not specified --
the canonical name
|
| equals | | public boolean equals(Object o)(Code) | | return true if o is a taclet of the same name and
o and this contain no mutually exclusive
taclet options.
|
| getBoundVariables | | public SetOfQuantifiableVariable getBoundVariables()(Code) | | computes and returns all variables that occur bound in the taclet
including the taclets defined in addrules sections. The result
is cached and therefore only computed once.
all variables occuring bound in the taclet |
| getBoundVariablesHelper | | abstract protected SetOfQuantifiableVariable getBoundVariablesHelper()(Code) | | collects bound variables in taclet entities others than goal templates
set of variables that occur bound in taclet entities others than goal templates |
| getChoices | | public SetOfChoice getChoices()(Code) | | |
| getIfFindVariables | | abstract public SetOfSchemaVariable getIfFindVariables()(Code) | | set of schemavariables of the if and the (optional)find part |
| getIfVariables | | protected SetOfSchemaVariable getIfVariables()(Code) | | returns the set of schemavariables of the taclet's if-part
Set of schemavariables of the if part |
| getNameCorrespondent | | public SchemaVariable getNameCorrespondent(SchemaVariable p)(Code) | | Find a schema variable that could be used to choose a name for
an instantiation (a new variable or constant) of "p"
a schema variable that is substituted by "p" somewherein this taclet (that is, these schema variables occur asarguments of a substitution operator) |
| getPrefix | | public TacletPrefix getPrefix(SchemaVariable sv)(Code) | | returns the computed prefix for the given schemavariable. The
prefix of a schemavariable is used to determine if an
instantiation is correct, in more detail: it mainly contains all
variables that can appear free in an instantiation of the
schemvariable sv (rewrite taclets have some special handling, see
paper of M. Giese and comment of method isContextInPrefix).
Parameters:
sv - the Schemavariable prefix of schema variable sv |
| getRuleSets | | public ListOfRuleSet getRuleSets()(Code) | | |
| getVariableConditions | | public IteratorOfVariableCondition getVariableConditions()(Code) | | the generic variable conditions of this taclet |
| goalTemplates | | public ListOfTacletGoalTemplate goalTemplates()(Code) | | returns an iterator over the goal descriptions.
|
| hasReplaceWith | | public boolean hasReplaceWith()(Code) | | returns true if one of the goal templates is a replacewith. Already
computed and cached by method cacheMatchInfo
|
| hashCode | | public int hashCode()(Code) | | |
| ifSequent | | public Sequent ifSequent()(Code) | | returns the if-sequence of the application part of the Taclet.
|
| isContextInPrefix | | public boolean isContextInPrefix()(Code) | | returns true iff a context flag is set in one of the entries in
the prefix map. Is cached after having been called
once. __OPTIMIZE__ is caching really necessary here?
true iff a context flag is set in one of the entries inthe prefix map. |
| match | | protected MatchConditions match(Term term, Term template, boolean ignoreUpdates, MatchConditions matchCond, Services services, Constraint userConstraint)(Code) | | returns a SVInstantiations object iff the given Term
template can be instantiated to
match the given Term term using the known instantiations stored in
svInst. If a
matching cannot be found null is returned.
The not free in condition is checked in TacletApp. Collisions are
resolved there as well, if necessary.
Parameters:
term - the Term that has to be matched
Parameters:
template - the Term that is checked if it can match term
Parameters:
ignoreUpdates - a boolean if set to true updates will be ignored as e.g. wanted if an if-sequent is matched
Parameters:
matchCond - the SVInstantiations/Constraint that arerequired because of formerly matchings
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc.
Parameters:
userConstraint - current user constraint (which is in somesituations used to find instantiations) the new MatchConditions needed to match template withterm , if possible, null otherwise |
| match | | protected MatchConditions match(Term term, Term template, MatchConditions matchCond, Services services, Constraint userConstraint)(Code) | | same as the method above but with ignoreUpdates always false
Parameters:
term - the Term that has to be matched
Parameters:
template - the Term that is checked if it can match term
Parameters:
matchCond - the SVInstantiations/Constraint that arerequired because of formerly matchings
Parameters:
services - the Services object encapsulating informationabout the java datastructures like (static)types etc.
Parameters:
userConstraint - current user constraint (which is in somesituations used to find instantiations) the new MatchConditions needed to match template withterm , if possible, null otherwise |
| matchIf | | public IfMatchResult matchIf(IteratorOfIfFormulaInstantiation p_toMatch, Term p_template, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)(Code) | | Match the given template (which is probably a formula of the if
sequence) against a list of constraint formulas (probably the
formulas of the antecedent or the succedent), starting with the
given instantiations and constraint p_matchCond.
Parameters:
p_toMatch - list of constraint formulas to match p_template to
Parameters:
p_template - template formula as in "match"
Parameters:
p_matchCond - already performed instantiations
Parameters:
p_services - the Services object encapsulating informationabout the java datastructures like (static)types etc. Two lists (in an IfMatchResult object), containing thethe elements of p_toMatch that could successfully be matchedagainst p_template, and the corresponding MatchConditions. |
| matchIf | | public MatchConditions matchIf(IteratorOfIfFormulaInstantiation p_toMatch, MatchConditions p_matchCond, Services p_services, Constraint p_userConstraint)(Code) | | Match the whole if sequent using the given list of
instantiations of all if sequent formulas, starting with the
instantiations given by p_matchCond.
PRECONDITION: p_toMatch.size () == ifSequent ().size ()
resulting MatchConditions or null if the given listp_toMatch does not match |
| matchJavaBlock | | final protected MatchConditions matchJavaBlock(Term term, Term template, MatchConditions matchCond, Services services)(Code) | | returns the matchconditions that are required if the java block of the
given term matches the schema given by the template term or null if no
match is possible
(marked as final to help the compiler inlining methods)
Parameters:
term - the Term whose JavaBlock is matched against the JavaBlock ofthe template
Parameters:
template - the Term whose JavaBlock is the template that has tobe matched
Parameters:
matchCond - the MatchConditions that has to be paid respect whentrying to match the JavaBlocks
Parameters:
services - the Services object encapsulating information about theprogram context the new matchconditions if a match is possible, otherwise null |
| name | | public Name name()(Code) | | returns the name of the Taclet
|
| noninteractive | | public boolean noninteractive()(Code) | | returns true iff the Taclet is to be applied only noninteractive
|
| oldNames | | public ListOfName oldNames()(Code) | | returns the list of old names of the taclet
|
| prefixMap | | public MapFromSchemaVariableToTacletPrefix prefixMap()(Code) | | |
| readSet | | public ListOfSchemaVariable readSet()(Code) | | returns the variables in a Taclet with a read access
|
| replaceAtPos | | protected void replaceAtPos(Semisequent semi, Goal goal, PosInOccurrence pos, Services services, MatchConditions matchCond)(Code) | | replaces the constrained formula at the given position with the first
formula in the given semisequent and adds possible other formulas of the
semisequent starting at the position
Parameters:
semi - the Semisequent with the the ConstrainedFormulae to be added
Parameters:
goal - the Goal that knows the node the formulae have to be added
Parameters:
pos - the PosInOccurrence describing the place in the sequent
Parameters:
antec - boolean true(false) if elements have to be added to theantecedent(succedent) (only looked at if pos == null)
Parameters:
services - the Services encapsulating all java information
Parameters:
matchCond - the MatchConditions containing in particularthe instantiations of the schemavariables |
| ruleSets | | public IteratorOfRuleSet ruleSets()(Code) | | returns an iterator over the rule sets.
|
| setRestrictedMetavariables | | protected void setRestrictedMetavariables(Goal p_goal, MatchConditions p_matchCond)(Code) | | Restrict introduced metavariables to the subtree
|
| syntacticalReplace | | protected Term syntacticalReplace(Term term, Services services, MatchConditions mc)(Code) | | a new term is created by replacing variables of term whose replacement is
found in the given SVInstantiations
Parameters:
term - the Term the syntactical replacement is performed on
Parameters:
services - the Services
Parameters:
mc - the MatchConditions with all instantiations andthe constraint the (partially) instantiated term |
| toString | | public String toString()(Code) | | returns a representation of the Taclet as String
string representation |
| varDeclaredNew | | public NewVarcond varDeclaredNew(SchemaVariable var)(Code) | | looks if a variable is declared as new and returns its sort to match
with or the schema variable it shares the match-sort with. Returns
null if the SV is not declared to as new.
Parameters:
var - the SchemaVariable to look for the sort of the SV to match or the SV it shares the samematch-sort with |
| varIsBound | | protected boolean varIsBound(SchemaVariable v)(Code) | | returns true iff the given variable is bound either in the
ifSequent or in
any part of the TacletGoalTemplates
Parameters:
v - the bound variable to be searched |
| varsNew | | public ListOfNewVarcond varsNew()(Code) | | returns an iterator over the variables that are new in the Taclet.
|
| varsNewDependingOn | | public IteratorOfNewDependingOn varsNewDependingOn()(Code) | | |
| varsNotFreeIn | | public IteratorOfNotFreeIn varsNotFreeIn()(Code) | | returns an iterator over the variable pairs that indicate that are
new in the Taclet.
|
| writeSet | | public ListOfSchemaVariable writeSet()(Code) | | returns the variable in a Taclet to which is written to
|
|
|