See: Description
| Interface | Description |
|---|---|
| IntIterator |
implemented by iterators of primitive type int
|
| NameCreationInfo | |
| Named |
This interface has to be implemented by all logic signature elements, which
are identified by their name.
|
| PIOPathIterator |
This interface represents an iterator, iterating the nodes on the
path between the root of a term and a position within the term,
given by a
PosInOccurrence-object |
| ProgramConstruct |
A type that implement this interface can be used in all java
programs instead of an expression or statement.
|
| ProgramInLogic |
represents something in logic that originates from a program like
queries, program variables and therefore has a KeYJavaType
|
| ProgramPrefix |
this interface is implemented by program elements that may be matched
by the inactive program prefix
|
| Sorted | |
| Term |
In contrast to the distinction of formulas and terms as made by most of the
inductive definitions of the syntax of a logic, an instance of this class can
stand for a term or a formula.
|
| TermOrdering |
Interface for term ordering
|
| TermServices |
This interface defines the basic functionalities of services
required to construct
Terms. |
| Visitor |
| Class | Description |
|---|---|
| BooleanContainer |
BooleanContainer wraps primitive bool
|
| BoundVariableTools |
Some generally useful tools for dealing with arrays of bound variables
|
| BoundVarsVisitor |
Visitor traversing a term and collecting all variables that occur bound.
|
| Choice | |
| ClashFreeSubst | |
| ClashFreeSubst.VariableCollectVisitor |
A Visitor class to collect all (not just the free) variables
occurring in a term.
|
| DefaultVisitor |
This abstract Vistor class declares the interface for a common term visitor.
|
| FormulaChangeInfo |
This class is used to hold information about modified formulas.
|
| InnerVariableNamer |
Implements "inner renaming", i.e. renaming - if a new variable entering the
globals causes a name clash - this "inner" variable, and leaving the clashing
"outer" one untouched.
|
| JavaBlock | |
| LabeledTermImpl |
The labeled term class is used for terms that have a label
attached.
|
| LexPathOrdering | |
| LexPathOrdering.CacheKey | |
| LexPathOrdering.CompRes | |
| LexPathOrdering.FunctionWeighter |
Explicit ordering for different kinds of function symbols; symbols like
C::
|
| LexPathOrdering.LiteralWeighter |
Explicit ordering of literals (symbols assigned a weight by this
class are regarded as smaller than all other symbols)
|
| LexPathOrdering.Weighter |
Base class for metrics on symbols that are used to construct an ordering
|
| MethodStackInfo | |
| MultiRenamingTable | |
| Name |
A Name object is created to represent the name of an object which usually
implements the interface
Named. |
| Namespace<E extends Named> |
A Namespace keeps track of already used
Names and the objects
carrying these names. |
| NamespaceSet | |
| OpCollector |
Collects all operators occurring in the traversed term.
|
| PosInOccurrence |
This class describes a position in an occurrence of a term.
|
| PosInProgram |
this class describes the position of a statement in a program.
|
| PosInProgram.PosArrayIntIterator | |
| PosInTerm |
Describes the position within a term by a sequence of integers.
|
| PosInTerm.PiTIterator | |
| ProgramElementName | |
| RenameTable | |
| RenameTable.EmptyRenameTable | |
| RenamingTable | |
| Semisequent |
This class represents the succedent or antecendent part of a
sequent.
|
| Semisequent.Empty | |
| SemisequentChangeInfo |
Records the changes made to a semisequent.
|
| Sequent |
This class represents a sequent.
|
| Sequent.NILSequent | |
| Sequent.SequentIterator | |
| SequentChangeInfo |
Records the changes made to a sequent.
|
| SequentFormula |
A sequent formula is a wrapper around a formula that occurs
as top level formula in a sequent.
|
| SingleRenamingTable | |
| SingleRenamingTable.SingleIterator | |
| SortCollector | |
| TermBuilder |
Use this class if you intend to build complex terms by hand.
|
| TermFactory |
The TermFactory is the only way to create terms using constructors
of class Term or any of its subclasses.
|
| TermImpl |
The currently only class implementing the Term interface.
|
| VariableNamer |
Responsible for program variable naming issues.
|
| VariableNamer.BasenameAndIndex |
tuple of a basename and an index
|
| VariableNamer.CustomJavaASTWalker |
a customized JavaASTWalker
|
| VariableNamer.IndProgramElementName |
ProgramElementName carrying an additional index
|
| VariableNamer.PermIndProgramElementName |
regular indexed ProgramElementName
|
| VariableNamer.TempIndProgramElementName |
temporary indexed ProgramElementName
|
| WaryClashFreeSubst |
| Enum | Description |
|---|---|
| TermImpl.ThreeValuedTruth |
| Exception | Description |
|---|---|
| TermCreationException |
provides a representation for the term and sequent
structure. The structure of a term is defined in Term. Subclasses of Term provide representations for special
kinds of terms. However, these subclasses are supposed to be not
directly accessed. Instead, Term
provides methods for all the methods of the
subclasses. Moreover, Terms (or
their subclasses) are supposed to be never constructed by
constructors of their own, but by instances of TermFactory.
The function of Terms (e.g., if
they represent a conjunction of subterms, a quantified
formula,...) is only determined by an Operator that is assigned to a Term when the Term is constructed.
Sequents consist of two Semisequents which represent a
duplicate-free list of a SequentFormulas. The latter consist of
a de.uka.ilkd.key.logic.Constraint and a Term of a special sort Sort.FORMULA.
Sequents and Terms are immutable.
Last modified: Wed Dec 4 15:11:14 MET 2002