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.
{nonNullArray(a)} j := j + 1; {nonNullArray(a)}
nonNullArray(a) → wp(j := j + 1, nonNullArray(a))
nonNullArray(a) → hj := j + 1;inonNullArray(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 [
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. 2
This section sketches the program logic used throughout the paper. We use
object-oriented dynamic logic (ODL) [
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 [
As mentioned in Sect. 1 we distinguish between rigid and state-dependent (non-rigid) function and predicate symbols with the following notation: PSym = PSymr ∪ PSymnr and FSym = FSymr ∪ FSymnr. It is useful to single out from the non-rigid function symbols FSymnr the subset of location function symbols, i.e., functions used to represent local program variables, fields and arrays that can be changed by a program or update: Definition 2 (Location Function Symbols). The set of location function symbols FSymloc ⊆ FSymnr contains for each arity an infinite number of symbols including – for each program variable pv used in an ODL program a constant symbol with the same name and type; – for each attribute a of type T declared in a class C of the ODL program, a unary location function symbol a@(C) : C → T ; – the array access operator [] : > × int → >.
Note 1. ODL features separate syntactic categories for program and logic (firstorder) variables. Program variables are modelled as non-rigid constants and cannot be quantified. Logic variables are rigid, quantifiable, and must not occur inside programs. We omit the @(C) suffix from attribute names if no ambiguity arises and write o.a instead of a(o) for attribute lookup expressions. Definition 3 (Updates). Given a location function f and terms oi and v. Then the expression f (o1, . . . , on) := v denotes an elementary update. General updates are defined inductively. Let U , U1, U2 be updates, then all of the following expressions are updates as well: – the sequential composition U1 ; U2, – the parallel composition U1 || U2, – 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 hpiφ (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, I0) providing a domain mapping D that assigns to each type its domain (with D(int) = Z) and a partial interpretation I0 for all rigid and non-rigid predicate symbols:
I0(q) := ↑ , if q ∈ PSymnr
G , if q ∈ PSymr, for some G ⊆ D(T1) × . . . × D(Tn) where q : T1 × . . . × Tn is a predicate symbol (analogous for function symbols) – A set of states S where each S ∈ S contains an interpretation Inr completing the partial interpretation I0 to a total interpretation I := I0 ∪˙ Inr by assigning a meaning to all non-rigid symbols. – The state transition relation ρ defining the programs’ semantics, where for a program p and two states S1, S2 ∈ S the relation ρ(p)(S1, S2) holds if and only if executing p in state S1 terminates in the final state S2. As ODL programs are deterministic the final state is unique whenever it exists.
A function β : VSym → ST ∈T D(T ) assigning to all logic variables an element of the universe of the appropriate type is a variable assignment.
hf, (e1, . . . , en)i where f : T1 × . . . × Tn → T is a location function symbol as in Def. 2 and ei (for i ∈ {1, . . . , n}) are elements in D(Ti).
update is a pair (hf, (e1, . . . , en)i, d) where hf, (e1, . . . , en)i is a semantic location with f : T1 × . . . × Tn → 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.
cation of a consistent semantic update CU is a mapping between states. Applying CU in a state S maps it to the state S0 = CU (S) that coincides on the value of all location function with S except for the semantic locations occurring in CU : whenever (hf, (e1, . . . , en)i, d) ∈ CU then S0(f )(e1, . . . , en) 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 := t1 || l := t2. We use a last-one-wins clash
resolution, i.e., in the resulting state location l has the value t2. 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 [
– 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.
definitions are as usual. We list only a few non-obvious cases, full definitions
are in [
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. – ({U } t)(K,S,β) := t(K,S0,β) where S0 = U (K,S,β)(S) – S, β |= h i
p φ (p ∈ Π) iff a state S0 exists with S0, β |= φ and ρ(p)(S, S0)
– S, β |= [p]φ (p ∈ Π) iff S0, β |= φ holds for any state S0 with ρ(p)(S, S0)
– S, β |= {U } φ iff S0, β |= φ, where S0 = U (K,S,β)(S)
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 [
The atomic programs st1, st2 . . . 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 sti.
mous program sti is interpreted in an ODL Kripke Structure K such that for all S ∈ S there exists exactly one state S0 ∈ S such that ρ(sti)(S, S0) holds. An anonymous program update ωi is then evaluated to a state transformer such that ωi(K,S,β)(S) = S0 for all variable assignments β. 3
In this section we introduce a syntactic notation for non-rigid symbols that renders explicit the implicit dependencies on the state in their definition. 3.1
We need a notation to describe sets of locations. We use location descriptors
introduced in the KeY-system [
\for x1, . . . , xn; \if (Φ) loc where (i) x1, . . . , xn 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 x1, . . . , xn no other free variables occur in Φ or loc.
Location descriptors ld1, ld2 can be accumulated to sets of location descriptors by concatenation: ldnew := ld1 ; ld2. 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. – \for T [] a, int i; \if (i >= 0 ∧ i < a.length) a[i] meaning all T -typed array component locations with indexes between 0 and the array length.3 – \for Tree t; t.left ; \for Tree t; t.right capturing all left and right locations of Tree-typed elements.
Definition 13 (Location Descriptor Extension). Let K := (M, S, ρ) be an ODL Kripke structure with universe D = ST ∈T D(T ). The extension of a location descriptor ld = \for x1, . . . , xn; \if (Φ) l(t1, . . . , tn) in a given state S ∈ S is defined as the set of semantic locations:
ld(K,S) := {h l, (t1, . . . , tn)(K,S,β)i | (K, S, β) |= Φ, β : VSym → D} 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. 3.2
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.
semicolon-separated list of location descriptors and let p : T1 × · · · × Tn be a non-rigid predicate. The non-rigid predicate symbol p[ld] : T1 × · · · × Tn is called 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 S1, S2 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 S1 ≈ld S2 iff the following two conditions hold: 1. ld(K,S1) = ld(K,S2) (identical location descriptor extension) and 2. f (K,S1)(d1, . . . , dn) = f (K,S2)(d1, . . . , dn) for any hf, (d1, . . . , dn)i ∈ ld(K,S1). The additional restriction required for Kripke structures to accomodate symbols with explicit dependencies is now covered by the definition:
ODL Kripke structure K := (M, S, ρ) dependency-consistent if for any predicate k[ld] (function f [ld]) depending on ld and any two states S1, S2 with S1 ≈ld S2 the evaluation of predicate k[ld] (function f [ld]) in S1 and S2 coincides. Lemma 1. Let K be a dependency-consistent Kripke structure. Then in any two states S1, S2 ∈ S with ti(K,S1) = t(K,S2) (i ∈ {1 . . . n}) the atomic formula i p[ld](t1, . . . , tn) evaluates to the same truth value whenever S1 ≈ld S2 holds. Analogously for location dependent function symbols. Note 3. The notions of satisfiability, validity and model carry over to dependency-consistent Kripke structures in a straightforward manner. From now on we deal only with dependency-consistent Kripke structures and the corresponding notions of model, validity, etc., if not stated otherwise.
Example 3. Instead of modelling nonNullArray as a non-rigid predicate as done on p. 28, it can now be modelled as a predicate symbol with explicit dependencies: nonNullArray[\for T [] a, int i; a[i]] : T []. This expresses explicitly that its value depends only on the value of the components of T []-typed arrays and, of course, on its argument. 4
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 : Tp[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 : Tp[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](t1, . . . , tn) φ(t1, . . . , tn) named axiomp[ld]→φ, where the ti’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:
ld := \for T o; \if (φ) f (t) be a location descriptor. The quantified update
Vld := \for T o; \if (φ); f (t) := c(t) 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 = ld1; . . . ; ldn we define Vld = Vld1 || . . . || Vldn.
With the help of anonymising updates it is possible to formulate dependence consistency (Def. 16) directly as the proof obligation pop[ld]→φ := ∀x : Tp[ld]; (({ωc} {Vld} φ(x)) ↔ {Vld} φ(x))) (1) where ωc is a fresh anonymous program update (Def. 10).
Theorem 1. If (1) is logically valid, then ∀x : Tp[ld]; (p[ld](x) → φ) is consistent with respect to dependency semantics. 5
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], [
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](s1, . . . , sn) stands for a function or predicate symbol with explicit dependencies, ld = ld1; . . . ; ldq; – ldi := \for Ti1 oi1; . . . ; Tiri oiri; \if (φi) fi(ti1, . . . , tiαi) For ease of presentation we assume that fi 6= fj for i 6= j. This affects the formula ψU1,U2,ld in Def. 20. It is not hard to see how to adapt this formula to the unrestricted case.
Loc(¬ψ) := Loc(ψ) Loc(Q T x; ψ) := Loc(ψ) Loc(ψ ◦ φ) := Loc(ψ) ∪ Loc(φ), Loc(h(s1, . . . , sn)) := Sin=1 Loc(si), Loc(hprgiψ) := FSymloc Loc([prg]ψ) Loc(g(s1, . . . , sn)) Loc(ld) Q ∈ {∀, ∃} ◦ ∈ {∧, ∨, →, . . .} h is a rigid symbol see Def. 2 :::=== {FSgSq}ym∪lSocin=1 Loc(si) g is a location fct. symbol
see Def. 2 i=1 Loc(fi(ti1, . . . , tiαi)) ld as stipulated above
∪ Loc(φi) Loc(h[ld](s1, . . . , sn)) := Loc(ld) ∪ Sin=1 Loc(si) Loc(h(s1, . . . , sn)) := FSymloc Loc(U ) Lemma 3. Let φ be an arbitrary formula, K a Kripke structure, S a state in K, U as in Lemma 2 with gi 6∈ Loc(φ) for all i then
(K, S) |= φ iff (K, S) |= {U }φ
{U } k[ld](s1, . . . , sn) {U 0} k[ld](s1, . . . , sn) where U 0 := U − {upP arti | gi 6∈ Loc(k[ld](s1, . . . , sn))} and U as in Lemma 2. Example 4. Here is an instance of the coincidence simplification rule, where s is a term with j 6∈ Loc(s): ({i := iV al || j := jV al} p[i](s)) ({i := iV al} p[i](s)) Example 5. The coincidence simplification rule allows to prove the motivating example on p. 28 easily: in nonNullArray(a) → {j := j + 1} nonNullArray(a) we use nonNullArray[\for T [] a, int i; a[i]] as introduced in Example 3. For j 6∈ Loc(a) an instance of this rule simplifies {j := j + 1} nonNullArray[. . .](a) nonNullArray[. . .](a) rendering the implication trivially valid.
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 {U1} k[ld](s1, . . . , sn) and {U2} k[ld](s1, . . . , sn). First we want the argument terms of k[ld] to evaluate to the same values after the respective updates, i.e., . {U1}sl = {U2}sl for all 1 ≤ l ≤ n. Next we want to formalise that the locations described by each ldj after update U1 are the same as those described by ldj after update U2 and that their values coincide: ψj1 = ∀d; ∀cj; ∀oj; . . . .
({U1} (φj ∧ cj = tj ∧ d = fj(tj))) → ∃oj({U2} (φj ∧ cj = tj ∧ d = fj(tj))) ψj2 = ∀d; ∀cj; ∀oj; . . . .
({U2} (φj ∧ cj = tj ∧ d = fj(tj))) → ∃oj({U1} (φj ∧ cj = tj ∧ d = fj(tj))) It is now not hard to see that ψU1,U2,ld = Vjq=1(ψj1 ∧ ψj2) ∧ Vln=1{U1}sl =. {U2}sl is valid if and only if {U1} k[ld](s1, . . . , sn) ↔ {U2} k[ld](s1, . . . , sn) is valid. This justifies the following rule:
{U1} k[ld](s1, . . . , sn)
{U2} k[ld](s1, . . . , sn) provided formula ψU1,U2,ld holds. Example 6. We modify Ex. 5 by using the more specialised 0-ary predicate nonNullArraya[\for int i; a[i]] restricting the non-null element property to only those arrays referenced by the program variable a. Let
a 6= b → (nonNullArraya[. . .] → {b[0] := null} nonNullArraya[. . .]) 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 ψ11: ∀d : T ; c1 : T []; c2 : int; i : int;
. . . (({b[0] := null} (true ∧ c1 .= a ∧ c2 .= i ∧ d.= a[i])) →
∃i : int; (true ∧ c1 = a ∧ c2 = i ∧ d = a[i])) Under the assumption a 6= 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. 6
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. 6.1
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 left n2 n1 right
n3 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 the reachability predicate is rather straightforward: reach(x, y, n) :⇔ false , if n < 0 x =. y , if n =. 0
. (x.left 6=.null ∧reach(x.left, y, n − 1))∨ , if n > 0 (x.right 6= null ∧reach(x.right, y, n − 1))
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) . 6.2
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.4
The permutation predicate perm[\for int[] o; int i; o[i]](int[], int[]) 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
4 This case study has been joint work and is also reported in [
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. 6.3
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
5 Slightly simplified and beautified.
Schorr-Waite graph marking algorithm [
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. 7
The Java Modelling Language (JML) [
Separation logic [
Dynamic frames as introduced in [
In [
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. Ru¨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 Pi 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 U2. 8
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 [
We thank Philipp Ru¨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.