Clément Hurlin
email: clement.hurlin@inria.fr

François Bobot
email: bobot@lri.fr

Alexander J Summers
email: alexander.j.summers@imperial.ac.uk

Size Does Matter: Two Certified Abstractions to Disprove Entailment in Intuitionistic and Classical Separation Logic

We describe an algorithm to disprove entailment between separation logic formulas. We abstract models of formulas by their size and check whether two formulas have models whose sizes are compatible. Given two formulas A and B that do not have compatible models, we can conclude that A B. We provide two different abstractions (of different precision) of models. Our algorithm is of interest wherever entailment checking is performed (such as in program verifiers).

INTRODUCTION

Separation logic [START_REF] Reynolds | Separation logic: A logic for shared mutable data structures[END_REF] has recently made a dent in the verification of pointer manipulating programs. Its successes include simple pointer programs with parallelism [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF], C programs [START_REF] Jacobs | The verifast program verifier[END_REF], and object-oriented programs [START_REF] Chin | Enhancing modular OO verification with separation logic[END_REF][START_REF] Distefano | jStar: Towards practical verification for Java[END_REF]. Formulas in separation logic typically describe parts of the heap: in the context of program verifiers, method preconditions describe the heap space required by methods to execute correctly, and method postconditions describe the heap space passed back to the caller when the method returns. Separation logic comes in two flavours: intuitionistic separation logic is used to verify garbage-collected programs [START_REF] Parkinson | Local reasoning for Java[END_REF][START_REF] Distefano | jStar: Towards practical verification for Java[END_REF] while classical separation logic is used to verify programs in which memory deallocation is performed manually [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF][START_REF] Jacobs | The verifast program verifier[END_REF]. Contrary to intuitionistic separation logic, classical separation logic does not admit weakening, allowing one to reason about memory leaks.

We propose a novel algorithm to disprove entailment between formulas. We abstract formulas by the sizes of their possible models and use comparisons of these sizes to disprove entailment between formulas. Intuitively, to disprove an entailment A ⊢ B, it suffices to show that there exists a model (i.e., a heap) of A whose size is smaller than the size of all models of B. We give two different ways of calculating sizes of models, which have differing complexities and precisions.

Our algorithm is of interest whenever entailment checking is performed, for example in program verifiers. In this particular context, since our algorithm's complexity is low, it can be used to quickly show that a method is not provable, perhaps because programmersupplied specifications are incorrect.

1. A commutative semigroup with total binary operator + M .

2. A minimal permission, m 0 , that satisfies the following property: (∀m)(m 0 + M m = m).

3. A maximal permission, m W .

4. A total order on permissions, ≤ M .

5. A subset of permissions which are defined to be splittable.

6.

A pair of functions on permissions, split1 and split2, which define the two parts into which a splittable permission may be split. These functions must satisfy the following property:

(∀m)(split1(m) + M split2(m) = m).
The maximal permission m W represents full (and exclusive) access to a location, whereas the minimal permission represents no access. Permissions in between these two extremes will allow read access but not write access to a location. Some (in some models, all) permissions are splittable: they can be divided into two smaller (in the sense of permission ordering) permissions. In particular, the maximal permission (which denotes exclusive access) may be split into smaller permissions, none of which allow full access to the location. However, permissions may also be combined (by addition): in this way it is possible for a full permission to be regained, if all partial permissions are combined together. Later, we define heaps that only contain valid permissions. Valid permissions are permissions that can be obtained by splitting the maximal permission. As a corollary, any valid permission m satisfies the following inequality: m 0 < M m ≤ M m W . Our model, however, includes permissions that are bigger than m W , because we need to sum permissions above m W . That is why + M is a total operator. Our paper's results have been established for two concrete permissions models: Boyland's fractional permissions [START_REF] Boyland | Checking interference with fractional permissions[END_REF][START_REF] Bornat | Permission accounting in separation logic[END_REF] and the counting model of Bornat et al. [START_REF] Bornat | Permission accounting in separation logic[END_REF].

In the fractional permission model, permissions are rational numbers. The binary operator and the ordering are the usual + and ≤ on rationals, the minimal permission is 0 and the maximal permission is 1. All permissions are splittable, and splitting simply divides permissions in half: split1(m) = split2(m) = m 2 . In the counting model, permissions were originally represented by integers, but we re-encode them in a different manner to allow the use of a standard order. We encode permissions as a pair (n, i), where n is a natural number (in fact, only 0 or 1), and i is an integer. Intuitively, the first of the pair indicates whether this permission can be split, to give out further (read) permissions, while the second indicates a number of read permissions (positive to represent read permissions which have been obtained, and negative to represent those given out). The minimal permission is (0, 0), and the maximal permission is (1, 0). Permissions are added by pairwise addition of their components, and ordered by the lexicographic ordering. A permission is splittable if its first component is 1. The split functions are defined by: split1((1, i)) = (1, i -1) and split2((1, i)) = (0, 1).

We map Bornat's counting permissions onto our pairs model, by the following rules (in which n represents a positive integer):

0 → (1, 0) n → (1, -n) -n → (0, n)
We study both intuitionistic and classical separation logic [START_REF] Ishtiaq | BI as an assertion language for mutable data structures[END_REF]. Both flavours contains pure (heap independent) and spatial (heap dependent) formulas: → v has the same meaning as the harpoon but it enforces that the heap contains only the cell at address a. Intuitionistic (respectively classical) separation logic is obtained by taking Σ to be Σ I (respectively Σ C ) below:

n ∈ N a, v ∈ n | n + n | n -n | . . .
A, B ::= Π | Σ | A ⋆ A | A ∧ A | A ∨ A formulas
In A ⋆ B, ⋆ is the separating conjunction. A ⋆ B represents a heap consisting of two separate subheaps A and B. A ∧ B is the usual logical conjunction, which represents two different views of a heap. We do not include the standard implication ⇒ because this simplifies the situation by avoiding bunched contexts in the proof system [START_REF] O'hearn | The logic of bunched implications[END_REF]. The fact that most separation-logic-based program verifiers do not include a standard implication [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF][START_REF] Jacobs | The verifast program verifier[END_REF][START_REF] Distefano | jStar: Towards practical verification for Java[END_REF] supports our choice. In addition, we use a language without variables, but describe how variables interfere with our algorithm in Sec. 7.

