| de.uka.ilkd.key.logic |
|
provides a representation for the term and sequent
structure. The structure of a term is defined in {@link
de.uka.ilkd.key.logic.Term}. Subclasses of {@link
de.uka.ilkd.key.logic.Term} provide representations for special
kinds of terms. However, these subclasses are supposed to be not
directly accessed. Instead, {@link de.uka.ilkd.key.logic.Term}
provides methods for all the methods of the
subclasses. Moreover, {@link de.uka.ilkd.key.logic.Term}s (or
their subclasses) are supposed to be never constructed by
constructors of their own, but by instances of {@link
de.uka.ilkd.key.logic.TermFactory}.
The function of {@link de.uka.ilkd.key.logic.Term}s (e.g., if
they represent a conjunction of subterms, a quantified
formula,...) is only determined by an {@link
de.uka.ilkd.key.logic.op.Operator} that is assigned to a {@link
de.uka.ilkd.key.logic.Term} when the {@link
de.uka.ilkd.key.logic.Term} is constructed.
{@link de.uka.ilkd.key.logic.Sequent}s consist of two {@link
de.uka.ilkd.key.logic.Semisequent}s which represent a
duplicate-free list of a {@link
de.uka.ilkd.key.logic.ConstrainedFormula}s. The latter consist of
a {@link de.uka.ilkd.key.logic.Constraint} and a {@link
de.uka.ilkd.key.logic.Term} of a special sort {@link
de.uka.ilkd.key.logic.sort.Sort#FORMULA}.
{@link de.uka.ilkd.key.logic.Sequent}s and {@link
de.uka.ilkd.key.logic.Term}s are immutable.
Last modified: Wed Dec 4 15:11:14 MET 2002
|
| Java Source File Name | Type | Comment |
| AnonymisingUpdateFactory.java | Class | Creates anonymising updates for sets of locations, i.e. |
| AtPreNamespace.java | Class | |
| AttributeElementName.java | Class | |
| Axiom.java | Class | Axiom inherits from Term. |
| BasicLocationDescriptor.java | Class | |
| BooleanContainer.java | Class | |
| BoundVariableTools.java | Class | |
| BoundVarsTerm.java | Class | Used for OCL Simplification.
A BoundVarsTerm is an object that contains an Operator and several subterms.
It can also have a number of bound variables for each subterm. |
| BoundVarsVisitor.java | Class | Visitor traversing a term and collecting all variables that occur bound. |
| CascadeDepthTermOrdering.java | Class | Term ordering, comparing the maximum depths of terms and contained
variables; following definition 5.14 in the script "Automatisches
Beweisen", Bernhard Beckert, Reiner Haehnle
This ordering has the possibility to refer to a secundary ordering
upon terms having the same depths (i.e. |
| CascadeTermOrdering.java | Class | |
| CExProblem.java | Class | This class contains a an ADT and a conjecture and is the input for the call to Mgtp.
The package de.uka.ilkd.key.counterexample uses this as input for the generation
of the counterexample calculus which is then given as input to Mgtp. |
| Choice.java | Class | |
| ClashFreeSubst.java | Class | |
| CollisionDeletingSubstitutionTermApplier.java | Class | visitor for execPostOrder of
de.uka.ilkd.key.logic.Term . |
| ConstrainedFormula.java | Class | This class contains a term of type bool with the constraints it
has to satisfy. |
| Constraint.java | Interface | Abstract constraint interface for constraints offering unification
of terms and joins. |
| ConstraintContainer.java | Class | |
| DepthCollector.java | Class | This class is used to collect all appearing metavariables and logic
variables in a term, together with their maximum term depth. |
| DepthTermOrdering.java | Class | |
| EqualityConstraint.java | Class | This class implements a persistent constraint. |
| EverythingLocationDescriptor.java | Class | |
| FormulaChangeInfo.java | Class | This class is used to hold information about modified formulas. |
| FunctionNameFunctionSymbolMapper.java | Class | |
| IfExThenElseTerm.java | Class | |
| InnerVariableNamer.java | Class | |
| IntersectionConstraint.java | Class | Class representing the intersection of a set of constraints
(i.e. |
| IntIterator.java | Interface | |
| JavaBlock.java | Class | |
| LexPathOrdering.java | Class | |
| LocationDescriptor.java | Interface | |
| LVRCollector.java | Class | This class is used to collect all appearing variables that can
represent logic variables in a term. |
| MetavariableDeliverer.java | Class | |
| MethodStackInfo.java | Class | |
| MultiRenamingTable.java | Class | |
| MVCollector.java | Class | This class is used to collect all appearing metavariables in a
term. |
| Name.java | Class | A Name object is created to represent the name of an object which
usually implements the interface
Named . |
| NameCreationInfo.java | Interface | |
| Named.java | Interface | This interface has to be implemented by all logic signature elements, which
are identified by their name. |
| Namespace.java | Class | A Namespace keeps track of already used
Name s and the objects
carrying these names. |
| NamespaceSet.java | Class | |
| NameTermOrdering.java | Class | |
| OpCollector.java | Class | Collects all operators occuring in the traversed term. |
| OpTerm.java | Class | An OpTerm is an object that contains an Operator and several subterms. |
| PairOfTermArrayAndBoundVarsArray.java | Class | A structure for storing the arguments to an Operator
when creating a Term. |
| PIOPathIterator.java | Interface | |
| PosInOccurrence.java | Class | This class describes a position in an occurrence of a term. |
| PosInProgram.java | Class | this class describes the position of a statement in a program. |
| PosInTerm.java | Class | |
| PostFormulaTransformer.java | Class | Only for use in the generation of the translation of an OCL constaint !!!
creates a mapping of the names of functions (as strings) to the
corresponding functionsymbol (object) ... |
| ProgramConstruct.java | Interface | A type that implement this interface can be used in all java
programs instead of an expression or statement. |
| ProgramElementName.java | Class | |
| ProgramInLogic.java | Interface | |
| ProgramPrefix.java | Interface | |
| ProgramTerm.java | Class | |
| QuantifierTerm.java | Class | |
| QuanUpdateTerm.java | Class | |
| RenameTable.java | Class | |
| RenamingTable.java | Class | |
| Semisequent.java | Class | This class represents the succedent or antecendent part of a
sequent. |
| SemisequentChangeInfo.java | Class | Records the changes made to a semisequent. |
| Sequent.java | Class | This class represents a sequent. |
| SequentChangeInfo.java | Class | Records the changes made to a sequent. |
| ShadowReplaceVisitor.java | Class | |
| SingleRenamingTable.java | Class | |
| SubstitutionTerm.java | Class | A SubstitutionTerm is an object that contains an Operator two subterms. |
| Term.java | Class | In contrast to the distinction of formulas and terms as made by most of the
inductive definition of the syntax of a logic, an instance of this class can
stand for a term or a formula. |
| TermBuilder.java | Class | Use this class if you intend to build complex terms by hand. |
| TermCreationException.java | Class | |
| TermFactory.java | Class | The TermFactory is the only way to create terms using constructos of
class Term or any of its subclasses. |
| TermOrdering.java | Interface | |
| TermWithBoundVars.java | Class | A TermWithBoundVars is an object that contains a Term and 0, 1,
or 2 QuantifiableVariable that are bound in the Term. |
| TestClashFreeSubst.java | Class | |
| TestConstraint.java | Class | |
| TestNamespace.java | Class | |
| TestPosInOcc.java | Class | |
| TestSemisequent.java | Class | |
| TestSyntacticalReplaceVisitor.java | Class | |
| TestTerm.java | Class | |
| TestTermFactory.java | Class | |
| TestTermOrdering.java | Class | |
| TestUpdateFactory.java | Class | |
| TestUpdatetermNormalisation.java | Class | |
| TestVariableNamer.java | Class | |
| UpdateFactory.java | Class | Factory providing the update constructors that are described in "Sequential,
Parallel and Quantified Updates of First-Order Structures". |
| UpdateTerm.java | Class | |
| VariableNamer.java | Class | Responsible for program variable naming issues. |
| Visitor.java | Class | This abstract Vistor class declares the interface for a common term visitor. |
| WaryClashFreeSubst.java | Class | |