|
| |
|
| java.lang.Object
 de.uka.ilkd.key.counterexample.Calculus
de.uka.ilkd.key.counterexample.SortCalculus
de.uka.ilkd.key.counterexample.AxiomCalculus
All known Subclasses: de.uka.ilkd.key.counterexample.ConjCalculus,
| AxiomCalculus | | public class AxiomCalculus extends SortCalculus (Code) | | This class generates the clauses for the axioms. It contains
the complete Axiom Transformation algorithm as described in
Wolfgang Ahrendt's PHD-Thesis
author:
Sonja Pieper
version:
0.1 |
| AxiomCalculus | | public AxiomCalculus(ADT a)(Code) | | |
| TransTerm | | public String TransTerm(CExTerm term)(Code) | | Eigentliche Rekursion;
nachbedingung: nach ausfuehrung fuer Transterm muss bekannt
sein ob ein ffterm nun fft ist oder nicht!!!!
|
| TransTermListe | | public String TransTermListe(CExTerm[] termliste)(Code) | | ruft auf jedem CExTerm des Arrays CExTerm auf und baut eine Konjunktion zusammen
"," wird in der CExTerm eingefuegt!
|
| axiomClauses | | public Clauses axiomClauses()(Code) | | This method runs the loop so every axiom can be transformed with
transAxiom(...) and then added to the list of axiomclauses
the list of clauses with the transformed axioms |
| transAxiom | | public Clause transAxiom(Axiom axiom)(Code) | | This is the start of the actual Transformation of the axioms.
The completely transformed axiom in the calculus clause format |
| transDisj | | public String transDisj(Term term)(Code) | | Since an Axiom is a disjunktion of equalities or unequalities
one calls this funktion before being able to transform the equalities
which is done in the transLit function. A literal in this case
means an equality.
Parameters:
term - the first call gets the full axiom then it works downthe disjunctions recursively. |
| transLit | | public String transLit(Term lit)(Code) | | This method works with equalities mainly and calls on the
transformation methods for the two sides of the equality.
Parameters:
lit - A literal meaning either an equality or inequality An mgtp formatted string which contains the transformed literal |
|
|
|