| de.uka.ilkd.key.proof |
|
| Java Source File Name | Type | Comment |
| AndRuleFilter.java | Class | |
| AnyRuleSetTacletFilter.java | Class | Filter that selects taclets that belong to at least one
rule set, i.e. |
| ApplyTacletDialogModel.java | Class | |
| BalancedGoalChooserBuilder.java | Class | |
| BalancedLoopGC.java | Class | This goal chooser takes care of a balanced unwinding of loops
acorss different proof branches. |
| BuiltInRuleAppIndex.java | Class | |
| BuiltInRuleIndex.java | Class | Index for managing built-in-rules usch as integer decision or update
simplification rule. |
| CompoundProof.java | Class | |
| ConstraintTableEvent.java | Class | |
| ConstraintTableListener.java | Interface | |
| ConstraintTableModel.java | Class | |
| Counter.java | Class | |
| CountingBufferedInputStream.java | Class | |
| DefaultGoalChooser.java | Class | Helper class for managing a list of goals on which rules are applied.
The class provides methods for removing a goal, and for updating the internal
data structures after a rule has been applied. |
| DefaultGoalChooserBuilder.java | Class | |
| DiffMyers.java | Class | A class to compare vectors of objects. |
| FormulaTag.java | Class | Class whose instances represent tags to identify the formulas of sequents
persistently, i.e. |
| FormulaTagManager.java | Class | Class to manage the tags of the formulas of a sequent (node). |
| Goal.java | Class | A proof is represented as a tree of nodes containing sequents. |
| GoalChooserBuilder.java | Interface | |
| GoalListener.java | Interface | |
| IfChoiceModel.java | Class | |
| IfMismatchException.java | Class | |
| IGoalChooser.java | Interface | Interface to be implemented by classes in order to customize the goal selection
strategy of the automatic prover environment. |
| IHTacletFilter.java | Class | Filter that selects taclets using the method admissible of the
Taclet class, i.e. |
| InstantiationProposer.java | Interface | Provides proposals for schema variable instantiations. |
| InstantiationProposerCollection.java | Class | Composite of instantiation proposers. |
| ITermTacletAppIndexCache.java | Interface | The general interface for caches for accelerating
TermTacletAppIndex. |
| JavaModel.java | Class | |
| LoopInvariantProposer.java | Class | |
| MethodSpecTransformation.java | Class | Transformation according to Sect. |
| MissingInstantiationException.java | Class | |
| MissingSortException.java | Class | |
| ModelChangeListener.java | Interface | |
| ModelEvent.java | Class | |
| ModifiesParserHelper.java | Class | Parses modifies clauses. |
| NewRuleListener.java | Interface | |
| Node.java | Class | |
| NodeContents.java | Interface | |
| NodeInfo.java | Class | The node info object contains additional information about a node used to
give user feedback. |
| NotRuleFilter.java | Class | |
| NullNewRuleListener.java | Class | |
| OpReplacer.java | Class | Replaces operators in a term by other operators with the same signature,
or subterms of the term by other terms with the same sort. |
| PrefixTermTacletAppIndexCache.java | Class | The abstract superclass of caches for taclet app indexes that are separated
by different prefixes of bound variables. |
| PrefixTermTacletAppIndexCacheImpl.java | Class | The abstract superclass of caches for taclet app indexes that are implemented
using a common backend LRUCache (the backend is stored in
TermTacletAppIndexCacheSet). |
| ProblemLoader.java | Class | |
| ProgVarReplacer.java | Class | Replaces program variables. |
| Proof.java | Class | A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals. |
| ProofAggregate.java | Class | |
| ProofEvent.java | Class | |
| ProofSaver.java | Class | Saves a proof and provides useful methods for pretty printing
terms or programs. |
| ProofSaverLatex.java | Class | |
| ProofTreeAdapter.java | Class | An abstract adapter class for receiving proof tree events. |
| ProofTreeEvent.java | Class | Encapsulates information describing changes to a proof tree, and
used to notify proof tree listeners of the change. |
| ProofTreeListener.java | Interface | |
| ProofTreeRemovedNodeEvent.java | Class | Encapsulates information describing changes to a proof tree, and
used to notify proof tree listeners of the change. |
| RuleAppIndex.java | Class | |
| RuleFilter.java | Interface | Interface for objects that represent sets of rules, and which can be used
to distinguish different kinds of rules. |
| RuleSource.java | Class | |
| RuleTreeModel.java | Class | |
| SemisequentTacletAppIndex.java | Class | This class holds TermTacletAppIndexs for all formulas of
a semisequent. |
| SetRuleFilter.java | Class | |
| SimplifyIntegerRuleFilter.java | Class | Filter that selects instances of the SimplifierIntegerRule. |
| SingleProof.java | Class | |
| SortMismatchException.java | Class | |
| SVInstantiationException.java | Class | |
| SVInstantiationExceptionWithPosition.java | Class | Represents an exception with position information. |
| SVInstantiationParserException.java | Class | |
| SVRigidnessException.java | Class | |
| SymbolReplacer.java | Class | |
| TacletAppIndex.java | Class | the class manages the available TacletApps. |
| TacletFilter.java | Class | Interface for filtering a list of TacletApps, for example to
choose only taclets for interactive application or taclets
belonging to some given heuristics. |
| TacletFilterCloseGoal.java | Class | |
| TacletFilterSplitGoal.java | Class | |
| TacletIndex.java | Class | manages all applicable Taclets (more precisely: Taclets with
instantiations but without position information, the ???NoPosTacletApp???s)
at one node. |
| TacletInstantiationsTableModel.java | Class | |
| TermSVReplacer.java | Class | |
| TermTacletAppIndex.java | Class | |
| TermTacletAppIndexCacheSet.java | Class | Cache that is used for accelerating TermTacletAppIndex.
Basically, this is a mapping from terms to objects of
TermTacletAppIndex, following the idea that the same taclets
will be applicable to an occurrence of the same term in different places.
There are different categories of locations/areas in a term that have to be
separated, because different taclets could be applicable. |
| TestGoal.java | Class | class tests the goal, especially the split and set back mechanism. |
| TestProofTree.java | Class | |
| TestTacletIndex.java | Class | |
| TestTermTacletAppIndex.java | Class | |
| UpdateSimplificationRuleFilter.java | Class | Filter that selects instances of UpdateSimplificationRule. |
| UseMethodContractRuleFilter.java | Class | |
| VariableNameProposer.java | Class | Proposes names for variables (except program variables). |