Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.gui.nodeviews | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
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.join | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.strategy.termgenerator | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.symbolic_execution.strategy | |
de.uka.ilkd.key.symbolic_execution.util |
Constructor and Description |
---|
SearchNode(SequentFormula[] pattern,
int succAntPos,
ImmutableList<IfFormulaInstantiation> antec,
ImmutableList<IfFormulaInstantiation> succ) |
Modifier and Type | Method and Description |
---|---|
Node |
CurrentGoalView.jumpToIntroduction(Node node,
SequentFormula form)
given a node and a sequent formula, returns the first node
among the node's parents that contains the sequent formula @form.
|
Modifier and Type | Method and Description |
---|---|
SequentFormula |
Semisequent.get(int idx)
gets the element at a specific index
|
SequentFormula |
Semisequent.getFirst() |
SequentFormula |
Sequent.getFormulabyNr(int formulaNumber) |
SequentFormula |
FormulaChangeInfo.getNewFormula() |
SequentFormula |
FormulaChangeInfo.getOriginalFormula() |
SequentFormula |
PosInOccurrence.sequentFormula()
returns the SequentFormula that determines the occurrence of
this PosInOccurrence
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<SequentFormula> |
SequentChangeInfo.addedFormulas()
The formulas added to the sequent are returned as a concatenated list of
the formulas added to each semisequent.
|
ImmutableList<SequentFormula> |
SemisequentChangeInfo.addedFormulas()
returns the list of all added constrained formulas
|
ImmutableList<SequentFormula> |
SequentChangeInfo.addedFormulas(boolean antec)
The formulas added to one of the semisequents are returned.
|
ImmutableList<SequentFormula> |
Sequent.asList()
Returns a list containing every
SequentFormula in this sequent. |
ImmutableList<SequentFormula> |
Semisequent.asList() |
ImmutableList<SequentFormula> |
SemisequentChangeInfo.getFormulaList()
returns the list of constrained formula of the new semisequent
|
java.util.Iterator<SequentFormula> |
Sequent.iterator()
returns iterator about all ConstrainedFormulae of the sequent
|
java.util.Iterator<SequentFormula> |
Semisequent.iterator()
returns iterator about the elements of the sequent
|
ImmutableList<SequentFormula> |
SequentChangeInfo.rejectedFormulas()
Returns the formulas that have been rejected when trying to add as being redundant.
|
ImmutableList<SequentFormula> |
SemisequentChangeInfo.rejectedFormulas()
returns a list of formulas that have been tried to add to
the semisequent but got rejected as they were redundant
|
ImmutableList<SequentFormula> |
SequentChangeInfo.rejectedFormulas(boolean antec)
Returns the formulas that have been rejected when trying to add as being redundant.
|
ImmutableList<SequentFormula> |
SequentChangeInfo.removedFormulas()
The formulas removed from the sequent are returned as a
concatenated list of the formulas removed from each semisequent.
|
ImmutableList<SequentFormula> |
SemisequentChangeInfo.removedFormulas()
returns the list of all removed constrained formulas
|
ImmutableList<SequentFormula> |
SequentChangeInfo.removedFormulas(boolean antec)
The formulas removed from one of the semisequents are returned.
|
Modifier and Type | Method and Description |
---|---|
void |
SemisequentChangeInfo.addedFormula(int idx,
SequentFormula cf)
logs an added formula at position idx
|
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(SequentFormula newCF,
PosInOccurrence p)
replaces the formula at the given position with another one (NOTICE:Sequent
determines index using identity (==) not equality.)
|
boolean |
Sequent.contains(SequentFormula form)
used to check whether this sequent contains a given sequent formula.
|
boolean |
Semisequent.contains(SequentFormula sequentFormula)
checks if the
SequentFormula occurs in this
Semisequent (identity check) |
boolean |
Semisequent.containsEqual(SequentFormula sequentFormula)
checks if a
SequentFormula is in this Semisequent
(equality check) |
int |
Sequent.formulaNumberInSequent(boolean inAntec,
SequentFormula cfma)
Computes the position of the given sequent formula on the proof sequent,
starting with one for the very first sequent formula.
|
int |
Semisequent.indexOf(SequentFormula sequentFormula)
returns the index of the given
SequentFormula or -1
if the sequent formula is not found. |
SemisequentChangeInfo |
Semisequent.insert(int idx,
SequentFormula sequentFormula)
inserts an element at a specified index performing redundancy
checks, this may result in returning same semisequent if
inserting would create redundancies
|
SemisequentChangeInfo |
Semisequent.insertFirst(SequentFormula sequentFormula)
inserts element at index 0 performing redundancy
checks, this may result in returning same semisequent if
inserting would create redundancies
|
SemisequentChangeInfo |
Semisequent.insertLast(SequentFormula sequentFormula)
inserts element at the end of the semisequent performing
redundancy checks, this may result in returning same
semisequent if inserting would create redundancies
|
void |
SemisequentChangeInfo.rejectedFormula(SequentFormula f)
adding formula f to the semisequent failed due to
a redundance check.
|
void |
SemisequentChangeInfo.removedFormula(int idx,
SequentFormula cf)
logs an added formula at position idx
|
SemisequentChangeInfo |
Semisequent.replace(int idx,
SequentFormula sequentFormula)
replaces the idx-th formula by sequentFormula
|
SemisequentChangeInfo |
Semisequent.replace(PosInOccurrence pos,
SequentFormula sequentFormula)
replaces the element at place idx with sequentFormula
|
PosInOccurrence |
PosInOccurrence.replaceConstrainedFormula(SequentFormula p_newFormula)
Replace the formula this object points to with the new formula given
|
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.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.)
|
SemisequentChangeInfo |
Semisequent.insert(int idx,
ImmutableList<SequentFormula> insertionList)
inserts the elements of the list at the specified index
performing redundancy checks
|
SemisequentChangeInfo |
Semisequent.insertFirst(ImmutableList<SequentFormula> insertions)
inserts element at index 0 performing redundancy
checks, this may result in returning same semisequent if
inserting would create redundancies
|
SemisequentChangeInfo |
Semisequent.insertLast(ImmutableList<SequentFormula> insertions)
inserts the formulas of the list at the end of the semisequent
performing redundancy checks, this may result in returning same
semisequent if inserting would create redundancies
|
SemisequentChangeInfo |
Semisequent.replace(int idx,
ImmutableList<SequentFormula> replacements)
replaces the formula at position
idx by the given list of formulas |
SemisequentChangeInfo |
Semisequent.replace(PosInOccurrence pos,
ImmutableList<SequentFormula> replacements)
replaces the element at place idx with the first element of the
given list and adds the rest of the list to the semisequent
behind the replaced formula
|
void |
SemisequentChangeInfo.setFormulaList(ImmutableList<SequentFormula> list)
sets the list of constrained formula containing all formulas of
the semisequent after the operation
|
Constructor and Description |
---|
FormulaChangeInfo(PosInOccurrence positionOfModification,
SequentFormula newFormula) |
PosInOccurrence(SequentFormula sequentFormula,
PosInTerm posInTerm,
boolean inAntec) |
Semisequent(SequentFormula seqFormula)
creates a new Semisequent with the Semisequent elements in
seqList
|
Constructor and Description |
---|
SemisequentChangeInfo(ImmutableList<SequentFormula> formulas) |
Modifier and Type | Method and Description |
---|---|
protected void |
TermLabelManager.mergeLabels(SequentChangeInfo currentSequent,
Services services,
SequentFormula rejectedSF,
boolean inAntecedent)
|
Modifier and Type | Method and Description |
---|---|
Term |
RewriteCommand.getTermAtPos(SequentFormula sf,
PosInOccurrence pio)
Calculates term at the PosInOccurrence pio
|
Modifier and Type | Method and Description |
---|---|
SequentFormula |
SequentPrintFilterEntry.getFilteredFormula()
Formula to display
|
SequentFormula |
IdentitySequentPrintFilter.IdentityFilterEntry.getFilteredFormula()
Formula to display
|
SequentFormula |
ShowSelectedSequentPrintFilter.Entry.getFilteredFormula() |
SequentFormula |
SequentPrintFilterEntry.getOriginalFormula()
Original formula from sequent
|
SequentFormula |
IdentitySequentPrintFilter.IdentityFilterEntry.getOriginalFormula()
Original formula from sequent
|
SequentFormula |
ShowSelectedSequentPrintFilter.Entry.getOriginalFormula() |
Modifier and Type | Method and Description |
---|---|
protected SequentPrintFilterEntry |
IdentitySequentPrintFilter.filterFormula(SequentFormula sequentFormula) |
void |
LogicPrinter.printConstrainedFormula(SequentFormula cfma)
Pretty-prints a constrained formula.
|
Modifier and Type | Method and Description |
---|---|
SequentFormula |
ProgVarReplacer.replace(SequentFormula cf)
replaces in a constrained formula
|
Modifier and Type | Method and Description |
---|---|
void |
Goal.addFormula(SequentFormula cf,
boolean inAntec,
boolean first)
adds a formula to the antecedent or succedent of a
sequent.
|
void |
Goal.addFormula(SequentFormula cf,
PosInOccurrence p)
adds a formula to the sequent before the given position
and informs the rule application index about this change
|
void |
Goal.changeFormula(SequentFormula cf,
PosInOccurrence p)
replaces a formula at the given position
and informs the rule application index about this change
|
SequentFormula |
ProgVarReplacer.replace(SequentFormula cf)
replaces in a constrained formula
|
Modifier and Type | Method and Description |
---|---|
SequentFormula |
ProspectivePartner.getFormula(int i) |
SequentFormula |
ProspectivePartner.getFormulaForHiding() |
Constructor and Description |
---|
ProspectivePartner(Term commonFormula,
Node node1,
SequentFormula formula1,
Term update1,
Node node2,
SequentFormula formula2,
Term update2)
Constructs a new prospective partner object, i.e.
|
Modifier and Type | Method and Description |
---|---|
SequentFormula |
IfFormulaInstSeq.getConstrainedFormula() |
SequentFormula |
IfFormulaInstantiation.getConstrainedFormula() |
SequentFormula |
IfFormulaInstDirect.getConstrainedFormula() |
SequentFormula |
RewriteTaclet.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
SequentFormula |
Taclet.TacletLabelHint.getSequentFormula()
Returns the optional
SequentFormula contained in Taclet.TacletLabelHint.getSequent() . |
Constructor and Description |
---|
IfFormulaInstDirect(SequentFormula p_cf) |
IfFormulaInstSeq(Sequent p_seq,
boolean antec,
SequentFormula p_cf) |
TacletLabelHint(Taclet.TacletLabelHint labelHint,
SequentFormula sequentFormula)
Constructor.
|
Modifier and Type | Method and Description |
---|---|
SequentFormula |
RewriteTacletExecutor.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
Modifier and Type | Method and Description |
---|---|
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
|
Modifier and Type | Method and Description |
---|---|
static java.util.Set<SequentFormula> |
FormulaTermLabelRefactoring.getSequentFormulasToRefactor(TermLabelState state)
Returns the
SequentFormula s to refactor. |
Modifier and Type | Method and Description |
---|---|
static void |
FormulaTermLabelRefactoring.addSequentFormulaToRefactor(TermLabelState state,
SequentFormula sf)
Adds the given
SequentFormula for refactoring purpose. |
boolean |
TermLabelMerger.mergeLabels(SequentFormula existingSF,
Term existingTerm,
TermLabel existingLabel,
SequentFormula rejectedSF,
Term rejectedTerm,
TermLabel rejectedLabel,
java.util.List<TermLabel> mergedLabels)
Merges the existing and the rejected
TermLabel by updating the merged List . |
boolean |
FormulaTermLabelMerger.mergeLabels(SequentFormula existingSF,
Term existingTerm,
TermLabel existingLabel,
SequentFormula rejectedSF,
Term rejectedTerm,
TermLabel rejectedLabel,
java.util.List<TermLabel> mergedLabels)
Merges the existing and the rejected
TermLabel by updating the merged List . |
Modifier and Type | Method and Description |
---|---|
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
LocationVariable heap,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built, however with a smaller set of variables,
due to the nature of the jml statement.
|
SequentFormula |
StatementWellDefinedness.generateSequent(ProgramVariable self,
ProgramVariable exception,
ProgramVariable result,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
ImmutableSet<ProgramVariable> ps,
Term leadingUpdate,
Term localAnonUpdate,
Services services)
This is where the proof sequent is built.
|
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 |
---|---|
protected abstract java.util.Iterator<SequentFormula> |
SequentFormulasGenerator.generateForIt(Goal goal) |
Modifier and Type | Method and Description |
---|---|
protected static Term |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
FormulaTermLabel label,
boolean antecedentRuleApplication,
TermBuilder tb)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
protected static void |
TruthValueTracingUtil.checkForNewMinorIdsOSS(SequentFormula onlyChangedChildSF,
Term term,
Name termLabelName,
PosInOccurrence parentPio,
TermBuilder tb,
java.util.Map<java.lang.String,TruthValueTracingUtil.MultiEvaluationResult> results)
Checks if new minor IDs are available in case of
OneStepSimplifier usage. |
static boolean |
TruthValueTracingUtil.isPredicate(SequentFormula sequentFormula)
Checks if the given
SequentFormula is a predicate. |
protected static void |
TruthValueTracingUtil.listLabelReplacements(SequentFormula sf,
Name labelName,
java.lang.String labelId,
java.util.List<Term> resultToFill)
Lists all label replacements in the given
SequentFormula . |
Modifier and Type | Method and Description |
---|---|
protected static SequentFormula |
AbstractSideProofRule.replace(PosInOccurrence pio,
Term newTerm,
Services services)
|
Modifier and Type | Method and Description |
---|---|
protected void |
CutHeapObjectsTermGenerator.collectEqualityTerms(SequentFormula sf,
java.util.Set<Term> equalityTerms,
java.util.Set<Term> topTerms,
HeapLDT heapLDT,
Services services)
Computes all possible equality terms between objects in the given
SequentFormula . |
Modifier and Type | Method and Description |
---|---|
static int |
SymbolicExecutionUtil.checkSkolemEquality(SequentFormula sf)
Checks if the given
SequentFormula is a skolem equality. |
static Sequent |
SymbolicExecutionSideProofUtil.computeGeneralSequentToProve(Sequent goalSequent,
SequentFormula currentSF)
Computes a general
Sequent to prove in a side proof which
contains all SequentFormula of the original Sequent
except the given current SequentFormula and those which
contains modalities and queries. |
static boolean |
SymbolicExecutionSideProofUtil.containsIrrelevantThings(Services services,
SequentFormula sf,
java.util.Set<Operator> relevantThings)
Checks if the given
SequentFormula contains irrelevant things
(things which are not contained in the relevantThingsToProve and are no Java types) |
static boolean |
SymbolicExecutionSideProofUtil.containsModalityOrQuery(SequentFormula sf)
Checks if the given
SequentFormula contains a modality or query. |
static boolean |
SymbolicExecutionSideProofUtil.isIrrelevantCondition(Services services,
Sequent initialSequent,
java.util.Set<Operator> relevantThingsInSequentToProve,
SequentFormula sf)
Checks if the given
SequentFormula is a relevant condition. |
Copyright © 2003-2019 The KeY-Project.