Specifications of programs use auxiliary symbols to encapsulate concepts for a variety of reasons: readability, reusability, structuring and, in particular, for writing recursive definitions. The definition of these symbols often depends implicitly on the value of other locations such as fields that are not stated explicitly as arguments. These hidden dependencies make the verification process substantially more difficult. In this paper we develop a framework that makes dependency on locations explicit. This allows to define general simplification rules that avoid unfolding of predicate definitions in many cases. A number of non-trivial case studies show the usefulness of the concept.
In program logics, especially in logics that target object-oriented languages, state-dependent predicates or functions are a convenient and often necessary concept used in specifications. They allow one to keep specifications concise and easy to read for humans. They are indispensable for the specification of inherently recursive properties such as reachability. Especially in first-order program logics there is no other alternative to specify properties recursively.
Such state-dependent predicate or function symbols, which are sometimes called non-rigid symbols, are not straightforward to use in verification practice, because they require special inference techniques. To unpack and transform their definition after every single state change would be extremely inefficient and must be avoided. As a first example, we consider the frequent specification task that stipulates an object array a to contain only non-null references. It is convenient to define a non-rigid unary predicate symbol on arrays: nonNullArray(a) :⇔ ∀i.a[i] = null A typical desirable property in this context is that a simple assignment to a program variable j does not change the validity of nonNullArray. The formulation in Hoare logic [11] is in the first line below, the second line is the same in Dijkstra's weakest precondition calculus [9], and the third line reformulates it in Dynamic Logic [10]: {nonNullArray(a)} j := j + 1; {nonNullArray(a)} nonNullArray(a) → wp(j := j + 1, nonNullArray(a)) nonNullArray(a) → j := j + 1; nonNullArray(a) .
To prove this claim naïvely entails unpacking the definition of nonNullArray or to define a special-purpose predicate transformer having specific knowledge about the state dependencies in its definition. For example, the definition of nonNullArray contains an implicit dependency on a and on a[i] for all i, but not on any integer program variable j. The contribution of this paper is a technique that makes this kind of implicit dependency information explicit in the symbol's syntax. This leads to significantly higher automation. The presented approach has been evaluated in several small examples, e.g. verification of a selection sort algorithm, but also to verify an implementation of the Schorr-Waite algorithm. It allows to formulate uniform predicate transformers that can exploit generic dependencies and that are applicable in a variety of situations. This paper is partly based on results first published in the first co-author's dissertation [8].
The paper is structured as follows. The program logic used in this paper is introduced in Sect. 2. Syntax and semantics for the explicit dependency notation called location descriptors are presented in Sect. 3. In Sect. 4 we show how to prove that the chosen location descriptor is consistent with the predicate's definition. Predicate transformers in the form of simplification rules that take advantage of explicit dependencies are presented in Sect. 5. Sect. 6 presents applications and case studies that show the usefulness of the concept of location descriptors. Sect. 7 credits related work and outlines future work.
This section sketches the program logic used throughout the paper. We use object-oriented dynamic logic (ODL) [4] which extends standard dynamic logic [10] to cover all essential features of object-orientation, but is small enough for theoretical purposes.
The programming language used in ODL is essentially a stripped down version of JAVA. It supports all concepts except for inner and anonymous classes, floating point arithmetic, threads (and, hence, GUI). Additionally, ODL does not support dynamic method binding or exceptions. Some of these restrictions stem from open scientific problems (floating points, threads), others are a consequence of the goal to define a minimalistic object-oriented language into which all aspects of realistic languages can be compiled without much overhead. We concentrate on the language aspects essential for the paper and leave out, for example, object allocation or exceptions. For a full account see [4]. When convenient we use the style of presentation given in [3] for the logic JAVA CARD DL. Definition 1 (Signature). Let T all := { , boolean, int, ⊥} ∪ T d denote a finite set of types. (T all , ) forms a complete lattice with respect to the partial order (modelling the subtype hierarchy). T d is the set of all reference types (closed by intersection) containing the Null type as least element. Further, T := T all − {⊥} denotes the set of all types except the bottom type. Then the expression f (o 1 , . . . , o n ) := v denotes an elementary update. General updates are defined inductively. Let U , U 1 , U 2 be updates, then all of the following expressions are updates as well:
the conditional \if (φ); U (where φ is a formula), and the quantification \for x; U (binding the first-order variable x in update U ). Definition 4 (Terms and Formulae). The inductive definition of terms and formulae is as usual for typed first-order dynamic logic. We define only the less common cases:
-Let U be an update and ξ a term (formula), then {U } ξ is a term (formula).
-Let φ be a formula and p a program, then [p]φ (partial correctness) and p φ (total correctness) are formulae.
The following definitions formalise the semantics of formulae and updates.
Definition 5 (ODL Kripke Structure). An ODL Kripke structure K := (M, S, ρ) consists of -A partial first-order model M = (D, I 0 ) providing a domain mapping D that assigns to each type its domain (with D(int) = Z) and a partial interpretation I 0 for all rigid and non-rigid predicate symbols:
where q : T 1 × . . . A function β : VSym → T ∈T D(T ) assigning to all logic variables an element of the universe of the appropriate type is a variable assignment.
A semantic location is defined as a tuple f, (e 1 , . . . , e n ) where f : T 1 × . . . × T n → T is a location function symbol as in Def. 2 and e i (for i ∈ {1, . . . , n}) are elements in D(T i ).
Definition 7 ((Consistent) Semantic Update). An elementary semantic update is a pair ( f, (e 1 , . . . , e n ) , d) where f, (e 1 , . . . , e n ) is a semantic location with f : T 1 × . . . × T n → T and d an element of D(T ). A (possible empty) set of elementary semantic updates is called semantic update. A semantic update is called consistent, if it contains for any semantic location at most one elementary semantic update. Definition 8 (Application of a Consistent Semantic Update). The application of a consistent semantic update CU is a mapping between states. Applying CU in a state S maps it to the state S = CU (S) that coincides on the value of all location function with S except for the semantic locations occurring in CU : whenever ( f, (e 1 , . . . , e n ) , d) ∈ CU then S (f )(e 1 , . . . , e n ) evaluates to d.
Updates are an explicit notation to capture symbolic state changes. The definition of a semantics for updates is rather technical due to clashes when an update assigns different values to the same location. Sequential composition describes two successive state changes, while parallel composition updates the locations simultaneously and may cause clashes by updating the same location with differing values, e.g., l := t 1 || l := t 2 . We use a last-one-wins clash resolution, i.e., in the resulting state location l has the value t 2 . Quantified updates allow us to represent state changes of infinitely many locations. Resolution of clashes caused by quantified updates is left out for space reasons (see [3,18]).
Example 1. Some updates and their intended semantics:
-The elementary update x := t assigns to the program variable x the value t.
Applying it to a program variable y in {x := t} y results in t if x and y are the same variable, otherwise, the term evaluates to y. -The parallel update x := y || y := x swaps the content of the program variables x and y. Parallel updates are evaluated simultaneously and, therefore, are independent of each other. More formally, let K := (M, S, ρ) be an ODL Kripke structure, S ∈ S and β a variable assignment. Evaluating the above update under (K, S, β) results in the consistent update CU mapping S to a state CU (S) coinciding with S except for the program variables x and y whose values in (K, S, β) are swapped. -The quantified update \for i; a[i] := 0 assigns 0 to all components of a.
We continue by defining the semantics of terms and formulae: Definition 9 (Semantics of Terms and Formulae). The inductive semantic definitions are as usual. We list only a few non-obvious cases, full definitions are in [3,4].
Let K := (M, S, ρ) denote an ODL Kripke structure, t (K,S,β) the evaluation of term t in state S under a variable assignment β, and |= the validity relation.
-
Later in the paper we need means to relate two arbitrary states on the syntactic level. For this we use a special kind of update called anonymous program update whose purpose is to perform a state transition to an unspecified state. Anonymous programs of this kind are well-known from propositional dynamic logic [10]. They are deterministic and terminating.
The atomic programs st 1 , st 2 . . . are called (elementary) anonymous programs. The set of programs Π is extended accordingly. Further, we extend the inductive definition of updates by including the elementary anonymous program update ω i for each anonymous program st i .
). An anonymous program st i is interpreted in an ODL Kripke Structure K such that for all S ∈ S there exists exactly one state S ∈ S such that ρ(st i )(S, S ) holds. An anonymous program update ω i is then evaluated to a state transformer such that ω (K,S,β) i (S) = S for all variable assignments β.
In this section we introduce a syntactic notation for non-rigid symbols that renders explicit the implicit dependencies on the state in their definition.
We need a notation to describe sets of locations. We use location descriptors introduced in the KeY-system [3] for modifies/assignable clauses. The origin of this notation goes back to quantified updates [18], see also Sect. 2. Location descriptors permit a compact and extensional characterisation of location sets.
A location descriptor has the form \for x 1 , . . . , x n ; \if (Φ) loc where (i) x 1 , . . . , x n are variables bound in Φ and loc, (ii) Φ is an arbitrary formula, and (iii) loc is a term with a location function symbol as top level operator, i.e., a program variable, an attribute function or the array access function. Except for x 1 , . . . , x n no other free variables occur in Φ or loc.
Location descriptors ld 1 , ld 2 can be accumulated to sets of location descriptors by concatenation: ld new := ld 1 ; ld 2 . In case no variables are bound or Φ is identical to true, the corresponding parts in the syntax can be omitted.
Example 2. Here are some typical usages of location descriptors:
-\for List x; x.next capturing all next locations of List-typed elements.
Note that the guard has been omitted here.
Concatenation of location descriptors is evaluated as union of their extensions. 3 The attribute length returns the length for each array and is unspecified otherwise.
Note 2. This definition works for any kind of location descriptor. In particular, the guard formula Φ and possible subterms of the location term can be arbitrary ODL formulae and terms that may contain non-rigid symbols or even programs.
The notation introduced above provides a concise way to characterise sets of locations. Now we extend the names of non-rigid (predicate and function) symbols by qualifications in the form of location descriptors. The idea is that the value of thus qualified symbols depends at most on the values of their arguments plus those locations contained in the extension of their location descriptor.
Definition 14 (Symbols with Explicit Dependencies). Let ld denote a semicolon-separated list of location descriptors and let p :
predicate with explicit dependencies. Analogously for functions. The definitions of terms and formulae remain unchanged. The only difference is that the signature contains the above defined location-dependent symbols.
There are only few restrictions on the interpretation of ordinary non-rigid function and predicate symbols: essentially, their interpretation has to be well-defined and respect their types. The situation is different for symbols with explicit dependencies. The interpretation of a symbol p[ld] with explicit dependencies has to coincide on all states S 1 , S 2 that share the same values for the locations described by ld. This is precisely formulated in the next two definitions.
Definition 15 (ld-Equivalence). For any Kripke structure K we define for any location descriptor ld the equivalence relation ≈ ld on states where S 1 ≈ ld S 2 iff the following two conditions hold:
1. ld (K,S 1 ) = ld (K,S 2 ) (identical location descriptor extension) and 2.
The additional restriction required for Kripke structures to accomodate symbols with explicit dependencies is now covered by the definition:
Definitional extension in first-order logic preserves consistency, i.e., adding a new axiom of the form ∀x(p(x) ↔ φ) for a new predicate symbol p not occurring in φ will not introduce new inconsistencies. For predicates with explicit dependencies an axiom of the form ∀x : T p[ld] ; (p[ld](x) ↔ φ) may already by inconsistent with respect to the dependency semantics of Def. 16: one has to ensure that the implicit state dependencies of φ are reflected in the location descriptor ld. The problem only concerns the implication ∀x : T p[ld] ; (p[ld](x) → φ). We will consider only implicational axioms of this type and, to simplify the presentation, we assume there is only one axiom for each defined predicate. These axioms will be exploited during proof search as rewrite rules p[ld](t 1 , . . . , t n ) φ(t 1 , . . . , t n ) named axiom p[ld]→φ , where the t i 's are terms of the appropriate type. In this setting we allow the defined symbol to occur recursively on the right-hand side.
We intend to define a proof obligation that, when valid, ensures a given implicational axiomatisation of a location-dependent symbol to be consistent with respect to dependency semantics. The problem of termination in the case of recursive rewrite rules is a different matter and has to be dealt with separately.
We need a new concept called anonymising update for location descriptors: this is a quantified update for a given location descriptor that assigns all locations in its extension a fixed, but unknown value: Definition 17 (Anonymising Update for Location Descriptors). Let ld := \for T o; \if (φ) f (t) be a location descriptor. The quantified update
with c being a fresh uninterpreted rigid function symbol of matching type and arity is called an anonymising update for the location descriptor ld. For ld = ld 1 ; . . . ; ld n we define
With the help of anonymising updates it is possible to formulate dependence consistency (Def. 16) directly as the proof obligation
where ω c is a fresh anonymous program update (Def. 10). Theorem 1. If (1) is logically valid, then ∀x : T p[ld] ; (p[ld](x) → φ) is consistent with respect to dependency semantics.
In this section we introduce two update simplification rules that can be applied to arbitrary atomic formulas with explicit dependencies. We make use of the following Lemma [3, Sect. 3.9], [18]:
Crucial for the first simplification rule is the notion of relevant location symbol. Relevant location symbols are a syntactic approximation of the location symbols that a formula φ or a term t may depend on. The notation is Loc(φ) and Loc(t). In the definition below, and later, we use the following notation:
h[ld](s 1 , . . . , s n ) stands for a function or predicate symbol with explicit dependencies, ld = ld 1 ; . . . ; ld q ; ld i := \for T i1 o i1 ; . . . ;
For ease of presentation we assume that f i = f j for i = j. This affects the formula ψ U 1 ,U 2 ,ld in Def. 20. It is not hard to see how to adapt this formula to the unrestricted case. Definition 18 (Relevant Location Symbols). Loc(¬ψ) The coincidence simplification rule is of an approximate nature but is sufficient for many practical purposes. We provide a stronger, semantic simplification rule in the form of the equivalence simplification rule. We require sufficient and necessary conditions for the logical equivalence of the two formulae {U 1 } k[ld](s 1 , . . . , s n ) and {U 2 } k[ld](s 1 , . . . , s n ). First we want the argument terms of k[ld] to evaluate to the same values after the respective updates, i.e., {U 1 }s l . = {U 2 }s l for all 1 ≤ l ≤ n. Next we want to formalise that the locations described by each ld j after update U 1 are the same as those described by ld j after update U 2 and that their values coincide:
Definition 20 (Equivalence Simplification Rule).
Example 6. We modify Ex. 5 by using the more specialised 0-ary predicate nonNullArray a [\for int i; a[i]] restricting the non-null element property to only those arrays referenced by the program variable a. Let
the formula to be proven valid where b is an array of the same type as a. Note that we cannot apply the coincidence simplification rule here: Loc(\for int i; a[i]) yields [•], i.e., the non-rigid array lookup function which is also the leading function symbol of the update {b[0] := null} . Now we apply the equivalence simplification rule which gives for formula ψ 1 1 :
Under the assumption a = b this can be easily proven with a first-order theorem prover after applying the update.
Note 4. The calculus with the equivalence simplification rule added is complete for the logic containing symbols with explicit dependencies relative to the calculus without those symbols.
In this section we show applications of symbols with explicit dependency information modelling specification predicates such as reachability. Using these symbols provides advantages for interactive and automated proving. By being able to delay expanding the definition of a non-recursive predicate, the proof remains readable for a human reader. The automation benefits from the availability of general simplification rules reducing the need to look into the definition of non-rigid symbols. This is briefly illustrated in two case studies.
Reachability. Treatment of linked data structures in specification and verification of object-oriented programs requires routinely to express reachability between two objects via a finite chain of fields. Fig. 1 shows a simple binary, directed tree, where subtrees are accessible via the fields left and right. Specifying properties such as an element occurring in a given list requires to introduce and formalise the concept of reachability for these data structures. In the following we concentrate on the definition of a predicate formalising reachability for the directed, binary tree structure in Fig. 1. We aim to define a Fig. 1. A binary tree datastructure with its associated reachable predicate symbol.
predicate that takes three arguments x, y (both of type Tree) and n (of type int) and holds if the subtree y can be reached from tree x in exactly n steps using only the fields left and right. The recursive definition for reachability predicate is rather straightforward:
A calculus rule can be easily derived from the definition. The predicate is clearly non-rigid as it depends not only on the value of its arguments but also on the left and right fields of the subtrees below and including x. Therefore, we easily identify a location descriptor capturing all location dependencies, namely \for Tree t; t.left; \for Tree t; t.right describing the set of all left, right locations of all trees. Hence, the location-dependent predicate symbol for capturing reachability in our notation is: reach[\for Tree t; t.left; \for Tree t; t.right](Tree, Tree, int) .
Verification of a sorting algorithm consists of showing that the result is indeed sorted and that the result contains exactly the elements of the original collection, in other words, that the result is a permutation of the input. For the verification of a standard selection sort implementation in JAVA a specification predicate with explicit dependencies has been used to formalise permutation of two arrays. 4The permutation predicate perm
is defined with the help of a recursive count of the occurrences of all elements in both arrays. The predicate occurs once in the post condition stating that the resulting array is indeed a permutation of the original, and the second time in the loop invariant of the sorting algorithm.
The selection sort algorithm starts at the first array element and swaps it with the first minimal element encountered in the subsequent array continuing until the last element is reached. Therefore, it utilises two nested loops. To prove that both loops preserve the permutation property without predicates having explicit location dependencies requires several inductive subproofs. To substantiate this claim we look at the following formula5 that occurs subgoal during the proof and has to be proven valid: The update of the formula in the implication's premise states a transition to a state where array aCopy is a shallow copy of the old content of array a0.
Simultaneously new values are assigned to the components of array a0. The complete formula in the premise states then that in this state aCopy and a0 are permutations.
The update of the formula in the conclusion starts with a number of updates stemming from branch predicates irrelevant for the permutation property. The quantified updates assign the components of the arrays aCopy and a0 the exact same values as it is the case for the premise formula. But the following two updates lead to a slightly different state with a0[idx1] and a0[idx2] swapped.
Obviously, the implication is valid, because a standard transposition lemma can be used to show preservation of the permutation property. The technical difficulty is that a straightforward application of this transposition lemma is not possible. One has to prove that all updates preceding the array locations including the twelve updates abbreviated by ". . . " have no effect on the permutation property. This is done inductively using a strengthening of the claim where for any possible value of b10, b4, b5, . . . the permutation property remains unchanged.
In contrast, the approach presented in this paper exploiting dependency information allows to prove the formula valid without induction. Application of the Coincidence Simplification Rule (Def. 19) simplifies the state representation in the conclusion so far that the application of the transposition lemma is directly possible. We were able to prove the permutation property for an executable JAVA implementation of selection sort with only one user interaction exploiting the fact that swapping exactly two elements in an array preserves the permutation property.
The most complex case study so far where predicates with explicit dependencies were used is the verification of a fully functional JAVA implementation of the Schorr-Waite graph marking algorithm [20] for arbitrary finite graph structures. The abstract algorithm has been verified in several case studies [7,6,21,16,1,5,12], mostly for the case of binary graphs. Our case study, first reported in [8], is to knowledge the first time that an executable JAVA implementation for the general case was verified.
The Schorr-Waite graph marking algorithm saves memory by avoiding to encode the taken path in the method call stack. Instead a small number of auxiliary variables and subtle pointer rotations are used to encode the backtracking path. Besides showing that all reachable nodes are visited, the challenge is to show that afterwards the graph structure is restored, because the traversal uses destructive pointer manipulations.
Specification predicates with explicit dependencies were employed to express reachability of two nodes in the graph structure and for a specification predicate that characterises the backtracking path. The reachability predicate has been specified similar to the one in Sect. 6.1. The predicate characterising the backtracking path is specified in such a way that it evaluates to true if a given node is an element of the currently taken path. This is clearly state-dependent as the backtracking path changes during execution.
The Java Modelling Language (JML) [14] supports a depends clause used to express on which other fields a model field depends. The depends clause is then used to extend assignable clauses appropriately in case they contain model fields. These depends clauses have been introduced by Leino [15], the main idea being to replace the occurrence of an abstract/model field a with a function symbol a (f 1 , . . . , f n ) that explicitly enumerates the fields it depends on.
Separation logic [17] requires to specify exactly those locations of the heap (alternatively, to separate a heap into two orthogonal heaps) that are necessary to prove a property. The local judgements are then generalised by application of a frame rule. This approach is in the following sense complementary to ours: in separation logic, the shape of the heap is made explicit and dependencies are lifted with the help of a frame axiom. We make location dependencies explicit and can, therefore, abstract away from the concrete layout of the heap. This seems more appropriate for target languages such as JAVA. Another advantage of our approach is that only standard typed first-order logic is used.
Dynamic frames as introduced in [13] provide a uniform treatment of modified locations and dependencies, which are separate concerns in the presented work allowing for more precision. Of particular interest is the preservance operator Ξf for a dynamic frame (set of locations) f expressing that a computation does depend on or modify it. This property can be translated to our framework and logic. The other operators for dynamic frames deal with variants of modifies clauses in presence of object creation.
In [2] read effects are used for treating invocations of pure methods. Our approach is directly targeted at the level of specification predicates without the need to them as pure boolean methods, it provides a compact and precise notion for the dependencies and works without an explicit heap presentation. Another concern of [2] is well-definedness of specifications containing pure methods. For our approach well-definedness is desirable, but will not cause unsoundness of the verification system.
Further related work focusses on data groups or similar concepts to support information hiding and encapsulation. This is ongoing work in the context of the KeY project.
Future work includes to exploit further application scenarios for predicates with explicit dependencies. Rümmer suggested to use them to achieve secondorder like specification capabilities in a first-order dynamic logic through parameterisation with functions. This allows, for example, to use the same specification for the sum over all elements of an array i f (a[i]) for any function f . Further, we will investigate how to improve automation of the equivalence update simplification rule, i.e., in finding a suitable equivalent update U 2 .
We introduced non-rigid specification predicate (and function) symbols that explicitly list the set of locations their value may depend on. Then we presented a verification framework for such symbols with explicit dependencies. This framework consists of two parts: on the one hand a uniformly generated proof obligation that ensures correctness of a predicate with explicit dependencies with respect to its axiomatisation; on the other hand a number of general simplification rules that allow one to exploit explicit dependencies within the context of a proof. Several application scenarios common in program verification as well as two case studies support the usefulness of our approach. The implementation and case studies were done within the KeY-system [3], however, as pointed out in the introduction the problem of location-dependent predicates as well as the solution presented here can be transferred to other program logics based on weakest precondition reasoning.
We thank Philipp Rümmer and Wolfgang Ahrendt for valuable comments. Special thanks go also to Benjamin Weiß for valuable comments and in particular for pointing out a problem in the original version of Def. 8. We thank the anonymous referees for their valuable comments.