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.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.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.symbolic_execution.util |
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 | Field and Description |
---|---|
static Semisequent |
Semisequent.EMPTY_SEMISEQUENT
the empty semisequent (using singleton pattern)
|
Modifier and Type | Method and Description |
---|---|
Semisequent |
Sequent.antecedent()
returns semisequent of the antecedent to work with
|
Semisequent |
SemisequentChangeInfo.semisequent()
returns the semisequent that is the result of the change
operation
|
Semisequent |
Sequent.succedent()
returns semisequent of the succedent to work with
|
Modifier and Type | Method and Description |
---|---|
static Sequent |
Sequent.createAnteSequent(Semisequent ante)
creates a new Sequent with empty succedent
|
static Sequent |
Sequent.createSequent(Semisequent ante,
Semisequent succ)
creates a new Sequent
|
static Sequent |
Sequent.createSuccSequent(Semisequent succ)
creates a new Sequent with empty antecedent
|
Modifier and Type | Method and Description |
---|---|
protected void |
TermLabelManager.refactorSemisequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Semisequent semisequent,
boolean inAntec,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Performs a
TermLabel refactoring on the given Semisequent . |
Modifier and Type | Method and Description |
---|---|
Semisequent |
ExpressionBuilder.visitSemisequent(KeYParser.SemisequentContext ctx) |
Modifier and Type | Method and Description |
---|---|
void |
LogicPrinter.printSemisequent(Semisequent semiseq)
Pretty-prints a Semisequent.
|
static java.lang.String |
LogicPrinter.quickPrintSemisequent(Semisequent s,
Services services)
Converts a semisequent to a string.
|
Modifier and Type | Method and Description |
---|---|
SemisequentChangeInfo |
ProgVarReplacer.replace(Semisequent s)
replaces in a semisequent
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<IfFormulaInstantiation> |
IfFormulaInstantiationCache.get(boolean antec,
Semisequent s) |
void |
IfFormulaInstantiationCache.put(boolean antec,
Semisequent s,
ImmutableList<IfFormulaInstantiation> value) |
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 ImmutableList<SequentFormula> |
TacletExecutor.instantiateSemisequent(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
instantiates the given semisequent with the instantiations found in
Matchconditions
|
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
|
Modifier and Type | Method and Description |
---|---|
protected boolean |
NonDuplicateAppFeature.semiSequentContains(Semisequent semisequent,
SequentFormula cfma) |
protected boolean |
EqNonDuplicateAppFeature.semiSequentContains(Semisequent semisequent,
SequentFormula cfma) |
protected boolean |
InfFlowContractAppFeature.semiSequentContains(Semisequent semisequent,
SequentFormula cfma)
Check whether a semisequent contains a formula.
|
protected abstract boolean |
AbstractNonDuplicateAppFeature.semiSequentContains(Semisequent semisequent,
SequentFormula cfma)
Check whether a semisequent contains a formula.
|
Modifier and Type | Method and Description |
---|---|
static PosInOccurrence |
SymbolicExecutionUtil.findModalityWithMaxSymbolicExecutionLabelId(Semisequent semisequent,
boolean inAntec)
Searches the modality
Term with the maximal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Semisequent . |
static PosInOccurrence |
SymbolicExecutionUtil.findModalityWithMinSymbolicExecutionLabelId(Semisequent semisequent,
boolean inAntec)
Searches the modality
PosInOccurrence with the minimal SymbolicExecutionTermLabel ID
SymbolicExecutionTermLabel.getId() in the given Semisequent . |
static ImmutableList<Term> |
SymbolicExecutionUtil.listSemisequentTerms(Semisequent semisequent)
Lists the
Term s contained in the given Semisequent . |
Copyright © 2003-2019 The KeY-Project.