Because our algorithms are defined in Coq [START_REF] Wadler | The Coq proof assistant reference manual V8.0[END_REF], we represent heaps as lists (which are well supported by Coq's standard library). A list entry is a triplet of an address, a valid permission, and a value:

c ::= (a, m, v) heap cells h ::= [] | c :: h heaps
We define a projection operator to extract a value from a cell: val(a, m, v) = v and we write h[a] to denote h's set of heap cells whose address are a:

[][a] = / 0 ((a, m, v) :: h)[a ′ ] = {(a, m, v)} ∪ h[a] if a = a ′ h[a] otherwise
We write h(a) to denote the sum of permissions to a occurring in h

: [](a) = m 0 ((a, m, v) :: h)(a ′ ) = m + M h(a) if a = a ′ h(a) otherwise
Conjunction of two heaps is simply list concatenation (written h@h ′ ) and compatibility of heaps is standard:

h # h ′ ∆ = (∀a) h(a) + M h ′ (a) ≤ m W and (∀c ∈ h[a], ∀c ′ ∈ h ′ [a])(val(c) = val(c ′ ))
The semantics of formulas is standard. In particular, the semantics of pure formulas is left unaxiomatized:

h |= iff Π oracle(Π) h |= iff emp h = [] h |= iff a m ֒→v (∃h ′ )(h = (a, m, v)@h ′ ) h |= iff a m → v h = (a, m, v) h |= iff A ⋆ B (∃h 1 , h 2 )(h 1 # h 2 , h = h 1 @h 2 , h 1 |= iffA, and h 2 |= B) h |= iff A ∧ B h |= A and h |= B h |= iff A ∨ B h |= A or h |= B
We write A ⊢ B to denote that A entails B. Appendix A shows ⊢'s definition, i.e., our proof system. It is driven by natural deduction rules that are common to the logic of bunched implications [START_REF] O'hearn | The logic of bunched implications[END_REF] and linear logic [START_REF] Wadler | A taste of linear logic[END_REF]. The only non-standard rules are (Splitting) and (Merging) [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF] that lift permission splitting to formulas. The proof system is sound w.r.t. to the semantics above:

THEOREM 1 (SOUNDNESS OF THE PROOF SYSTEM). If A ⊢ B, then for all h, h |= A implies h |= B.

Because we use it later, we spell out Thm. 1's contraposition:

THEOREM 2 (CONTRAPOSITION OF THM. 1). If there exists h such that h |= A and h |= B, then A B.

PRELIMINARIES

We abstract models of separation logic formulas (i.e., heaps) by their size. We use two abstractions of different precisions: the first abstraction is a whole heap abstraction while the second abstraction is a per cell abstraction. For the whole heap abstraction, the size of a heap is simply the sum of all permissions occurring in this heap:

size M ([]) = m 0 size M ((a, m, v) :: h) = m + M size M (h)
For the per cell abstraction, the size of a heap is a permission table i.e., the corresponding heap without values:

pt c ::= (a, m) permission table cells pt ::= [] | pt c :: pt permission tables size P ([]) = [] size P ((a, m, v) :: h) = (a, m) :: size P (h)
As for heaps, we write pt(a) to denote the sum of permissions to a occurring in pt. Sizes are equipped with an order. For the whole heap abstraction, we use the order on permissions ≤ M while for the per cell abstraction, we use an order on permission tables ≤ P :

pt ≤ P pt ′ ∆ = (∀a)(pt(a) ≤ pt ′ (a))
Sizes are equipped with minimum and maximum functions. For the whole heap abstraction, we use standard definitions according to the corresponding order on permissions ≤ M :

smin M (m, m ′ ) = m iff m ≤ M m ′ m ′ otherwise smax M (m, m ′ ) = m ′ iff m ≤ M m ′ m otherwise
For the per cell abstraction, we use definitions that merge permission tables point-wise:

smin P (pt, pt ′ ) ∆ = {pt ′′ | (∀a)(pt ′′ (a) = smin M (pt(a), pt ′ (a)))} smax P (pt, pt ′ ) ∆ = {pt ′′ | (∀a)(pt ′′ (a) = smax M (pt(a), pt ′ (a)))}
>From now on, we subscript functions when we speak about a concrete abstraction while we use functions without subscripts when we describe properties of both abstractions.

THE DISPROVING ALGORITHM FOR INTUITIONISTIC SEPARATION LOGIC

To disprove entailment between formulas in intuitionistic separation logic, we search for models with bounded sizes. Formally, we use min and max functions that satisfy the following property:

THEOREM 3 (PROPERTY OF min AND max). If h |= A, then there exist h s , h r such that h = h s @h r and h s |= A and min(A) ≤ size(h s ) ≤ max(A).

Intuitively, Thm. 3 states that, given a satisfiable formula A (i.e., there exists h such that h |= A), there exists a "small" model h s of A whose size is in between min(A) and max(A) (the possibility of a superfluous heap portion h r reflects the semantics of intuitionistic separation logic). Then, we use min and max to disprove entailment as follows: THEOREM 4 (min/max IS A DISPROVING ALGORITHM). If A is satisfiable and min(B) ≤ max(A) does not hold, then A B.

PROOF. Because A is satisfiable, there exists h such that h |= A. Then, by Thm. 3, it follows that there exists h s such that h s |= A and size(h s ) ≤ max(A). Now, suppose h s |= B. Then, by Thm. 3, it follows that min(B) ≤ size(h s ). From size(h s ) ≤ max(A), by transitivity, it follows that min(B) ≤ max(A). This contradicts, however, the hypothesis that min(B) ≤ max(A) does not hold. Hence, h s |= B.

From h s |= A and h s |= B, by Thm. 2, it follows that A B.

The reader might wonder why we formulate Thm. 4 with a negation on the ≤ operator instead of using a < operator. The reason is that, for permission tables, ¬(pt ≤ P pt ′ ) is not equivalent to pt ′ < P pt (where < P would be defined in a way similar to ≤ P ).

In the remainder of this section, we show definitions of min and max for the whole heap abstraction and the per cell abstraction.

Whole Heap Abstraction

min and max are defined as follows:

min(Π) = m 0 min(a m ֒→ v) = m min(A ⋆ B) = min(A) + M min(B) min(A ∧ B) = smax M (min(A), min(B)) min(A ∨ B) = smin M (min(A), min(B)) max(Π) = m 0 max(a m ֒→ v) = m max(A ⋆ B) = max(A) + M max(B) max(A ∧ B) = max(A) + M max(B) max(A ∨ B) = smax M (max(A), max(B))

Per Cell Abstraction

min and max are defined as follows:

min(Π) = [] min(a m ֒→ v) = (a, m) :: [] min(A ⋆ B) = min(A)@min(B) min(A ∧ B) = smax P (min(A), min(B)) min(A ∨ B) = smin P (min(A), min(B)) max(Π) = [] max(a m ֒→ v) = (a, m) :: [] max(A ⋆ B) = max(A)@max(B) max(A ∧ B) = smax P (max(A), max(B)) max(A ∨ B) = smax P (max(A), max(B))
Although max's definitions are very similar for the two abstractions, there is one case where they differ: in case ∧ of max. In analogy with the per cell abstraction, one could expect max(A ∧ B) to be smax M (max(A), max(B)) in the whole heap abstraction. To see why this is unsound, however, one can consider a formula where the right and left hand sides of a ∧ represent separate parts of the heap such as 42

THE DISPROVING ALGORITHM FOR CLASSICAL SEPARATION LOGIC

To disprove entailment between formulas in classical separation logic, we pursue a slightly different goal than for intuitionistic separation logic: instead of exhibiting one model whose size is bounded, we search for bounds on the size of all models.

Because we allow pure formulas, which do not constrain the size of heaps modelling them, we cannot always find an upper-bound on the size of heaps. Hence we add a distinguished "maximal" size that we write ∞ (both for the whole heap and for the per cell abstraction). The meaning of ∞ is axiomatized as follows:

(∀m)(m ≤ M ∞) (∀pt)(pt ≤ P ∞)

THEOREM 5 (PROPERTY OF min AND max). If h |= A, then min(A) ≤ size(h) ≤ max(A).

Then, we use min and max to disprove entailment as follows: THEOREM 6 (min/max IS A DISPROVING ALGORITHM). If A is satisfiable and min(B) ≤ max(A) does not hold, then A B.

PROOF. Similar to the proof of Thm. 4.

In the remainder of this section, we give definitions of min and max for the whole heap abstraction and the per cell abstraction. For min, we only show its definition in case of a formula emp; for other cases min's definition is similar to the intuitionistic case (see Sec. 4.1 and 4.2).

Whole Heap Abstraction

min and max are defined as follows:

min(emp) = m 0 max(Π) = ∞ max(emp) = m 0 max(a m → v) = m max(A ⋆ B) = max(A) + M max(B) max(A ∧ B) = smin M (max(A), max(B)) max(A ∨ B) = smax M (max(A), max(B))
As an example, consider the following computations of the maximum and minimum of two formulas (for the fractional permissions model):

max((42 1 → _ ⋆ 47 1 /2 → _)∨ ((42 1 → _ ⋆ 47 3 /4 → _) ∧ (47 1 /2 → _ ⋆ 47 1 /4 → _ ⋆ 42 1 → _))) = max M (1 + M 1 /2, min(max(42 1 → _ ⋆ 47 3 /4 → _), max(47 1 /2 → _ ⋆ 47 1 /4 → _ ⋆ 42 1 → _))) = smax M ( 3 2 , smin M ( 7 4 , 7 4
)) = 7 4 min(42

1 → _ ⋆ 47 1 /2 → _ ⋆ 47 1 /2 → _) = 1 + M 1 2 + M 1 2 = 2 Now, because 2 ≤ M 7 /4
does not hold, our algorithm deduces:

(42 1 → _ ⋆ 47 1 /2 → _) ∨ ((42 1 → _ ⋆ 47 3 /4 → _) ∧ (47 1 /2 → _ ⋆ 47 1 /4 → _ ⋆ 42 1 → _)) 42 1 → _ ⋆ 47 1 /2 → _ ⋆ 47 1 /2 → _
We now compare max's definition for ⋆ and ∧ in both semantics (similar remarks will apply for the per cell abstraction).

• In the classical semantics, we have max(A ⋆ B) = max(A)

+ M max(B), while we have max(A ∧ B) = smin M (max(A), max(B)). This reflects the intuition that, (1) in A ⋆ B, A and B represents separate heaps while (2) in A ∧ B, A and B represents different views of the same heap.

• In the intuitionistic semantics, however, we have max

(A ⋆ B) = max(A ∧ B) = max(A) + M max(B)
. This reflects that, both in A ⋆ B and in A ∧ B, A and B must (for ⋆) or may (for ∧) represent separate parts of the heap.

Per Cell Abstraction

min and max are defined as follows:

min(emp) = [] max(Π) = ∞ max(emp) = [] max(a m → v) = (a, m) :: [] max(A ⋆ B) =      max(A)@max(B) if max(A) = ∞ and max(B) = ∞ ∞ otherwise max(A ∧ B) = smin P (max(A), max(B)) max(A ∨ B) = smax P (max(A), max(B))
In this case, the definitions of max are similar in both abstractions.

On ∞

We elaborate here on the consequence of our use of ∞ above for the whole heap abstraction (similar comments apply to the per cell abstraction).

The ⋆ and ∨ connectives have a different behavior w.r.t. ∞ than ∧. To see why, consider the following properties of + M , smin M , and smax M w.r.t. ∞:

(∀m)(m + M ∞ = ∞ + M m = ∞) (∀m)(smin M (m, ∞) = smin M (∞, m) = m) (∀m)(smax M (m, ∞) = smax M (∞, m) = ∞)
Because of the properties above, both the ⋆ and ∨ operators "spread" ∞:

for op ∈ {⋆, ∨}, max(A op B) = ∞ if max(A) = ∞ or max(B) = ∞. The ∧ operator, however, stops ∞ from spreading: max(A ∧ B) = ∞ if max(A) = ∞ or max(B) = ∞.
Because the variants of separation logic used in program verifiers [START_REF] Berdine | Smallfoot: Modular automatic assertion checking with separation logic[END_REF][START_REF] Distefano | jStar: Towards practical verification for Java[END_REF] impose pure formulas and spatial formulas to be ∧conjoined at the top level, max would never return ∞ in these variants.

PRECISION

Ideally, min and max's definitions need to be as tight as possible, while retaining soundness (Thms. 3 and 5). We exemplify this for both flavours of the logic. Our explanations focus solely on the whole heap abstraction but our remarks apply to both abstractions.

• In the intuitionistic semantics, we have max(A ∧ B) = max(A) + max(B). At first sight, this might appear too loose, but the semantics of the harpoon requires this definition for soundness. To see why, one can consider a formula in which the right and left hand sides of a ∧ represent separate parts of the heap, such as 42

1 ֒→ _ ∧ 47 1 ֒→ _.
• In the classical semantics, we have max(A ∧ B) = smin M (max(A), max(B)). This definition is tight: if max(A) < max(B), by ∧'s semantics, it follows that any model of B whose size is greater than max(A) cannot be a model of A ∧ B (and conversely). In the classical semantics, we have

max(A ∨ B) = smax M (max(A), max(B)
). This definition is also tight because, if max(A) < max(B), by ∨'s semantics, it follows that a model of B can be a model of A ∨ B (and conversely).

EXTENSION TO OTHER OPERATORS OF SEPARATION LOGIC

In this section, we review extensions of our algorithm for which our results are partial. Our algorithm has been extended to deal with the magic wand solely for the classical semantics (Sec. 7.1), soundness of min and max for quantifiers has been checked only on pen and paper (Sec. 7.2), and variables have been integrated only with the whole heap abstraction (Sec. 7.3).

The magic wand --⋆

The magic wand --⋆ matches the resource conjunction ⋆, in the sense that the modus ponens law is satisfied:

A⋆(A--⋆ B) implies B.
The magic wand's semantics quantifies over models of the wand's left-hand side:

h |= A --⋆ B iff (∀h ′ )((h ′ |= A and h ′ # h) implies h ′ @h |= B)
In the classical semantics, we have mechanically verified that our algorithm can be extended to deal with the magic wand. Because min and max are now mutually recursive, min, like max, can return ∞. For the whole heap abstraction, definitions of min and max from Sec. 5.1 are completed as follows (see Appendix B for the per cell approximation):

min(A --⋆ B) =      min(B) -M max(A) if min(B) = ∞ and max(A) = ∞ m 0 otherwise max(A --⋆ B) =      max(B) -M min(A) if max(B) = ∞ and min(A) = ∞ ∞ otherwise
For these definitions to be sound, we need to assume that formulas appearing on the left-hand side of the magic wand are satisfiable. While this is harmful from a theoretical point of view, the literature so far on program verification that uses the magic wand in examples [START_REF] Haack | Separation logic contracts for a Java-like language with fork/join[END_REF][START_REF] Haack | Resource usage protocols for iterators[END_REF] suggests this is a plausible assumption for program verifiers.

We believe this definition could be adapted for the intuitionistic semantics, but it is a non-trivial task. In a nutshell, the universal quantification in the magic wand's semantics and the way Thm. 3 is formulated (i.e., with an existential quantifier) prevent a simple proof by induction, and we leave this for future work.

Quantification

We distinguish between quantification on values and permissions. We add the following formulas to Sec. 2's language:

A, B ::= . . . | ∃v. A | ∃m. A | ∀v. A | ∀m. A
The semantics is standard and we omit the corresponding proof rules which are also standard. To define min and max, we introduce a "very small permission" ε ∈ M . The meaning of ε is axiomatized by: (∀m)(m < M m + M ε)

For both abstractions min and max are defined as follows:

min(∃v. A) = min(A) max(∃v. A) = max(A) min(∃m. A) = min(A[ε/m]) max(∃m. A) = max(A[m W /m]) min(∀v. A) = min(A) max(∀v. A) = max(A) min(∀m. A) = min(A[m W /m]) max(∀m. A) = max(A[m W /m])

Variables

In real-world flavours of separation logic, variables are used. For the whole heap abstraction, variables (including quantification over variables) do not create any extra difficulties for our work. For the per cell abstraction, it is unclear at this stage how variables can be handled elegantly, and we leave this for future work.

COMPLEXITY

The complexity of our techniques is linear for the whole heap abstraction, and O(n(log n)) for the per cell abstraction (where n is the input formula's size). To our knowledge, there is no complexity result for entailment checking in separation logic. We believe the complexity of our disproving algorithm is low enough to be useful when entailment must be checked quickly. This is supported by the fact that integrating both the magic wand and quantifiers do not increase our algorithm's complexity, while they typically increase by orders of magnitude the complexity of model-checking or validity-checking [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Brochenin | On the almighty wand[END_REF].

SOUNDNESS

All theorems from Sec. 2, 4, and 5 have been mechanically checked with Coq [START_REF] Wadler | The Coq proof assistant reference manual V8.0[END_REF]. Addition of the magic wand (Sec. 7.1) for the classical semantics has also been mechanically checked. Proofs about the proof system (Thms. 1 and 2); properties of permissions, heaps, permissions tables etc. are 3090 lines long. The proofs of Thms 3, 4, 5 and 6 are 620 lines long. The proofs have been engineered so that certified implementations of the two abstractions could be extracted. Proof scripts are available online [START_REF]Coq proof scripts[END_REF].

Proofs for quantifiers (Sec. 7.2) have been checked only on pen and paper.

RELATED WORK AND CONCLUSION

Related Work.

In the context of program verifiers, checking entailment between separation logic formulas has been studied for while languages [START_REF] Berdine | Symbolic execution with separation logic[END_REF] and object-oriented languages [START_REF] Distefano | jStar: Towards practical verification for Java[END_REF][START_REF] Chin | Enhancing modular OO verification with separation logic[END_REF]. In these fragments, the magic wand --⋆ is omitted and special predicates for describing data structures are present.

Properties (decidability, undecidability, and complexity) both for model checking and for validity have been studied [START_REF] Calcagno | Computability and complexity results for a spatial assertion language for data structures[END_REF][START_REF] Berdine | A decidable fragment of separation logic[END_REF][START_REF] Brochenin | On the almighty wand[END_REF]. To our knowledge, disproving entailment has only been studied in a fullyfledged tableaux procedure [START_REF] Galmiche | Tableaux and resource graphs for separation logic[END_REF]. The cited work's algorithm for checking entailment can generate either proofs or counter-models, whereas our algorithm focuses on disproving entailment and does not generate counter-models.

Conclusion.

We have presented new techniques for disproving entailment between separation logic formulas, which we believe to be particularly relevant in the context of automated provers for separation logic. Because our algorithm's complexity is low, it is of interest wherever entailment checking needs to be checked quickly. We have provided two different techniques (of different precision), each of which can be applied to both the intuitionistic and classical flavours of separation logic. We provide mechanical proofs of the soundness of our techniques [START_REF]Coq proof scripts[END_REF].

(Id)

A ⊢ A A ⊢ B (Weak) A,C ⊢ B oracle(Π) (Oracle) true ⊢ Π A 1 ⊢ B 1 A 2 ⊢ B 2 (⋆ Intro) A 1 , A 2 ⊢ B 1 ⋆ B 2 A ⊢ B 1 ⋆ B 2 C, B 1 , B 2 ⊢ D (⋆ Elim) A,C ⊢ D A, B 1 ⊢ B 2 (--⋆ Intro) A ⊢ B 1 --⋆ B 2 A ⊢ C 1 --⋆ C 2 B ⊢ C 1 (--⋆ Elim) A, B ⊢ C 2 A ⊢ B 1 A ⊢ B 2 (∧ Intro) A ⊢ B 1 ∧ B 2 A ⊢ B 1 ∧ B 2 (∧ Elim 1) A ⊢ B 1 A ⊢ B 1 ∧ B 2 (∧ Elim 2) A ⊢ B 2 A ⊢ B 1 (∨ Intro 1) A ⊢ B 1 ∨ B 2 A ⊢ B 2 (∨ Intro 2) A ⊢ B 1 ∨ B 2
∨ does not occur in A (Splitting) A ⊢ split1(A) ⋆ split2(A) ∨ does not occur in A (Merging) split1(A) ⋆ split2(A) ⊢ A In the proof rules (Splitting) and (Merging), we use split1 and split2 (defined below) to lift permission splitting to formula splitting. The conditions on the proof rules for splitting and merging, ensure that no disjunctions occur within the formulas concerned. This is because splitting and merging is unsound for disjunctions (and formulas with the magic wand). As we only split formulas without these connectives, we need not define those cases for the definition of splitting formulas:

B. OMITTED CASES

The definitions of min and max from Sec. 5.2 are completed as follows (where -P is defined by applying the unary -M operator point-wisely to permission tables):

  addresses and values m abstract permissions Π ::= a = a | a = a | true | . . . pure formulas Σ I ::= a m ֒→ v intuitionistic spatial formulas Σ C ::= emp | a m → v classical spatial formulas In intuitionistic separation logic, the atomic spatial formula is the harpoon a m ֒→ v while in classical separation logic, the atomic spatial formula is the points-to predicate a m → v. The harpoon a m ֒→ v has a dual meaning. Firstly, a m ֒→ v asserts that the heap contains a cell at address a with content v. Secondly, a m ֒→v asserts permission m to the cell at address a. If m = m W , a m ֒→ v asserts write and read authorization to the cell at address a, otherwise it asserts readonly authorization. The points-to predicate a m

1 ֒→ _ ∧ 47 1 ֒→

 11 _ (where _ denotes irrelevant values).

Figure 1 Fig. 1

 11 Figure 1: Proof Sytem

  ⋆ B) = split1(A) ⋆ split1(B) split1(A ∧ B) = split1(A) ∧ split1(⋆ B) = split2(A) ⋆ split2(B) split2(A ∧ B) = split2(A) ∧ split2(B)

  )@ -P (max(A)) if min(B) = ∞ and max(A) = ∞ [] otherwise max(A --⋆ B) =    max(B)@ -P (min(A)) if max(B) = ∞ and min(A) = ∞ ∞ otherwise

Acknowledgments.

We thank Didier Galmiche and Marieke Huisman for their fruitful comments about this paper. Hurlin was supported in part by IST-FET-2005-015905 Mobius project and ANR-06-SETIN-010 ParSec project.


Johannes Kanig
email: kanig@lri.fr

Jean-Christophe Filliâtre

Who: A Verifier for Effectful Higher-Order Programs

Keywords:

We present Who, a tool for verifying effectful higher-order functions. It features Effect polymorphism, higher-order logic and the possibility to reason about state in the logic, which enable highly modular specifications of generic code. Several small examples and a larger case study demonstrate its usefulness. The Who tool is intended to be used as an intermediate language for verification tools targeting ML-like programming languages.

Introduction and Motivation

Higher-order functions are a key feature, not only of purely functional languages like Haskell and the pure fragment of ML, but also in combination with imperative features, like references. The presence and frequent use of higher-order functions such as Array.iter in Ocaml prove this importance. However, reasoning about higher-order functions is difficult, and especially so in the presence of effectful computations. Any function's specification depends on its arguments. In a higher-order setting, arguments may be functions that have their own specification. In consequence, to be modular, the specification of a higher-order function can only be formulated depending on the specifications of its functional arguments. In a setting where side effects are possible, one also needs to formulate the specification depending on the side effects of the functional arguments. We claim that to be truly modular, the specification of a higher-order function must be generic with respect to the specification and the effect of its arguments.

We present the tool Who1 , an intermediate language aimed at verification of effectful higher-order programs. It features effect polymorphism, a higher-order logic to conveniently formulate specifications as well as special objects in the logic which repre-sent different states of parts of the store. This permits for natural specifications and proof obligations.

The Who tool has one fundamental restriction: aliasing of references is excluded. This allows for vastly simpler specifications. We do not consider this a limitation, because Who is intended to be used as an intermediate language, target of a more sophisticated analysis tool. Such a tool could, using some memory model, translate for example Ocaml programs to the Who language. A similar approach has been applied successfully to first-order programs and object oriented programs (Filliâtre and Marché 2007). In the absence of such a tool for Ocaml programs, all the examples in this paper have been proved correct directly using Who.

Section 2 recalls the basic principles of tools based on Hoare logic. This section can be skipped by readers who are already familiar with Hoare logic, perhaps with the exception of section 2.1. Section 3 explains the new concepts introduced by Who with many examples. In section 4, as a more complex case study, the Koda-Ruskey algorithm is considered.

A Short Introduction to Hoare Logic

Hoare logic is concerned about correctness of programs2 . Consider the following simple program which fills an array ar with the value v, starting from ofs for len cells3 . let fill ar ofs len v = for i = ofs to ofs + len -1 do set ar i v done where set ar i v sets cell at index i of array ar to the value v. Now Hoare logic permits to write pre-and postconditions for such a function, specifying using logical formulas what fill does or should do. The postcondition specifies what should be true after executing the function. In this case, we want the function to set all the elements between ofs and ofs + len -1 to v:

∀(k : int). ofs ≤ k ≤ ofs + len -1 → get ar k = v. For the postcondition to be complete, one should also specify that the array remains unchanged outside of [ofs..ofs + len -1].

We also need to add a precondition. Indeed, the function fill won't work for unsuitable values of ofs and len. We have to require 0 ≤ ofs ≤ length ar -len ∧ 0 ≤ len. The function is now specified from the outside -we have written down its pre-and postcondition. Using this specification and the rules of Hoare logic, we can prove that every use of fill adheres let fill (ar : α array) (ofs : int) (len : int) (v: α) = { 0 ≤ ofs ≤ length ar -len ∧ 0 ≤ len } for i = ofs to ofs + len -1 do { ∀(k : int). ofs ≤ k < i → get ar k = v } set ar i v done { ∀(k : int).

ofs

≤ k ≤ ofs + len -1 → get ar k = v } Figure 1. A simple first-order program.
to the requirements and does not use more information than what we have specified. However, to be able to prove the correctness of fill itself, with respect to the specification we have given, some more annotations are needed. In this case, the function body is a simple for loop. If we can state a formula which is initially true, preserved by the loop body, and which, using the upper loop bound, implies the postcondition, we are done. Such a formula is called a loop invariant. In this case, the invariant is simply a reformulation of the postcondition:

∀(k : int). ofs ≤ k → k < i → get ar k = v
For i = ofs + len, this clearly implies the postcondition. Also, assuming the precondition, the formula is initially true for i = ofs (because the premise of the implication is false). Fig. 1 summarizes the specification of the function fill.

The essence of traditional Hoare logic is what we have shown in this section: every function comes with a pre-and postcondition, loops have loop invariants. Before calling a function (entering a loop), one has to show that one can derive the precondition (the loop invariant) from the current context. Returning from a function call (exiting a loop), one can add the postcondition (the loop invariant) to the current context and proceed. The mechanical work of traversing the program code and generating proof obligations can be automated. Typically, one starts from the postcondition, traverses the code in reverse order and establish a necessary precondition; this is called a weakest precondition calculus.

There are many tools which implement Hoare logic in the described or a similar way. Examples are the Why platform [START_REF] Filliâtre | Verification of Non-Functional Programs using Interpretations in Type Theory[END_REF]) and the Boogie system [START_REF] Barnett | Boogie: A Modular Reusable Verifier for Object-Oriented Programs[END_REF].

Functional Programs

The mechanism we have shown in the previous section leaves some open questions when it comes to higher-order functions. It is unclear how to deal with the following code, for example: let apply f x = f x We can't give a precondition to apply because we don't know yet what function it is applied to. Similarly, we don't know what postcondition we can guarantee after calling f.

Intuitively, however, the situation is clear: apply should have the same precondition and postcondition as its argument f. In the Pangolin system [START_REF] Régis | A Hoare logic for call-by-value functional programs[END_REF] this can be expressed like this: let apply f x = { pre f x } f x { r : post f x r } Here, we state that the precondition of apply is the precondition of f applied to x and that the result r of apply does verify the postcondition of f applied to x. One can see that in Pangolin, f is treated quite differently in the logic and in the program. Indeed, types of functional objects are translated as follows. The function type t1 → t2 becomes a tuple type in the logic:

(t1 → prop) × (t1 → t2 → prop) A (program)
function becomes a pair of predicates, precisely its pre-and postcondition. This serves two purposes. First, this makes it impossible to call the function in the logic, avoiding issues with effectful and nonterminating functions. Second, it gives access to the specification of the function. The terms pre and post above are simply other names for fst and snd. To make things work out, however, this trick requires a higher-order logic, a logic where one can quantify over predicates, store predicates in tuples, etc.

Using this technique, the Pangolin system is capable of reasoning about purely functional higher-order functions as well as common constructs of function programs such as algebraic datatypes and pattern matching. The Pangolin system cannot deal with effectful functions.

Logic Functions and Axioms

In tools for program verification, one is often confronted with the problem of specifying the behaviour of a program where the most natural description of the behaviour is the program itself! Let us take an example: Suppose we want to prove correct the following program, computing the maximum of two integer values: let max (a b : int) = if a < b then b else a How can one express the specification of the program? One would like to say that it computes the maximum of its arguments, but then one would need to define maximum, and this definition would probably look like the body of max. The way out is to state the properties one expects from the maximum of two values. At least, one would like to have the two properties that if a ≤ b, then max a b = b and similarly if b ≤ a. From here, there are now two possibilities: one can either accept max as the definition of the maximum function and prove that it verifies the two desired properties. Or one can declare a logical function max with two integer arguments, postulate the two desired properties as axioms and define a program function pmax whose specification states it computes precisely the logical function max. In other words, one has to write:

logic max : int → int → int axiom maxright : ∀(a b : int) a ≤ b → max a b = b axiom maxleft : ∀(a b : int) a >= b → max a b = a let pmax (a b : int) =
if a < b then b else a { r : r = max a b } Notice that we have not given a definition for max, we have only postulated its existence. The other difference between a logical and a program function is that a logical function has to terminate and cannot have any side effects. In the Who system, these are also the only differences. Indeed, one can use logical functions in programs, if it is convenient. Continuing the above example, if one is not interested in the (trivial) correction of pmax, one can omit the definition of pmax and directly use max in the rest of the program. This also helps to avoid the recurring problem of defining everything twice -in the logic and in the program. As a final remark, let us state that this sharing between logic and programs is reminiscent to traditional Hoare logic, where arithmetic and boolean expressions are shared in the logic and in the program.

Modeling Data Structures. We can also apply this mecanism of logical declarations to model more complex data structures that are not a priori part of the programming language. For example one can define immutable arrays simply by postulating their existence as follows: type α farray logic get : ∀α. α farray → int → α logic set :

∀α. α farray → int → α → α farray logic length : ∀α. α farray → int Notice that the type farray describes functional (i.e., immutable) arrays. The set function returns a new array instead of unit. One also needs to specify axioms to describe the behaviour of these functions. This so-called theory of arrays is standard. From this starting point, one can model imperative arrays by representing them as references to functional arrays. An array update in Ocaml syntax (setting the array a at index i to x) a.(i) ← x becomes a := set !a i x In words: set returns a new array which has been modified at index i and we set the contents of a to this new array.

The examples in this paper using the Who system all use the above model for arrays. In the following, α array is thus an abbreviation for a reference to a α farray. The reader should keep in mind that Who is an intermediate language and that this kind of transformation could be done automatically. It shall be noted that this particular approach has the drawback that the array length is part of the state of an array. So, according to the model, an array update can change the length of an array. We therefore need an additional axiom which states that update does not change the length of the array. In the following, when dealing with arrays, we will omit annotations that deal with this issue.

An Overview of Who

The Who system is an effort to combine the complementary aspects of traditional first-order tools such as Why and the higher-order tool Pangolin. It contains the features we have described before: traditional Hoare style reasoning, logic declarations and axioms as well as reasoning about higher-order functions. In this section, we discuss the modifications present in Who, which are necessary to specify effectful higher order functions.

Features of Who

Regions. To be able to state properties about references, one needs to track them in a special way. It is clear that program identifiers are not suitable to track references, because several identifiers may denote the same physical reference. A standard solution to this problem is the use of regions [START_REF] Tofte | Region-based memory management[END_REF] to denote references. A region is simply an identifier for a reference cell, but on type system level. Reference types are annotated with a region: t refρ denotes the type of references which point to the cell ρ, which contains an object of type t. Annotated in this way, reference types become singleton types; each such type has only a single inhabitant, precisely the reference cell with that region name. One recovers typing flexibility by adding region polymorphism, which permits to use a function at different reference types.

From a specification point of view, regions replace program identifiers when dealing with objects stored in reference cells. However, in most situations (and in all situations in this paper), it is convenient to introduce syntactic sugar which permits use a program variable x instead of a region ρ, if x is of type t refρ. This will be done systematically throughout the document.

Effects. A distinguished feature of the Who system is the use of an effect system. In Ocaml, the type of fill is

α array → int → int → α → unit, but in Who, its type becomes ∀ar. α farray refar → ∅ int → ∅ int → ∅ α → {ar} unit
Every arrow is annotated with an effect, i.e. the list of regions which might change on function application. Here, only when all arguments are applied, the function has an effect on its first argument ar. The quantifier at the beginning binds the region ar, making it possible to use fill with different arrays.

To take effects into account, we also need to modify the way functions are handled in the logic. First, we introduce a new type for states, also called effect records in the logic. To every effect expression e we attribute an effect type e which represents the part of the store which contain exactly these reference cells. Similarly to the Pangolin system, a function of type t1 → {e} t2 is translated to its pre and postcondition

(t1 → e → prop)×(t1 → e → e → t2 → prop).
The precondition has an additional argument which corresponds to the state when entering the function. The postcondition has two additional arguments representing the states before and after executing the function. The corresponding arguments corresponding to states contain only the mutable variables which are relevant to the execution of the function. We will see many uses of this mechanism in the following.

Effect polymorphism and the aliasing restriction. So far we have seen that the specification of a functional argument, such as f in the example of apply, can be dealt with generically. But we also need to deal with the effect of f. Consider the following code:

let apply_reset f x = r := 0; f x where, before calling f, some global integer reference r is set to 0. Can we claim that r contains 0 after execution of the function body? And what can we say about the effect of f? The Who system answers the second question as follows. As we don't know the effect of f, we introduce an effect variable e for its effects and go on as before. This variable is generalized at the let-binding, just as type variables. The following code in Who shows some new elements of the syntax:

let apply_reset [e] (f : α → {e} β) (x : α) =
{ pre f x e} r := 0; f x { res : r = 0 ∧ post f x e |old e res} The brackets after the function name introduce an effect variable. We can use the effect variable e in the effect of f. We have to require the precondition of f applied to x and the effect represented by e. The postcondition states that r contains 0 and that we have the postcondition of f on its own part of the store, relating the old (e |old ) and the new state (e).

The reader is probably puzzled by the syntax of the annotations of the previous paragraph. Let us explain a bit more. The precondition of apply_reset as stated above is an abbreviation for the following predicate:

(fun (cur : r e ) → pre f x e |cur ) The precondition of every function introduces its own name for the current piece of state cur which corresponds to its effects (r and e here). One can refer to the components of this state (access the field of the effect record) by writing the name of the field and a bar |, followed by the name of the effect record. The explicit introduction of the current state cur can be omitted, it will be done automatically. Also, there is a notion of default state. In the preand postconditions, the default state is always cur, so fields of this state can simply be referred to by their name. We have made use let for [e] (inv : e → int → prop) (start : int) (end : int) (f : int

→ {e} unit) = { inv cur start ∧ ∀(i : int). start ≤ i ∧ i ≤ end → ∀(m : e ). inv m i → pre f i m ∧ ∀(n : e ). post f i m n () → inv n (i+1) } let rec aux (i : int) : int → {e} unit = {start ≤ i ∧ i ≤ end + 1 ∧ inv cur i} if i ≤ end then let () = f i in aux (i + 1) else () {inv cur (end + 1)} in if start ≤ end + 1 then aux start else () { inv cur (max start (end + 1))} Figure 2
. The for loop as a higher-order function.

of similar abbreviations for the postcondition, in which there is an additional state old, representing the state before exectuting the current function.

The reader may still wonder how we can claim r = 0 in the postcondition of apply_reset. The reason is the aliasing restriction of the Who system, herited from the Why system. Effect variables, introduced at let-bindings, are assumed to be disjoint from the other effects of the function. In our example, the effect e cannot contain r. This is verified when the effect variables are instantiated; invalid instantiations are rejected.

The region mechanism prevents other forms of aliasing as well. First of all, the instantiation of regions is subject to a similar restriction, to avoid aliasing between reference variables. Furthermore, since reference types are annotated with regions, polymorphic containers (lists, arrays) may not contain references to locations. An array of type int refr array can only contain pointers to the same reference cell. Finally, while references to functions are allowed and supported, a stratification of the store similar to [START_REF] Boudol | Fair cooperative multithreading or typing termination in a higher-order concurrent imperative language[END_REF] prevents circular use of references, such as Landin's knot [START_REF] Landin | The mechanical evaluation of expressions[END_REF]. The aliasing restriction is the key to simpler annotations.

To summarize, let us define the syntax of types:

t ::= int | bool | .. | t → t | t → {e} t | t × t | t
refr where r stands for a region name and e stands for an effect, i.e. a set of regions and effect variables. Types without the effectful arrow and without reference types can be used in the logic.

From a theoretical point of view, Who is based on a weakest precondition calculus which can deal with effect polymorphism and higher-order functions. The definition and correctness of this calculus are developped in [START_REF] Kanig | Proof of higher-order programs with effect polymorphism[END_REF].

Higher-order Specifications Involving State

We are now in the position to give examples for the specification of effectful higher-order functions. We consider two examples: a for loop implemented as a recursive function and the higher-order iterator for arrays.

The for loop as higher-order function. In a higher-order language, one can implement the first-order for loop by a function for : int → int → (int → unit) → unit, where the two integer arguments are the start and end value of the for loop, and the function argument corresponds to the body of the for loop and depends on the current value of the counter. While it is better to add the for loop directly to the language for convenience, let us demonstrate how to implement and specify such a function in the Who system.

As for is a higher-order function, it must be polymorphic with respect to the effects of its function argument. This is easily achieved by giving it the type for : ∀e. int → int →(int → {e} unit) → {e} unit If we want to be able to use this function in a way similar to the for loop in first-order Hoare logic, we also need the notion of invariant. As we can have logical arguments in the language, the simplest solution is just to add the invariant as an argument of the function. In this case, the invariant depends on the counter and the part of the state that is modified by the body of the loop. It thus can be given the type e → int → prop. In summary, the for function we want to implement has the following type: 2 shows a possible implementation along with its specification. The looping construct is replaced by a recursive function aux which tests if the counter is still below the end value, executes the body and continues recursively, if this is the case. Otherwise, it does nothing. Finally, we enter this auxiliary function only when the start value is actually at least as small as the end value.

for : ∀e. ( e → int → prop) → int → int → (int → {e} unit) → {e} unit Figure
From a specification point of view, the aux function corresponds exactly to the body of the for loop. Here we know that i is between the start and the end value (however, we may have exceeded the end value by one, because we test at the entry of the loop, not at the exit), and we know that the invariant is true for the current value of i and the current state, designated by the special variable cur. At the exit of the auxiliary function, we know that we have iterated until the end value.

To be able to prove the correctness of aux, we need the following premises: When the precondition of aux is true and when i ≤ end (the then branch of the conditional), the precondition of f is true as well (we have the right to call f). Also we need to prove that once we have called f, i.e., we have its postcondition, we can deduce the precondition of aux for the next step, where i is incremented by one. All these proof obligations cannot be proved here, because we do not know the invariant, nor do we know the pre-and postconditions of f. Therefore, they are stated in the precondition of for. To use for with some particular invariant and loop body, this precondition must be valid. Note that the proposed implementation and specification of for is not the only possibility, nor is it the most general one. For convenience, we have required the invariant to be true at least for the initial state. One could imagine a specification where this is only required when the loop body is executed at least once. In this case, the postcondition of for would need to express that nothing has changed otherwise.

i = 0 i nv 0 s0 i = 1 i nv 1 s1 • • • i = n -1 i nv (n -1) sn-1 i = n i nv n sn
Iteration over Arrays. Once we have expressed the specification of the for higher-order function, we can move on the more complex iteration schemes. For example, the iteration function for arrays4 is a very often used higher-order function, and it is exclusively used for the side effects it produces. It can be implemented as follows in Ocaml: let iter f a = for i = 0 to length a -1 do f (get a i) done where get a i denotes the ith element of array a.

Figure 3 shows the implementation of this function in Who. In some sense, it is simply a special case of the specification of the for loop seen in the previous section. It is a good example of a more interesting manipulation of state in the logic.

First of all, the specification of iter is similar to the specification of for. We require some kind of "stepping" condition from the function f to be iterated on (lines 6 to 9). We also expect an invariant as argument, which has to hold for the starting point of the iteration and which is guaranteed to hold for its final state. However, the pre-and postcondition of f now depend on a state which is smaller than the overall effect of the loop body. Indeed, f only affects e, the unknown part of the store, while the overall effect also contains read effects on ar, the array we iterate over. Remember that ar and e are disjoint, by the typing constraints of the language. Therefore, we can reason about the evolution of these two components independently. For example, we state in the precondition of iter that the invariant, for any step i and some corresponding state m, implies the precondition of f for the i-th cell of the array and the part of m designated by e (line 7). Similarly, the postcondition of f must ensure that the invariant is preserved (line 9).

Additionally, the invariant may refer to the current contents of ar. Therefore inv is introduced with type inv : ar e → int → prop where the first argument is the current state and the second argument is the current step i (line 2). Fig. 4 summarizes the succession of states of Array.iter.

Let us try to use iter to sum all the elements of an integer array. To specify this instance, we need a (logical) function which gives us the sum of an immutable array: logic sum_array : int → int array → int axiom sum_array_none : ∀(t : int array). sum_array 0 t = 0 axiom sum_array_step : ∀(t : int array) (i : int). 0 ≤ i → i < length t → sum_array (i+1) t = sum_array i t + get i t The logical term sum_array k a describes the sum of the elements of the array a up to (but not including) k. This logical description of the problem is the key to the specification; here is the annotated code: {} sum := !sum + z { sum = sum |old + z} ) {sum = sum_array (length ar) ar } Note that the effect and type polymorphic function iter has to be instantiated before use; we do not currently support type and effect inference. Concretely, the effect variable is instantiated with the effect of the function argument, {sum} here, and the type variable is instantiated with int, the content type of the array. This instantiated version is then applied to the array, an invariant, and a function which accumulates the sum of its integer arguments in a reference sum. The specification of this function simply states that it increments sum by its argument; it doesn't relate sum to the contents of the array. The invariant of the iteration is a logical function, introduced by {{...}}. It simply states that sum contains the sum of the elements of the array up to k, using the logical function sum_array. As the postcondition of iter guarantees the invariant for the last iteration state and the length of the array, we can deduce that sum finally contains indeed the sum of the array.

Notice that it is possible to write a variant of iter where the function argument is specified to modify the array argument. The specification and proof of this variant are essentially the same as the one we have shown.

Proof obligations

Specifying programs is but one part of the task of proving program correctness. The two other main tasks are

• generating proof obligations from the specification and

• proving these obligations. We have seen that Who deals with the part which concerns the generation of proof obligations, thanks to its weakest precondition calculus. It remains the last point, the task of actually proving them. Currently, Who only outputs the proof obligations in Coq syntax. The proofs can then be done inside the proof assistant [START_REF] Coq | The Coq Proof Assistant Reference Manual -Version V8.1[END_REF]. If one changes the program or its specification, an already existing proof script is updated to match the new proof obligations.

A Complete Case Study

This section presents a realistic and non trivial case study involving an effectful continuation-based functional program. This example is contained in Who's sources.

Koda-Ruskey's Algorithm

The algorithm considered in this section is due to Y. Koda and F. Ruskey (Koda and Ruskey 1993;Knuth 2001). It enumerates the ideals of certain finite partially ordered sets-namely, those whose Hasse diagram is a forest-as a Gray code. The algorithm can be described in a simple way. The task is to enumerate all colorings of a given, arbitrary forest. A coloring consists in marking every node as either black or white, with the sole constraint that all descendants of a white node be white as well. For instance, the following forest:

(1) admits exactly 15 distinct colorings, all of which are given in Figure 5. By definition, a sequence of colorings forms a Gray code if and only if every coloring of the forest appears exactly once in it and two consecutive colorings differ by the color of exactly one node.

Let us illustrate the algorithm's functioning on the forest (1). The main idea is to interleave the sequences of colorings which correspond to each of the trees that form the forest. Here, one must interlace the sequence of the three colorings of the left-hand tree, namely:

(2) with the sequence of the five colorings of the right-hand tree, given below:

(3) Thus, the first line of Figure 5 exhibits the first coloring of the lefthand tree, combined successively with all colorings of the righthand tree. The second line shows the second coloring of the lefthand tree, again combined with all colorings of the right-hand tree, but this time in reverse order-indeed, it is clear that the mirror image of a Gray code remains a Gray code. Lastly, the third line exhibits the third coloring of the left-hand tree and all colorings of the right-hand tree, this time again in their initial order.

There remains to explain how to enumerate all colorings of a tree. Let the first coloring be uniformly white. Then, to obtain the remainder of the sequence, color the root node black and enumerate all colorings of the forest formed by its children. The sequence thus obtained is indeed a Gray code, because (i) the first and second colorings differ only by the color of the root node and (ii) from then on, the root node remains unaffected, and the sequence of the colorings of the children forms a Gray code by construction. This process is illustrated by ( 2) and (3) above. Note that the coloring where every node is black does not necessarily appear last in a sequence.

Functional Implementation

We consider an Ocaml implementation of Koda-Ruskey's algorithm which makes use of higher-order functions [START_REF] Filliâtre | Producing All Ideals of a Forest, Functionally[END_REF]. First, we introduce the types for trees, forests and colors as follows:

type tree = Node of int × forest and forest = tree list type color = White | Black A tree is thus a term Node(i, f ) where i is the index of its root and f the forest of its subtrees. A forest is simply a list of trees. The current coloring of the considered forest will be materialized in a global array bits, which is assumed to be large enough to contain all indices of the forest.

let rec enum_forest k = function | [] → k () | Node (i, f') :: f → let k () = enum_forest k f in if bits.(i) = White
A nice way to implement Koda-Ruskey's algorithm is to use a continuation-based approach, using a recursive function enum_forest with the following type: enum_forest : (unit → unit) → forest → unit It takes a continuation k and a forest f as arguments. Then it enumerates all colorings of f, applying continuation k once for each different coloring of f.

The code for enum_forest is given in Figure 6 and proceeds as follows. If the forest is empty, we simply call the continuation k. Otherwise, the forest contains at least one tree, say Node (i,f'), next to a sub-forest f. We first build a new continuation k which enumerates the colorings of f, using the old continuation k. Then we consider the tree itself. The function must be able to enumerate the colorings in both directions (as explained in the next section). To determine which, we look up the color of the tree's root, that is bits.(i). If it is currently white, then the whole tree must be white. We have a complete coloring, so we signal the continuation k; then, we color the root black and enumerate its children's colorings using enum_forest. If, on the other hand, the root is currently black, we do the converse. That is, we first use enum_forest to enumerate the children's colorings in reverse order, which leaves all of the children entirely white; then, we color the root white, and signal the continuation k.

Formal Specification

We are now going to give a formal specification to this functional implementation. In particular, we should characterize what is the effect of continuation k. Obviously, it modifies the contents of array bits, since it is precisely used to do so in recursive calls. But k may have other effects, if for instance the initial continuation is used to print the current coloring or to record it in some array 5 . Therefore, we use effect polymorphism to indicate that k may have some effect e, disjoint from bits: enum_forest :

∀e. (unit → {bits e} unit) → forest → {bits e} unit To specify the behavior of enum_forest, we must also exhibit the forest whose colorings are enumerated by the continuation, as an additional argument, say f0. Thus the Who implementation of Koda-Ruskey's algorithm has three parameters, and looks like let rec enum_forest

[e|] (f0 : forest) (k : unit → {bits e} unit) (f : forest) = ... The additional argument f0 is logical, since it only participates to the specification and not to the computation. As we already claimed, Who is intended to be an intermediate language for pro-5 For the purpose of drawing pictures such as the one in Figure 5, enum_forest was even used with a continuation k producing pictures.

1 let rec enum_forest [e] (f0 : forest) (k : unit → {bits e} unit) (f : forest) = 2 { validf (append f f0) ∧ anyf bits (append f f0) ∧ 3 (∀(s : bits e ). validf f0 → anyf bits |s f0 → pre k () s) ∧ 4 (∀(s s': bits e ). post k () s s' () → mirrorf bits |s bits |s' f0 ∧ eq_out bits |s bits |s' f0) } gram verification, where programs do not necessarily need to coincide with the original Ocaml programs.

We now turn to the specification itself. Here, we focus on the behavior of enum_forest with respect to the current coloring, i.e. we characterize the conditions under which the function can be called and its effect on the contents of array bits. We do not prove that the set of all colorings form a Gray code, but this could be deduced without too much effort. The Who code for function enum_forest is given in Figure 7 and its annotations are detailed in the remaining of this section.

The first requirement is a sanity condition over forests f and f0, which says that they do not contain duplicate indices. We write i ∈ t (resp. i ∈ f ) when i is an index occurring in tree t (resp. in forest f ). We also write valid t (resp. valid f ) to characterize a tree t (resp. a forest f ) where all indices are different. These two notions of occurrence and validity are easily defined inductively over trees and forests6 . If append denotes the concatenation of forests, we thus require valid (append f f0) as a precondition (line 2).

The next requirement is a condition over the current coloring, i.e. the state of bits, for enum_forest to execute correctly. Requiring the nodes to be all colored in white is a too strong condition, since recursive calls are going to be used to "decolor" some trees, as in the second row of Figure 5. We must thus characterize the final coloring of a tree or a forest. Obviously, the parity of the number of colorings plays a role. Indeed, in a forest containing two trees, say t1 and t2 in that order, the final coloring of t2 will be all white if t1 admits an even number of colorings, and will be itself a final coloring of t2 otherwise. We introduce the predicates even and odd, over trees and forests, to indicate an even (resp. odd) number of colorings. They are inductively defined as follows: even t even (t::f ) even f even (t::f )

odd f even (Node (i, f )) odd [] odd t odd f odd (t::f ) even f odd (Node (i, f ))
We can now define the notions of initial and final colorings. In the following, s stands for a possible state of array bits, that is an greater clarity. We proceed similarly for other predicates defined on trees and forests. array of colors. The predicate I s f characterizes an initial state s for a given forest f , as being all-white:

I s f def = ∀i, i ∈ f ⇒ s(i) = White
Similarly, the predicate F s t (resp. F s f ) characterizes a final state s for a tree t (resp. a forest f ):

F s t even t I s f F s (t::f )

F s t odd t F s f F s (t::f ) F s [] s(i) = Black F s f F s (Node (i, f
)) The precondition of enum_forest requires each tree of the forest to be either in an initial or final state, which can be defined as follows:

any s [f1; . . . ; fn] def = ∀i, I s fi ∨ F s fi More precisely, the precondition requires that any holds on the concatenated forest append f f0 (line 2). We also require that valid and any are sufficient conditions to ensure the precondition of k (line 3). Finally, the new continuation k which is built in enum_forest is given the same requirement (line 8).

We now turn to the postcondition of enum_forest. Simply speaking, we want to state that it switches the coloring of the forest from initial to final and conversely. As for the precondition, it would be a too strong requirement and we need to characterize the effect of enum_forest more subtly. Again, the parity of the number of colorings is playing a role, since an even number of colorings for the first tree would result in an unchanged coloring for the remaining of the forest and, conversely, an odd number for the first tree would result in a switch for the remaining of the forest. To denote unchanged colorings, we introduce the following predicate over two different states s1 and s2: mirror s1 s2 t even t same s1 s2 f mirror s1 s2 (t :: f ) This is the expected postcondition for enum_forest (line 18), and thus also a requirement over continuation k (lines 4 and 10).

same s1 s2 f def = ∀i, i ∈ f ⇒ s1(i) = s2(i)
As such, the specification of enum_forest is incomplete, as it does not say anything about the colors for the indices which are not in f. Since the state of bits is considered as a whole, these colors could have been changed. But for the correctness proof of enum_forest, it is necessary to know that recursive calls will not modify the color of node i. Thus we need a stronger postcondition, which "frames" the effects on array bits. For that purpose, we introduce the predicate

eqout s1 s2 f def = ∀i, i ∈ f ⇒ s1(i) = s2(i)
and use it in the postcondition of enum_forest (line 18) and k (lines 4 and 10).

Formal Proof

When processed with Who, the code in Figure 7 results in 17 proof obligations. They have been discharged using the Coq proof assistant, with the use of several auxiliary lemmas over predicates even, any, mirror, etc. Completing the proofs of these lemmas is still work in progress, as is the proof that enum_forest indeed realizes a Gray code enumeration. Anyhow, the Who tool already proved very useful in the process of obtained the verification conditions and debugging the specification.

Related Work

The Pangolin system, the implementation of the theoretical system of [START_REF] Régis | A Hoare logic for call-by-value functional programs[END_REF], can also be used to reason about purely functional programs. It cannot deal with side effects. However, Pangolin has been one of the starting points of our work.

Systems for verification of first-order programs like Why (Filliâtre 2003) or Spec# [START_REF] Barnett | The Spec# Programming System: An Overview[END_REF]) are the other starting points of this work. These systems generally deal very well with usual features of first-order programs, for example arrays, use SMT solvers to discharge proof obligations and strive for the best possible automation. We try to improve on this work by adding higherorder features, trying to maintain the degree of automation and ease of use.

Honda, Yoshida and Berger [START_REF] Honda | An observationally complete program logic for imperative higher-order functions[END_REF][START_REF] Berger | A logical analysis of aliasing in imperative higher-order functions[END_REF]) present a logic for imperative higher-order programs, first without, then with aliasing, but without allocation. They obtain strong theoretical results (e.g. a completeness result of their program logic). However, they describe the system in Hoare logic style with many non-structural rules, which seems to render it difficult to implement. The Who implementation has been straightforwardly derived from the syntax-directed formulation of a weakestpreconditions calculus.

The Ynot System [START_REF] Nanevski | Ynot: Reasoning with the awkward squad[END_REF]) is an extension to the Coq proof assistant, capable of reasoning about imperative higherorder programs, including effectful functions as arguments, using a monad in which effectful computations can take place. Ynot is strictly more expressive than our system and features modular reasoning (abstracting over the specification and effect of a function as argument) while being able to reason about aliasing situations thanks to separation logic. We believe however, that one can obtain much simpler proof obligations, without separation logic, in the case of alias-free programs. We leave the work of substantiating this claim for future work.

Another line of work consists in giving a translation from an imperative to a functional language, with the aim of applying one of the techniques for purely functional programs to the translation. O'Hearn and Reynolds (O'Hearn and Reynolds 2000) present a translation from Algol with first-class references and dynamic allocation to a linear λ-calculus. They impose an alias-avoiding restriction which is similar to ours, by the notion of syntactic interference. It is not clear to us how this restriction compares to ours. [START_REF] Charguéraud | Functional translation of a calculus of capabilities[END_REF] give a translation from Core ML with first-class references, dynamic allocation and aliasing to a functional language, using a very expressive type system with linear capabilities. Both systems have not yet been connected to a program logic, so it is unclear what kind of proof obligations one would obtain. Although we use a simpler programming language than Charguéraud and Pottier, we present a complete cycle from imperative programs to proof obligations.

Future Work

The current prototype implementation is still very limited. We plan to extend it in several ways. First, we intend to add creation of reference cells to the language. Using now-standard techniques of alias tracking this can be done in a straightforward way. Second, an important feature of functional languages are algebraic datatypes. We plan to add them natively to the language. This will result in programs much simpler to write and understand, and can also be exploited to obtain simpler proof obligations.

All the proofs presented in this paper have been done manually, using the Coq proof assistant (The [START_REF] Coq | The Coq Proof Assistant Reference Manual -Version V8.1[END_REF]. With the exception of the proof obligations for the Koda-Ruskey algorithm, all proofs are actually very simple and, after some structural reasoning, can be discharged by built-in automatic tactics (in particular the omega tactic for arithmetic reasoning) . This fact, along with the experience of the Pangolin system, makes us think that the resulting proof obligations are suited for SMT provers [START_REF] Ranise | The Satisfiability Modulo Theories Library (SMT-LIB)[END_REF], which would avoid manual proofs in many cases. We are currently investigating the possibility to use SMT provers, using an encoding of higher-order logic into first-order logic.

Effectful computations with aliasing, mutable data structures and sharing is currently out of the scope of Who. We plan to build a more sophisticated analysis on top of the presented tool. A suitable memory model along with a translation, guided by this model, to the Who language, could deal with these difficult issues independently of considerations of a weakest precondition calculus.

Conclusion

We have presented Who, a tool to specify and prove effectful higher-order functions, as they occur very often in language mixing functional and imperative features. We have demonstrated its usefulness on several small and one more complex example. The current limitations are either subject to (relatively straightforward) future work, like algebraic datatypes and even the treatment of local allocation, or motivated by its status as an intermediate language, target of a tool applying a more sophisticated aliasing analysis.

6 ∀Figure 3 .

 63 Figure 3. Annotated code for Array.iter.

Figure 4 .

 4 Figure 4. The succession of states during the execution of Array.iter.

  s : ar sum ) (k:int) → sum |s = sum_array k ar |s }} (fun (z : int) →

Figure 5 .

 5 Figure 5. Koda and Ruskey's algorithm applied to the forest (1).

Figure 6 .

 6 Figure 6. An Ocaml implementation of Koda-Ruskey's algorithm.

Figure 7 .

 7 Figure 7. Who implementation of Koda-Ruskey's algorithm.

  Then we can define the effect of enum_forest between pre-state s1 and post-state s2, as the following, inductively defined predicate

	mirror:	I s1 t F s2 t	F s1 t I s2 t
		mirror s1 s2 t	mirror s1 s2 t
		mirror s1 s2 []
		mirror s1 s2 t odd t mirror s1 s2 f
		mirror s1 s2 (

t :: f )

Who is freely distributed at http://www.lri.fr/~kanig/files/ who-0.1.tgz.

We only consider partial correctness in this paper. Total correctness requires termination proofs as well.

3 Most of the code in this paper is taken from the Ocaml standard library and has been only slightly changed.

Array.iter in the Ocaml standard library.

In the Coq files, we distinguish validt for trees and validf for forests, since there is no overloading; in this paper, we simply write valid for

Acknowledgments

We would like to thank the anonymous referees for their helpful comments.