de.uka.ilkd.key.rule

Class NoFindTaclet

java.lang.Object

de.uka.ilkd.key.rule.Taclet

de.uka.ilkd.key.rule.NoFindTaclet

All Implemented Interfaces:

Named, Rule

public class NoFindTaclet
extends Taclet

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.

Nested Class Summary

Nested classes/interfaces inherited from class de.uka.ilkd.key.rule.Taclet

Taclet.TacletLabelHint

Field Summary

Fields inherited from class de.uka.ilkd.key.rule.Taclet

choices, executor, prefixMap, ruleSets, tacletAnnotations, tacletAsString

Constructor Summary

Constructors

Constructor and Description
NoFindTaclet(Name name, TacletApplPart applPart, ImmutableList<TacletGoalTemplate> goalTemplates, ImmutableList<RuleSet> ruleSets, TacletAttributes attrs, ImmutableMap<SchemaVariable,TacletPrefix> prefixMap, ImmutableSet<Choice> choices, ImmutableSet<TacletAnnotation> tacletAnnotations) creates a Schematic Theory Specific Rule (Taclet) with the given parameters.

Method Summary

Modifier and Type	Method and Description
protected void	createAndInitializeExecutor()
protected ImmutableSet<QuantifiableVariable>	getBoundVariablesHelper() the empty set as a no find taclet has no other entities where variables cann occur bound than in the goal templates
ImmutableSet<SchemaVariable>	getIfFindVariables()
NoFindTaclet	setName(java.lang.String s)

Methods inherited from class de.uka.ilkd.key.rule.Taclet

admissible, admissibleAutomatic, admissibleInteractive, apply, closeGoal, collectSchemaVars, createAndInitializeMatcher, createTacletServices, displayName, equals, getBoundVariables, getChoices, getExecutor, getIfVariables, getMatcher, getNameCorrespondent, getPrefix, getRuleJustification, getRuleSets, getSurviveSymbExec, getTrigger, getVariableConditions, goalTemplates, hashCode, hasReplaceWith, hasTrigger, ifSequent, isContextInPrefix, name, prefixMap, ruleSets, toString, toStringAttribs, toStringGoalTemplates, toStringIf, toStringRuleSets, toStringVarCond, varDeclaredNew, varsNew, varsNewDependingOn, varsNotFreeIn

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

NoFindTaclet

public NoFindTaclet(Name name,
                    TacletApplPart applPart,
                    ImmutableList<TacletGoalTemplate> goalTemplates,
                    ImmutableList<RuleSet> ruleSets,
                    TacletAttributes attrs,
                    ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
                    ImmutableSet<Choice> choices,
                    ImmutableSet<TacletAnnotation> tacletAnnotations)

creates a Schematic Theory Specific Rule (Taclet) with the given parameters.

Parameters:

name - the name of the Taclet

applPart - contains the application part of an Taclet that is the if-sequent, the variable conditions

goalTemplates - the IList containg all goal descriptions of the taclet to be created

ruleSets - a list of rule sets for the Taclet

attrs - attributes for the Taclet; these are boolean values

prefixMap - a ImmMap that contains the prefix for each SchemaVariable in the Taclet

choices - the SetOf to which this taclet belongs to

Method Detail

createAndInitializeExecutor

protected void createAndInitializeExecutor()

Specified by:

createAndInitializeExecutor in class Taclet

getIfFindVariables

public ImmutableSet<SchemaVariable> getIfFindVariables()

Specified by:

getIfFindVariables in class Taclet

Returns:

Set of schemavariables of the if and the (optional) find part

getBoundVariablesHelper

protected ImmutableSet<QuantifiableVariable> getBoundVariablesHelper()

the empty set as a no find taclet has no other entities where variables cann occur bound than in the goal templates

Specified by:

getBoundVariablesHelper in class Taclet

Returns:

empty set

setName

public NoFindTaclet setName(java.lang.String s)

Specified by:

setName in class Taclet