KeY-TechTips No.3 (21.01.2002) ------------------------------ 0. General ---------- The topic of this KeY-TechTip are the datastructures used to represent a formula or a term, especially focusing on their creation. Also all KeY-TechTips are now available at http://i12www.iti.kit.edu/~bubel/private/keytechtips/tips.html 1. Building terms and formulae ------------------------------ (The use of the word 'singleton' is slightly stretched in the next paragraphs. The intention of the singleton pattern will be covered, but often not in the strict meaning that there is only one instance of the class, but only one object for the corresponding logic element, will be clarified when the word is used.) As the syntactical construction principle of both, terms and formulae, are quite similar, we use the same classes to represent these logic elements. This affects only the implementational view not the theoretical one. As the used dynamic logic is sorted, a special sort is used to distinguish terms and formulae, the last one must have the sort FORMULA, while the target sort of terms never have this sort. In the following article most of the used classes can be found in the package de.uka.ilkd.key.logicdata . 1.1. Building terms ------------------- As a first example we will build some terms of sort int. First the needed sorts have to be created. This is important as sorts are singletons, so that memory is saved and testing sorts of equality will be faster, as we have just to look for object identity ('=='). This implies that if you create two objects of type Sort they will represent different sorts, even if the name of them is equal. For this example only one sort - the sort "int" - is needed: Sort int_sort = new Sort(new Name("int")); To create the constant 'zero', we need a function symbol Function zero = new Function(new Name("zero"), int_sort, new Sort[0]); The first argument of the constructor is just the name of the function symbol, the second one is the (target) sort of the function, last but not least the constructor needs the sorts of the arguments in this case we have a constant so the arity of the function is zero. Please take care that the object created above is not a term it is more the signature/declaration of the function "zero", this means something like: zero: -> int Now we can build our first term: Term term_zero = new OpTerm(zero, new Term[0]); The class Term used in the declaration part of the assignment is the abstract superclass of all terms (and formulae), it is also the only one that can be seen outside, this means all other parts of the KeY-system (the prover, the ocl-dl translator etc.) know only the class Term and its operations, the visibility of subclasses should be restricted to the package 'logicdata'. All information about them should be derived using the operations of class Term. In this case we use the subclass OpTerm, that is always used if a term can be described just with its operator and subterms. What is an operator? The operator of a term is the top symbol in our case the function symbol 'zero'. Later we will see other examples of operators such as the logical operator 'AND', 'OR' etc. Each type that may stand as an operator has to implement the interface "Operator" and so does the class Function (more precise the class function extends the class TermSymbol which implements the interface). The top operator of the term is addressed by calling the method 'op()' and in our case it will deliver the function symbol zero: if (term_zero.op() == zero) { System.out.println("Zero function."); } else { System.out.println("Ooops."); } >> output: Zero function. The term stands for a constant and has therefore no subterms, that is why we have to hand over an empty array with element type Term. As next task we may want to build a more complex term, such as: add(x,add(y, zero)); This means we need a function symbol 'add' of arity '2' with target and argument sort 'int_sort'. Function add = new Function(new Name("add"), int_sort, new Sort[]{int_sort, int_sort}); Important: Function symbols are singletons, the implications are the same as described for sorts above. The function symbol is named "add" has as target sort 'int_sort' and two arguments both of sort 'int_sort'. Now we need two variables 'x' and 'y', therefore we use the class LogicVariable. KeY knows more kinds of variable, such as ProgramVariable (used to represent variables of a java program and cannot be quantified), SchemaVariable and so on but more on them later or in one of the next TechTips. LogicVariable var_x = new LogicVariable(new Name("x"), int_sort); LogicVariable var_y = new LogicVariable(new Name("y"), int_sort); As a term may consist of a single variable, the class LogicVariable implements the interface 'Operator'. The term can now be constructed as follows: Term term_x = new OpTerm(var_x, new Term[0]); Term term_y = new OpTerm(var_y, new Term[0]); Term add_y_zero = new OpTerm(add, new Term[] {term_y, term_zero}); Term add_x_add_y_zero = new OpTerm(add, new Term[]{term_x, add_y_zero}); Summary: a) Terms have an object of type Operator as top symbol. The abstract class Term is the only one seen outside the package 'logicdata' and therefore all necessary information about the term has to be communicated through the operations declared in the class Term. b) Function symbols as well as sorts are unique elements, having two different objects will describe different sorts (or functions) even if they have the same name. 1.2. Building a formula ------------------------ After building terms we now want to build a formula. Starting with a simple one that is just a predicate. Even(x) This predicate is named "Even" and has a variable of 'int_sort' as argument. The term 'term_x' with variable 'var_x' as top operator has already been built, the only missing symbol in order to create the formula is the predicate symbol 'Even' Function even = new Function(new Name("Even"), Sort.FORMULA, new Sort[]{int_sort}); Term even_x = new Term(even, new Term[]{term_x}); The predicate 'even' is of type function, but it has as target sort the sort 'FORMULA' that can be accessed by the static field 'FORMULA' of the class Sort. Each term with an operator of this sort is a formula, as 'even_x' is. After the role of the Sort FORMULA should now be clear, the next formula to be built is a bit more complex. all x:int.(even(x) -> even(add(x,2))) First we need the constant '2': Function two = new Function(new Name("2"), int_sort); and the corresponding Terms Term term_two = new OpTerm(two, new Term[0]); Term add_x_2 = new OpTerm(add, new Term[]{term_x, term_two}); Term even_add_x_2 = new OpTerm(even, new Term[]{add_x_2}); now the implication is built up Term even_x_impl_even_add_x_2 = new OpTerm(Op.IMP, new Term[]{ even_x, even_add_x_2 }); Stop here. What is this Op.IMP? OK, the former operators were all function- or predicate symbols, these may differ from application to application so we had to create our own ones. But there exists some default operations of the logic such like the different connectors and quantifiers or on the term side the epsilon operator for the epsilon terms. These default operators are also unique (singletons) and can be accessed by static fields in class Op. This class contains most of the logic operators and is extended by * the class Junctor that implements the junctors like 'and', 'or', 'not', 'imp' and so on * the class Quantifier to have the quantifiers 'all' and 'exist' * the class SubstOp for the substitution operator * the class Epsilon for the operator of the epsilon terms We will now use the quantifier "Op.ALL" to complete our formula. Term all_x_even_x_impl_even_add_x_2 = new QuantifierTerm(Op.ALL, new QuantifiableVariable[]{var_x}, even_x_impl_even_add_x_2); This time we need another subclass of term the class QuantifierTerm because additional information needs to be given. As the all-quantifier should be a singleton it cannot contain the variable it binds. This information is stored in the class QuantifierTerm and may be accessed using the method varsBoundHere(int n) declared in class Term overwritten by class QuantifierTerm. This method returns an ArrayOfQuantifiableVariable containing the variables that are bound in the n-th subterm by the quantifier of the current term. An OpTerm would always return an empty array. Summary: -------- a) the sort stored in Sort.FORMULA is used to describe a formula b) the class Op contains all the standard operators that are used as singletons, they can be accessed by static fields. 1.3. Some general words about the class Term -------------------------------------------- 1.3.1 Equality on terms - term sharing -------------------------------------- It was often mentioned that function/predicate symbols are unique (singletons) and equality is determined by object identity. This is not so for terms. The equals(Object o)-method on terms walks through the term tree and compares the operators of the terms, if they are equal (attention: for most operator (all, but UpdateOp) this means if they are same). To save memory, terms are immutable, so that they cannot be changed after their creation. There are situations where this may be uncomfortable, but it is necessary to have the possibility of sharing terms as shown below: In this example we want to create a similar term as the previous one but using the exist-operator: ex x:int.(even(x) -> even(add(x,2))) we could now create each subterm again, or use the benefits of term sharing. I prefer the last possibility because then Term ex_x_even_x_impl_even_add_x_2 = new QuantifierTerm(Op.EX, new QuantifiableVariable[]{var_x}, even_x_impl_even_add_x_2); is all that has to be done. If you look at the class Term you will find a method called equalsModRenaming(Object o) this methods returns true if two terms only differ in the names of their bound variables. Example: -------- Term ex_y_even_y_impl_even_add_y_2 = new QuantifierTerm(Op.EX, new QuantifiableVariable[]{var_y}, even_y_impl_even_add_y_2); is created similar to the term 'ex_x_even_x_impl_even_add_x_2'. Executing System.out.println("Equals: "+ ex_x_even_x_impl_even_add_x_2.equals(ex_y_even_y_impl_even_add_y_2)); System.out.println("EqualsModRenaming: "+ex_x_even_x_impl_even_add_x_2. equalsModRenaming(ex_y_even_y_impl_even_add_y_2)); delivers Equals: false EqualsModRenaming: true The equalsModRenaming(..) method is e.g. useful for matching terms in sequents. 1.3.2 Some other methods ------------------------ If you want to access the subterms of a term, you first have to get its arity using method arity() and then access the subterms with sub(int nr) Term term = even_x_impl_even_add_x_2; System.out.println("Top: +"term.op()); for (int i = 0; i Q(x1:int, x2:int)' ) returns 'A -> Q(x1:int, x2:int)' 1.5. Overview of term-classes ---------------------------- There are different subclasses of class Term. OpTerm: used for terms like f(x1,...,xn), atomar formulae and all formulae that are not covered by one of the following classes. QuantifierTerm: used for quantified formulae, e.g. all x:int.Even(x) ProgramTerm: used for diamond or box formulae. Only this class returns a program if method javaBlock is called, all other will return 'null' SubstitutionTerm: used to represent a term or a formula similar to {x zero} Even(x) meaning that x is replaced by zero in Even(x), but the substitution is not executed (e.g. performance reasons, description of the behaviour of some STSR). UpdateTerm: a formula describing an assignment of a variable. {i zero} <{ if (i == 0) ... }> i