| de.uka.ilkd.key.counterexample |
|
| Java Source File Name | Type | Comment |
| AxiomCalculus.java | Class | This class generates the clauses for the axioms. |
| Calculus.java | Class | The root of the Calculus Hierarchy, this class only produces the static
clauses which are the same for all problems. |
| CExTerm.java | Class | Diese Klasse soll als Wrapper dienen fuer ibijas Termklassen. |
| Clause.java | Class | |
| Clauses.java | Class | |
| Configuration.java | Class | This class is the storage for global configuration data
of the counterexample subpackage. |
| ConjCalculus.java | Class | An instance of this class contains the fully generated calculus including all components generated througout the inherited classes: static clauses, sort dependent clauses, clauses generated from axioms and the clause representing the conjecture. |
| CounterExample.java | Class | You can use this class to prove that a certain conjecture is wrong for an
abstract data type. |
| MgtpWrapper.java | Class | This class calls the parser of Mgtp with the generated Calculus.
After the parser has processed the calculus, the theorem prover
is called and the returned model is then further processed
and written to the 'result' attribute. |
| ModelRepresentation.java | Class | This class is a representation of the Model generated by mgtp
displaying the values that the variables are assigned, the
interpretation of subterms, the statistics of the latest mgtp
run etc. |
| SortCalculus.java | Class | This class generates the clauses which depend on the generated sorts,
it includes the static clauses generated by Calculus
which this class extends.
These clauses are different for each adt, depending on the generated
sorts that are used. |
| TestProgramm.java | Class | TestProgramm zum Testen des CounterExample Packages
Achtung: sehr sehr gehackt, z.B. |