Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule.executor | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
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.proofevent | |
de.uka.ilkd.key.rule.executor.javadl |
Modifier and Type | Method and Description |
---|---|
protected void |
InfFlowContractAppTacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services) |
Modifier and Type | Method and Description |
---|---|
SequentChangeInfo |
Sequent.addFormula(ImmutableList<SequentFormula> insertions,
boolean antec,
boolean first)
adds list of formulas to the antecedent (or succedent) of the sequent.
|
SequentChangeInfo |
Sequent.addFormula(ImmutableList<SequentFormula> insertions,
PosInOccurrence p)
adds the formulas of list insertions to the sequent starting at position p.
|
SequentChangeInfo |
Sequent.addFormula(SequentFormula cf,
boolean antec,
boolean first)
adds a formula to the antecedent (or succedent) of the sequent.
|
SequentChangeInfo |
Sequent.addFormula(SequentFormula cf,
PosInOccurrence p)
adds a formula to the sequent at the given position.
|
SequentChangeInfo |
Sequent.changeFormula(ImmutableList<SequentFormula> replacements,
PosInOccurrence p)
replaces the formula at position p with the head of the given list and adds
the remaining list elements to the sequent (NOTICE:Sequent determines index
using identity (==) not equality.)
|
SequentChangeInfo |
Sequent.changeFormula(SequentFormula newCF,
PosInOccurrence p)
replaces the formula at the given position with another one (NOTICE:Sequent
determines index using identity (==) not equality.)
|
static SequentChangeInfo |
SequentChangeInfo.createSequentChangeInfo(boolean antec,
SemisequentChangeInfo semiCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequent described by the
value of the selector antec (true selects antecedent; false selects
succedent) has changed.
|
static SequentChangeInfo |
SequentChangeInfo.createSequentChangeInfo(PosInOccurrence pos,
SemisequentChangeInfo semiCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequent described by position
pos has changed.
|
static SequentChangeInfo |
SequentChangeInfo.createSequentChangeInfo(SemisequentChangeInfo anteCI,
SemisequentChangeInfo sucCI,
Sequent result,
Sequent original)
creates a new sequent change info whose semisequents have changed.
|
SequentChangeInfo |
Sequent.removeFormula(PosInOccurrence p)
removes the formula at position p (NOTICE:Sequent determines index using
identity (==) not equality.)
|
Modifier and Type | Method and Description |
---|---|
void |
SequentChangeInfo.combine(SequentChangeInfo succ)
This method combines the change information from this info and its successor.
|
Modifier and Type | Method and Description |
---|---|
static SequentChangeInfo |
OriginTermLabel.removeOriginLabels(Sequent seq,
Services services)
Removes all
OriginTermLabel from the specified sequent. |
Modifier and Type | Method and Description |
---|---|
static void |
TermLabelManager.mergeLabels(SequentChangeInfo currentSequent,
Services services)
|
protected void |
TermLabelManager.mergeLabels(SequentChangeInfo currentSequent,
Services services,
SequentFormula rejectedSF,
boolean inAntecedent)
|
void |
TermLabelManager.mergeLabels(Services services,
SequentChangeInfo currentSequent)
|
Modifier and Type | Method and Description |
---|---|
SequentChangeInfo |
NodeInfo.getSequentChangeInfo() |
SequentChangeInfo |
ProgVarReplacer.replace(Sequent s)
replaces in a sequent
|
Modifier and Type | Method and Description |
---|---|
protected void |
Goal.fireSequentChanged(SequentChangeInfo sci)
informs all goal listeners about a change of the sequent
to reduce unnecessary object creation the necessary information is passed
to the listener as parameters and not through an event object.
|
void |
FormulaTagManager.sequentChanged(Goal source,
SequentChangeInfo sci) |
void |
RuleAppIndex.sequentChanged(Goal g,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
BuiltInRuleAppIndex.sequentChanged(Goal goal,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
TacletAppIndex.sequentChanged(Goal goal,
SequentChangeInfo sci)
called if a formula has been replaced
|
void |
GoalListener.sequentChanged(Goal source,
SequentChangeInfo sci)
informs the listener about a change that occured to the sequent of goal
|
SemisequentTacletAppIndex |
SemisequentTacletAppIndex.sequentChanged(SequentChangeInfo sci,
Services services,
TacletIndex tacletIndex,
NewRuleListener listener)
called if a formula has been replaced
|
void |
Goal.setSequent(SequentChangeInfo sci)
sets the sequent of the node
|
void |
NodeInfo.setSequentChangeInfo(SequentChangeInfo sequentChangeInfo) |
Modifier and Type | Field and Description |
---|---|
ImmutableList<SequentChangeInfo> |
NodeChangesHolder.scis |
Modifier and Type | Method and Description |
---|---|
void |
NodeChangesHolder.addSCI(SequentChangeInfo p_sci) |
void |
NodeChangeJournal.sequentChanged(Goal source,
SequentChangeInfo sci)
informs the listener about a change that occured to the sequent
of goal
|
Constructor and Description |
---|
NodeReplacement(Node p_node,
Node p_parent,
ImmutableList<SequentChangeInfo> p_changes) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<SequentChangeInfo> |
TacletExecutor.checkIfGoals(Goal p_goal,
ImmutableList<IfFormulaInstantiation> p_list,
MatchConditions p_matchCond,
int p_numberOfNewGoals)
Search for formulas within p_list that have to be proved by an
explicit assumes-goal, i.e.
|
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
protected void |
TacletExecutor.addToSucc(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds SequentFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent).
|
protected void |
RewriteTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
SuccTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
NoFindTacletExecutor.applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
TacletExecutor.applyAddProgVars(ImmutableSet<SchemaVariable> pvs,
SequentChangeInfo currentSequent,
Goal goal,
PosInOccurrence posOfFind,
Services services,
MatchConditions matchCond) |
protected void |
RewriteTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
SuccTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
TacletExecutor.replaceAtPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
MatchConditions matchCond,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp ruleApp,
Services services)
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
|
Copyright © 2003-2019 The KeY-Project.