Package | Description |
---|---|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
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.
|
Modifier and Type | Method and Description |
---|---|
SemisequentChangeInfo |
SequentChangeInfo.getSemisequentChangeInfo(boolean antec) |
SemisequentChangeInfo |
Semisequent.insert(int idx,
ImmutableList<SequentFormula> insertionList)
inserts the elements of the list at the specified index
performing redundancy checks
|
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(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.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(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.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
|
SemisequentChangeInfo |
Semisequent.remove(int idx)
removes an element
|
SemisequentChangeInfo |
Semisequent.replace(int idx,
ImmutableList<SequentFormula> replacements)
replaces the formula at position
idx by the given list of formulas |
SemisequentChangeInfo |
Semisequent.replace(int idx,
SequentFormula sequentFormula)
replaces the idx-th formula by sequentFormula
|
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
|
SemisequentChangeInfo |
Semisequent.replace(PosInOccurrence pos,
SequentFormula sequentFormula)
replaces the element at place idx with sequentFormula
|
Modifier and Type | Method and Description |
---|---|
void |
SemisequentChangeInfo.combine(SemisequentChangeInfo succ)
This method combines this change information from this info and its successor.
|
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.
|
Modifier and Type | Method and Description |
---|---|
SemisequentChangeInfo |
ProgVarReplacer.replace(Semisequent s)
replaces in a semisequent
|
Modifier and Type | Method and Description |
---|---|
static void |
ProgVarReplacer.mergeSemiCIs(SemisequentChangeInfo base,
SemisequentChangeInfo next,
int idx)
merges "next" into "base"
precondition:
"next" is the result of replacing in "base" the formula at position
"idx" by calling Semisequent.replace()
(this implies that "next" contains exactly one removed and one added
formula)
|
Copyright © 2003-2019 The KeY-Project.