Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.recoderext | |
de.uka.ilkd.key.java.reference |
Elements of the Java syntax tree representing implicit or explicit (named)
references to other program elements.
|
de.uka.ilkd.key.java.visitor |
contains classes representing visitors traversing the tree
structure of Java programs.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.nparser | |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.conditions | |
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.match.legacy | |
de.uka.ilkd.key.rule.match.vm | |
de.uka.ilkd.key.rule.match.vm.instructions | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.taclettranslation.lemma |
Constructor and Description |
---|
InfFlowContractAppTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
InfFlowContractAppTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
Modifier and Type | Field and Description |
---|---|
protected Namespace<SchemaVariable> |
SchemaRecoder2KeY.svns
the namespace containing the program schema variables allowed here
|
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
SchemaRecoder2KeYConverter.convert(CatchSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(CcatchSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(ExecCtxtSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(ExpressionSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(LabelSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(MethodSignatureSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(ProgramVariableSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(StatementSVWrapper svw) |
SchemaVariable |
SchemaRecoder2KeYConverter.convert(TypeSVWrapper svw) |
Modifier and Type | Method and Description |
---|---|
void |
PrettyPrinter.printSchemaVariable(SchemaVariable x) |
Modifier and Type | Method and Description |
---|---|
void |
SchemaJavaReader.setSVNamespace(Namespace<SchemaVariable> ns) |
void |
SchemaRecoder2KeY.setSVNamespace(Namespace<SchemaVariable> svns) |
Modifier and Type | Field and Description |
---|---|
protected SchemaVariable |
CcatchSVWrapper.sv |
protected SchemaVariable |
StatementSVWrapper.sv |
protected SchemaVariable |
ExpressionSVWrapper.sv |
protected SchemaVariable |
CatchSVWrapper.sv |
Modifier and Type | Field and Description |
---|---|
protected Namespace<SchemaVariable> |
SchemaJavaProgramFactory.svns |
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
CcatchSVWrapper.getSV()
returns a String name of this meta construct.
|
SchemaVariable |
JumpLabelSVWrapper.getSV() |
SchemaVariable |
SVWrapper.getSV()
returns a String name of this meta construct.
|
SchemaVariable |
MethodSignatureSVWrapper.getSV() |
SchemaVariable |
ExecCtxtSVWrapper.getSV()
returns the schema variable of this type sv wrapper
|
SchemaVariable |
ProgramVariableSVWrapper.getSV()
returns the schema variable of this type sv wrapper
|
SchemaVariable |
StatementSVWrapper.getSV()
returns a String name of this meta construct.
|
SchemaVariable |
TypeSVWrapper.getSV()
returns the schema variable of this type sv wrapper
|
SchemaVariable |
ExpressionSVWrapper.getSV() |
SchemaVariable |
CatchSVWrapper.getSV()
returns a String name of this meta construct.
|
SchemaVariable |
LabelSVWrapper.getSV()
returns the schema variable of this label sv wrapper
|
SchemaVariable |
SchemaJavaProgramFactory.lookupSchemaVariable(java.lang.String s) |
Modifier and Type | Method and Description |
---|---|
void |
CcatchSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort statement
|
void |
JumpLabelSVWrapper.setSV(SchemaVariable sv) |
void |
SVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort statement
|
void |
MethodSignatureSVWrapper.setSV(SchemaVariable sv) |
void |
ExecCtxtSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort label
|
void |
ProgramVariableSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort label
|
void |
StatementSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort statement
|
void |
TypeSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort label
|
void |
ExpressionSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort statement
|
void |
CatchSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort statement
|
void |
LabelSVWrapper.setSV(SchemaVariable sv)
sets the schema variable of sort label
|
static void |
SchemaJavaProgramFactory.throwSortInvalid(SchemaVariable sv,
java.lang.String s) |
Modifier and Type | Method and Description |
---|---|
void |
SchemaJavaProgramFactory.setSVNamespace(Namespace<SchemaVariable> ns) |
Constructor and Description |
---|
CatchSVWrapper(SchemaVariable sv) |
CcatchSVWrapper(SchemaVariable sv) |
ExecCtxtSVWrapper(SchemaVariable sv) |
ExpressionSVWrapper(SchemaVariable sv) |
JumpLabelSVWrapper(SchemaVariable l) |
LabelSVWrapper(SchemaVariable sv) |
MethodSignatureSVWrapper(SchemaVariable l) |
ProgramVariableSVWrapper(SchemaVariable sv) |
StatementSVWrapper(SchemaVariable sv) |
TypeSVWrapper(SchemaVariable sv) |
Modifier and Type | Field and Description |
---|---|
protected SchemaVariable |
SchematicFieldReference.schemaVariable
Reference suffix
|
Constructor and Description |
---|
SchematicFieldReference(SchemaVariable pe,
ReferencePrefix prefix) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<SchemaVariable> |
ProgramSVCollector.getSchemaVariables() |
Modifier and Type | Method and Description |
---|---|
void |
Visitor.performActionOnSchemaVariable(SchemaVariable x) |
void |
JavaASTVisitor.performActionOnSchemaVariable(SchemaVariable x) |
void |
ProgramReplaceVisitor.performActionOnSchemaVariable(SchemaVariable sv) |
Constructor and Description |
---|
ProgramSVCollector(ProgramElement root,
ImmutableList<SchemaVariable> vars)
create the ProgramSVCollector
|
ProgramSVCollector(ProgramElement root,
ImmutableList<SchemaVariable> vars,
SVInstantiations svInst)
create the ProgramSVCollector
|
Modifier and Type | Method and Description |
---|---|
protected ProgramElementName |
VariableNamer.getNameProposalForSchemaVariable(java.lang.String basename,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
(like getProposal(), but somewhat less nicely)
|
java.lang.String |
VariableNamer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
proposes a unique name for the instantiation of a schema variable
|
java.lang.String |
VariableNamer.getSuggestiveNameProposalForProgramVariable(SchemaVariable sv,
TacletApp app,
Services services,
ImmutableList<java.lang.String> previousProposals) |
boolean |
VariableNamer.isUniqueNameForSchemaVariable(java.lang.String name,
SchemaVariable sv,
PosInOccurrence posOfFind,
PosInProgram posOfDeclaration)
tells whether a name for instantiating a schema variable is unique
within its scope
|
Term |
TermBuilder.var(SchemaVariable v) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractSV
Abstract base class for schema variables.
|
class |
FormulaSV
A schema variable that is used as placeholder for formulas.
|
class |
ModalOperatorSV
Schema variable matching modal operators.
|
class |
ProgramSV
Objects of this class are schema variables matching program constructs within
modal operators.
|
class |
SkolemTermSV
Schema variable that is instantiated with fresh Skolem constants.
|
class |
TermLabelSV
A schema variable which matches term labels
|
class |
TermSV
A schema variable that is used as placeholder for terms.
|
class |
UpdateSV
A schema variable that is used as placeholder for updates.
|
class |
VariableSV
Schema variable that is instantiated with logical variables.
|
Modifier and Type | Method and Description |
---|---|
Namespace<SchemaVariable> |
KeyIO.Loader.getSchemaNamespace() |
Modifier and Type | Method and Description |
---|---|
void |
KeyIO.setSchemaNamespace(Namespace<SchemaVariable> ns) |
Modifier and Type | Method and Description |
---|---|
Namespace<SchemaVariable> |
DefaultBuilder.schemaVariables() |
ImmutableSet<SchemaVariable> |
TacletPBuilder.visitAddprogvar(KeYParser.AddprogvarContext ctx) |
Modifier and Type | Method and Description |
---|---|
void |
DefaultBuilder.setSchemaVariables(Namespace<SchemaVariable> ns) |
Constructor and Description |
---|
ExpressionBuilder(Services services,
NamespaceSet nss,
Namespace<SchemaVariable> schemaNamespace) |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printSchemaVariable(SchemaVariable sv) |
Modifier and Type | Method and Description |
---|---|
protected void |
LogicPrinter.printAddProgVars(ImmutableSet<SchemaVariable> apv) |
Modifier and Type | Method and Description |
---|---|
protected static java.lang.String |
VariableNameProposer.createBaseNameProposalBasedOnCorrespondence(TacletApp p_app,
SchemaVariable p_var,
Services services)
Find a name for the variable
p_var , based on the result
of Taclet.getNameCorrespondent |
java.lang.String |
InstantiationProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
VariableNameProposer.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals)
Returns an instantiation proposal for the schema variable var.
|
java.lang.String |
InstantiationProposerCollection.getProposal(TacletApp app,
SchemaVariable var,
Services services,
Node undoAnchor,
ImmutableList<java.lang.String> previousProposals) |
Modifier and Type | Method and Description |
---|---|
static TacletApp |
IntermediateProofReplayer.parseSV1(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Services services)
Instantiates a schema variable in the given taclet application.
|
static TacletApp |
IntermediateProofReplayer.parseSV2(TacletApp app,
SchemaVariable sv,
java.lang.String value,
Goal targetGoal)
Instantiates a schema variable in the given taclet application.
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableMap<SchemaVariable,TacletPrefix> |
Taclet.prefixMap
map from a schemavariable to its prefix.
|
protected ImmutableList<SchemaVariable> |
TacletSchemaVariableCollector.varList
collects all found variables
|
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
NewDependingOn.first()
Deprecated.
returns the first SchemaVariable of the pair.
|
SchemaVariable |
NotFreeIn.first()
returns the first SchemaVariable of the pair.
|
SchemaVariable |
Taclet.getNameCorrespondent(SchemaVariable p,
Services services)
Find a schema variable that could be used to choose a name for
an instantiation (a new variable or constant) of "p"
|
SchemaVariable |
NewVarcond.getPeerSchemaVariable() |
SchemaVariable |
NewVarcond.getSchemaVariable() |
SchemaVariable |
Trigger.getTriggerVar() |
SchemaVariable |
NewDependingOn.second()
Deprecated.
returns the second SchemaVariable of the pair.
|
SchemaVariable |
NotFreeIn.second()
returns the second SchemaVariable of the pair.
|
SchemaVariable |
TacletApp.varSVNameConflict()
returns the bound SchemaVariable that causes a name conflict (i.e.
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableSet<SchemaVariable> |
TacletApp.calculateNonInstantiatedSV()
calculate needed SchemaVariables that have not been instantiated yet.
|
java.util.Set<SchemaVariable> |
Taclet.collectSchemaVars() |
protected ImmutableList<SchemaVariable> |
TacletSchemaVariableCollector.collectSVInProgram(JavaBlock jb,
ImmutableList<SchemaVariable> vars)
collects all SchemVariables that occur in the JavaBlock
|
ImmutableMap<SchemaVariable,SchemaVariable> |
SVNameCorrespondenceCollector.getCorrespondences() |
ImmutableMap<SchemaVariable,SchemaVariable> |
SVNameCorrespondenceCollector.getCorrespondences() |
abstract ImmutableSet<SchemaVariable> |
Taclet.getIfFindVariables() |
ImmutableSet<SchemaVariable> |
FindTaclet.getIfFindVariables() |
ImmutableSet<SchemaVariable> |
NoFindTaclet.getIfFindVariables() |
protected ImmutableSet<SchemaVariable> |
Taclet.getIfVariables()
returns the set of schemavariables of the taclet's if-part
|
java.util.Iterator<SchemaVariable> |
TacletPrefix.iterator() |
ImmutableSet<SchemaVariable> |
TacletPrefix.prefix()
returns the prefix
|
ImmutableMap<SchemaVariable,TacletPrefix> |
Taclet.prefixMap() |
ImmutableSet<SchemaVariable> |
TacletApp.uninstantiatedVars()
returns the variables that have not yet been instantiated and need to be
instantiated to apply the Taclet.
|
java.util.Iterator<SchemaVariable> |
TacletSchemaVariableCollector.varIterator() |
java.lang.Iterable<SchemaVariable> |
TacletSchemaVariableCollector.vars() |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletApp.addCheckedInstantiation(SchemaVariable sv,
ProgramElement pe,
Services services,
boolean interesting)
checks if the instantiation of
sv with pe is
possible. |
TacletApp |
TacletApp.addCheckedInstantiation(SchemaVariable sv,
Term term,
Services services,
boolean interesting)
creates a new Tacletapp where the SchemaVariable sv is instantiated with
the the given Term term.
|
TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
Name name,
Services services) |
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
java.lang.Object[] list,
boolean interesting,
Services services) |
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
ProgramElement pe,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp.
|
TacletApp |
NoPosTacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
TacletApp |
PosTacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
abstract TacletApp |
TacletApp.addInstantiation(SchemaVariable sv,
Term term,
boolean interesting,
Services services)
adds a new instantiation to this TacletApp
|
MatchConditions |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
VariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
abstract boolean |
VariableConditionAdapter.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
MatchConditions |
TacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
boolean |
TacletSchemaVariableCollector.contains(SchemaVariable var) |
protected ImmutableSet<QuantifiableVariable> |
NoPosTacletApp.contextVars(SchemaVariable sv) |
protected ImmutableSet<QuantifiableVariable> |
PosTacletApp.contextVars(SchemaVariable sv) |
protected abstract ImmutableSet<QuantifiableVariable> |
TacletApp.contextVars(SchemaVariable sv) |
TacletApp |
TacletApp.createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
boolean interesting,
Services services)
Create a new constant named "instantiation" and instantiate "sv" with.
|
TacletApp |
TacletApp.createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
Sort sort,
boolean interesting,
Services services) |
Namespace<QuantifiableVariable> |
TacletApp.extendVarNamespaceForSV(Namespace<QuantifiableVariable> var_ns,
SchemaVariable sv)
creates a new variable namespace by adding names of the instantiations of
the schema variables in the context of the given schema variable and (if
the TacletApp's prefix has the context flag set) by adding names of the
logic variables of the context.
|
SchemaVariable |
Taclet.getNameCorrespondent(SchemaVariable p,
Services services)
Find a schema variable that could be used to choose a name for
an instantiation (a new variable or constant) of "p"
|
TacletPrefix |
Taclet.getPrefix(SchemaVariable sv)
returns the computed prefix for the given schemavariable.
|
ProgramElement |
TacletApp.getProgramElement(java.lang.String instantiation,
SchemaVariable sv,
Services services) |
Sort |
TacletApp.getRealSort(SchemaVariable p_sv,
TermServices services) |
boolean |
TacletApp.isInstantiationRequired(SchemaVariable sv)
returns true if the given
SchemaVariable must be explicitly instantiated
it does not check whether sv is already instantiated or not |
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
ProgramElement term,
MatchConditions matchCond,
Services services)
|
MatchConditions |
TacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
TacletPrefix |
TacletPrefix.put(SchemaVariable var)
creates a new TacletPrefix with a new prefix entry
|
TacletPrefix |
TacletPrefix.remove(SchemaVariable var)
removes a SchemaVariable from the prefix
|
protected static SVInstantiations |
TacletApp.replaceInstantiation(Taclet taclet,
SVInstantiations insts,
SchemaVariable varSV,
Services services)
returns a new SVInstantiations that modifies the given SVInstantiations
insts at the bound SchemaVariable varSV to a new LogicVariable.
|
NewVarcond |
Taclet.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.
|
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<SchemaVariable> |
TacletSchemaVariableCollector.collectSVInProgram(JavaBlock jb,
ImmutableList<SchemaVariable> vars)
collects all SchemVariables that occur in the JavaBlock
|
Constructor and Description |
---|
NewDependingOn(SchemaVariable first,
SchemaVariable second)
Deprecated.
constructs a pair of variables given two SchemaVariables.
|
NewVarcond(SchemaVariable sv,
KeYJavaType type) |
NewVarcond(SchemaVariable sv,
SchemaVariable peerSV) |
NotFreeIn(SchemaVariable first,
SchemaVariable second)
constructs a pair of variables given two SchemaVariables.
|
Trigger(SchemaVariable triggerVar,
Term trigger,
ImmutableList<Term> avoidConditions) |
Constructor and Description |
---|
AntecTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters.
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
FindTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a FindTaclet
|
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.
|
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
boolean surviveSymbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations) |
RewriteTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
Term find,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
int p_applicationRestriction,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that represents a rewrite rule.
|
SuccTaclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> heuristics,
TacletAttributes attrs,
Term find,
boolean ignoreTopLevelUpdates,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Schematic Theory Specific Rule (Taclet) with the given
parameters that works on the succedent.
|
Taclet(Name name,
TacletApplPart applPart,
ImmutableList<TacletGoalTemplate> goalTemplates,
ImmutableList<RuleSet> ruleSets,
TacletAttributes attrs,
ImmutableMap<SchemaVariable,TacletPrefix> prefixMap,
ImmutableSet<Choice> choices,
boolean surviveSmbExec,
ImmutableSet<TacletAnnotation> tacletAnnotations)
creates a Taclet (originally known as Schematic Theory Specific Rules)
|
Taclet(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.
|
TacletPrefix(ImmutableSet<SchemaVariable> prefix,
boolean context)
creates the prefix
|
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
ArrayComponentTypeCondition.getVar() |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
FieldTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessElementariesCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
NewJumpLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
IsLabeledCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SimplifyIfThenElseUpdateCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
LoopVariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
StoreStmtInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
ObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
HasLoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopFreeInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
EqualUniqueCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
ApplyUpdateOnRigidCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
JavaTypeToSortCondition.check(SchemaVariable var,
SVSubstitute svSubst,
MatchConditions matchCond,
Services services) |
MatchConditions |
LoopInvariantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
DropEffectlessStoresCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
MatchConditions |
StoreTermInCondition.check(SchemaVariable sv,
SVSubstitute instCandidate,
MatchConditions matchCond,
Services services) |
MatchConditions |
SameObserverCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
MatchConditions mc,
Services services) |
boolean |
AlternativeVariableCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services)
check whether any of the two delegates apply
|
boolean |
ContainsAssignmentCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services)
checks if the condition for a correct instantiation is fulfilled
|
boolean |
AbstractOrInterfaceType.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MayExpandMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
TypeComparisonCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayComponentTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
DifferentInstantiationCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
ArrayTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
IsThisReference.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
EnumTypeCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
StaticFieldCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TermLabelCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
TypeCondition.check(SchemaVariable p_var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
LocalVariableCondition.check(SchemaVariable var,
SVSubstitute candidate,
SVInstantiations svInst,
Services services) |
boolean |
SubFormulaCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
MetaDisjointCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
DifferentFields.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
ConstantCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
FinalReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
FreeLabelInVariableCondition.check(SchemaVariable var,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
boolean |
StaticMethodCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
EnumConstantCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
ArrayLengthCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
boolean |
StaticReferenceCondition.check(SchemaVariable var,
SVSubstitute subst,
SVInstantiations svInst,
Services services) |
static boolean |
FieldTypeToSortCondition.checkSortedSV(SchemaVariable exprOrTypeSV) |
static boolean |
JavaTypeToSortCondition.checkSortedSV(SchemaVariable exprOrTypeSV) |
static TypeResolver |
TypeResolver.createContainerTypeResolver(SchemaVariable s) |
static TypeResolver |
TypeResolver.createElementTypeResolver(SchemaVariable s) |
abstract boolean |
TypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.GenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.NonGenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ElementTypeResolverForSV.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ContainerTypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
abstract Sort |
TypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.GenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.NonGenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ElementTypeResolverForSV.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ContainerTypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Constructor and Description |
---|
ApplyUpdateOnRigidCondition(UpdateSV u,
SchemaVariable x,
SchemaVariable x2) |
ArrayComponentTypeCondition(SchemaVariable var,
boolean checkReferenceType)
creates an instance of this condition checking if array var has reference
or primitive component type depending on the value of
checkReferenceType |
ArrayLengthCondition(SchemaVariable reference,
boolean negation) |
ArrayTypeCondition(SchemaVariable var,
boolean negated)
creates an instance of this condition checking if an instantiation of a schema variable is an array or not
|
ContainerTypeResolver(SchemaVariable sv) |
ContainsAssignmentCondition(SchemaVariable x,
boolean negated)
creates an instance of the variable condition
|
DifferentFields(SchemaVariable var1,
SchemaVariable var2) |
DifferentInstantiationCondition(SchemaVariable var1,
SchemaVariable var2) |
DropEffectlessElementariesCondition(UpdateSV u,
SchemaVariable x,
SchemaVariable x2) |
ElementTypeResolverForSV(SchemaVariable sv) |
EnumConstantCondition(SchemaVariable reference)
the static reference condition checks if a suggested
instantiation for a schema variable denotes a reference to
an enum constant.
|
FieldTypeToSortCondition(SchemaVariable exprOrTypeSV,
GenericSort sort) |
FinalReferenceCondition(SchemaVariable reference,
boolean negation)
the static reference condition checks if a suggested
instantiation for a schema variable denotes a static
reference.
|
FreeLabelInVariableCondition(SchemaVariable label,
SchemaVariable statement,
boolean negated) |
HasLoopInvariantCondition(ProgramSV loopStmtSV,
SchemaVariable modalitySV) |
JavaTypeToSortCondition(SchemaVariable exprOrTypeSV,
GenericSort sort,
boolean elemSort) |
LocalVariableCondition(SchemaVariable var,
boolean neg) |
LoopFreeInvariantCondition(ProgramSV loopStmtSV,
SchemaVariable modalitySV,
SchemaVariable invSV) |
LoopInvariantCondition(ProgramSV loopStmtSV,
SchemaVariable modalitySV,
SchemaVariable invSV) |
LoopVariantCondition(ProgramSV loopStmtSV,
SchemaVariable variantSV) |
MayExpandMethodCondition(SchemaVariable methodName,
SchemaVariable args,
boolean negation) |
MayExpandMethodCondition(SchemaVariable receiver,
SchemaVariable methname,
SchemaVariable args,
boolean negation)
Instantiate a new variable condition.
|
NewJumpLabelCondition(SchemaVariable sv) |
SimplifyIfThenElseUpdateCondition(FormulaSV phi,
UpdateSV u1,
UpdateSV u2,
FormulaSV commonFormula,
SchemaVariable result) |
StaticFieldCondition(SchemaVariable field,
boolean negated) |
StaticMethodCondition(SchemaVariable caller,
SchemaVariable methname,
SchemaVariable args,
boolean negation)
the static reference condition checks if a suggested
instantiation for a schema variable denotes a static method
call.
|
StaticReferenceCondition(SchemaVariable reference,
boolean negation)
the static reference condition checks if a suggested
instantiation for a schema variable denotes a static
reference.
|
StoreTermInCondition(SchemaVariable resultVarSV,
Term term) |
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
ProgramSVEntry.key()
returns the SchemaVariable to be instantiated
|
SchemaVariable |
SVInstantiations.lookupVar(Name name) |
Modifier and Type | Method and Description |
---|---|
ImmutableMap<SchemaVariable,Term> |
TacletInstantiations.instantiations() |
ImmutableMap<SchemaVariable,InstantiationEntry<?>> |
SVInstantiations.interesting() |
ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>> |
SVInstantiations.lookupEntryForSV(Name name) |
java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> |
SVInstantiations.pairIterator()
returns iterator of the mapped pair (SchemaVariables, InstantiationEntry>)
|
java.util.Iterator<SchemaVariable> |
SVInstantiations.svIterator()
returns iterator of the SchemaVariables that have an instantiation
|
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ImmutableArray<TermLabel> labels,
Services services) |
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
adds the given pair to the instantiations.
|
ProgramSVInstantiation |
ProgramSVInstantiation.add(SchemaVariable sv,
JavaProgramElement prgElement)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ProgramElement pe,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ProgramList pes,
Services services) |
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
Term subst,
Services services)
adds the given pair to the instantiations.
|
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
Name name,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
ProgramElement pe,
Services services) |
SVInstantiations |
SVInstantiations.addInteresting(SchemaVariable sv,
Term subst,
Services services) |
SVInstantiations |
SVInstantiations.addInterestingList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
SVInstantiations |
SVInstantiations.addList(SchemaVariable sv,
java.lang.Object[] list,
Services services) |
java.lang.Boolean |
GenericSortInstantiations.checkSorts(SchemaVariable sv,
InstantiationEntry<?> p_entry) |
static GenericSortCondition |
GenericSortCondition.createCondition(SchemaVariable sv,
InstantiationEntry<?> p_entry)
Create the condition that needs to be fulfilled for the given
instantiation of a metavariable to be correct, i.e.
|
JavaProgramElement |
ProgramSVInstantiation.getInstantiation(SchemaVariable sv)
returns the instantiation of the given SchemaVariable
|
java.lang.Object |
SVInstantiations.getInstantiation(SchemaVariable sv)
returns the instantiation of the given SchemaVariable
|
InstantiationEntry<?> |
SVInstantiations.getInstantiationEntry(SchemaVariable sv)
returns the instantiation of the given SchemaVariable
|
Sort |
GenericSortInstantiations.getRealSort(SchemaVariable p_sv,
TermServices services) |
Term |
SVInstantiations.getTermInstantiation(SchemaVariable sv,
ExecutionContext ec,
Services services)
returns the instantiation of the given SchemaVariable as Term.
|
boolean |
ProgramSVInstantiation.isInstantiated(SchemaVariable sv)
returns true iff the sv has been instantiated already
|
boolean |
SVInstantiations.isInstantiated(SchemaVariable sv)
returns true iff the sv has been instantiated already
|
SVInstantiations |
SVInstantiations.makeInteresting(SchemaVariable sv,
Services services)
adds the schemvariable to the set of interesting ones
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ImmutableArray<ProgramElement> pes,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
InstantiationEntry<?> entry,
Services services)
replaces the given pair in the instantiations.
|
ProgramSVInstantiation |
ProgramSVInstantiation.replace(SchemaVariable sv,
JavaProgramElement prgElement)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
ProgramElement pe,
Services services)
replaces the given pair in the instantiations.
|
SVInstantiations |
SVInstantiations.replace(SchemaVariable sv,
Term term,
Services services)
replaces the given pair in the instantiations.
|
Modifier and Type | Method and Description |
---|---|
static GenericSortInstantiations |
GenericSortInstantiations.create(java.util.Iterator<ImmutableMapEntry<SchemaVariable,InstantiationEntry<?>>> p_instantiations,
ImmutableList<GenericSortCondition> p_conditions,
Services services)
Create an object that solves the conditions given by the
instantiation iterator, i.e.
|
Constructor and Description |
---|
ProgramSVEntry(SchemaVariable key,
JavaProgramElement value)
creates a new entry encapsulating the SchemaVariable key and its
JavaProgramElement instantiation value
|
Constructor and Description |
---|
TacletInstantiations(Taclet rule,
ImmutableMap<SchemaVariable,Term> instantiations) |
Modifier and Type | Method and Description |
---|---|
MatchConditions |
LegacyTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
LegacyTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Method and Description |
---|---|
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
TacletMatchProgram.getMatchInstructionForSV(SchemaVariable op)
returns the instruction for the specified variable
|
Modifier and Type | Method and Description |
---|---|
MatchConditions |
VMTacletMatcher.checkVariableConditions(SchemaVariable var,
SVSubstitute instantiationCandidate,
MatchConditions matchCond,
Services services)
checks if the conditions for a correct instantiation are satisfied
|
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
TacletMatchProgram.getMatchInstructionForSV(SchemaVariable op)
returns the instruction for the specified variable
|
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
ProgramElement pe,
MatchConditions matchCond,
Services services)
|
MatchConditions |
VMTacletMatcher.matchSV(SchemaVariable sv,
Term term,
MatchConditions matchCond,
Services services)
|
Modifier and Type | Class and Description |
---|---|
class |
MatchSchemaVariableInstruction<SV extends SchemaVariable> |
Modifier and Type | Method and Description |
---|---|
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
Instruction.matchFormulaSV(FormulaSV sv) |
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
Instruction.matchModalOperatorSV(ModalOperatorSV sv) |
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
Instruction.matchProgramSV(ProgramSV sv) |
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
Instruction.matchTermSV(TermSV sv) |
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
Instruction.matchUpdateSV(UpdateSV sv) |
static MatchSchemaVariableInstruction<? extends SchemaVariable> |
Instruction.matchVariableSV(VariableSV sv) |
Modifier and Type | Method and Description |
---|---|
SchemaVariable |
UnwindLoop.getInnerLabelSV()
Deprecated.
|
SchemaVariable |
UnwindLoop.getOuterLabelSV()
Deprecated.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<SchemaVariable> |
WhileInvariantTransformer.neededInstantiations(ProgramElement originalLoop,
SVInstantiations svInst)
returns the schemavariables that are needed to transform the given loop.
|
ImmutableList<SchemaVariable> |
UnwindLoop.neededInstantiations(SVInstantiations svInst)
return a list of the SV that are relevant to this UnwindLoop
|
ImmutableList<SchemaVariable> |
ForToWhile.neededInstantiations(SVInstantiations svInst)
return a list of the SV that are relevant to this UnwindLoop
|
ImmutableList<SchemaVariable> |
ProgramTransformer.neededInstantiations(SVInstantiations svInst)
get a list of schema variables that are needed by this entity when
working given a SV instantiation set.
|
ImmutableList<SchemaVariable> |
ProgramTransformer.needs()
get a list of schema variables that are needed by this entity when
working given a SV instantiation set.
|
Modifier and Type | Method and Description |
---|---|
void |
WhileLoopTransformation.performActionOnSchemaVariable(SchemaVariable sv) |
Constructor and Description |
---|
ArrayPostDecl(SchemaVariable sv) |
ConstructorCall(Name name,
SchemaVariable newObjectSV,
ProgramElement consRef) |
ConstructorCall(SchemaVariable newObjectSV,
ProgramElement consRef)
creates the metaconstruct
|
ExpandMethodBody(SchemaVariable sv) |
ForToWhile(SchemaVariable innerLabel,
SchemaVariable outerLabel,
Statement loop)
creates an loop to while - ProgramTransformer
|
InitArrayCreation(SchemaVariable newObjectSV,
ProgramElement newExpr) |
MethodCall(Name name,
ProgramSV ec,
SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
MethodCall(ProgramSV ec,
SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
MethodCall(SchemaVariable result,
ProgramElement body)
creates the methodcall-MetaConstruct
|
MultipleVarDecl(SchemaVariable sv) |
PostWork(SchemaVariable newObjectSV) |
SwitchToIf(SchemaVariable _switch)
creates a switch-to-if ProgramTransformer
|
UnwindLoop(SchemaVariable innerLabel,
SchemaVariable outerLabel,
LoopStatement loop)
creates an unwind-loop ProgramTransformer
|
Modifier and Type | Field and Description |
---|---|
protected ImmutableMap<SchemaVariable,TacletPrefix> |
TacletPrefixBuilder.prefixMap |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<SchemaVariable> |
TacletGoalTemplate.addedProgVars()
returns the set of schemavaroable whose instantiations will be
added to the sequent namespace
|
java.util.Set<SchemaVariable> |
RewriteTacletBuilderSchemaVarCollector.collectSchemaVariables() |
ImmutableMap<SchemaVariable,TacletPrefix> |
TacletPrefixBuilder.getPrefixMap() |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVarsNew(SchemaVariable v,
KeYJavaType type)
adds a new new variable to the variable conditions of
the Taclet: v is new and has the given type
|
void |
TacletBuilder.addVarsNew(SchemaVariable v,
SchemaVariable peerSV)
adds a new new variable to the variable conditions of
the Taclet: v is new and has the same type as peerSV
|
void |
TacletBuilder.addVarsNewDependingOn(SchemaVariable v0,
SchemaVariable v1)
Add a "v0 depending on v1"-statement.
|
void |
TacletBuilder.addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0,
SchemaVariable... v1) |
void |
TacletBuilder.addVarsNotFreeIn(SchemaVariable v0,
SchemaVariable v1)
adds a new NotFreeIn variable pair to the variable conditions of
the Taclet: v0 is not free in v1.
|
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
Modifier and Type | Method and Description |
---|---|
void |
TacletBuilder.addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0,
java.lang.Iterable<? extends SchemaVariable> v1) |
void |
TacletBuilder.addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0,
java.lang.Iterable<? extends SchemaVariable> v1) |
void |
TacletBuilder.addVarsNotFreeIn(java.lang.Iterable<? extends SchemaVariable> v0,
SchemaVariable... v1) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
Constructor and Description |
---|
AntecSuccTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Sequent replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
RewriteTacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
Term replacewith,
ImmutableSet<SchemaVariable> pvs)
creates new Goaldescription
|
TacletGoalTemplate(Sequent addedSeq,
ImmutableList<Taclet> addedRules,
ImmutableSet<SchemaVariable> addedProgVars)
creates new Goaldescription
|
Modifier and Type | Method and Description |
---|---|
void |
DefaultTacletSetTranslation.eventFormulaSV(SchemaVariable formula) |
void |
TranslationListener.eventFormulaSV(SchemaVariable formula)
Called when the translator finds a schema variable of type formula.
|
Modifier and Type | Method and Description |
---|---|
void |
UserDefinedSymbols.addSchemaVariable(SchemaVariable symbol) |
Copyright © 2003-2019 The KeY-Project.