First Pass

The previous chapter (Basic) covered simple programs that manipulate individual mutable cells. This chapter focuses on the specification and verification of programs manipulating mutable data structures like lists and trees. In Separation Logic, such data structures are specified using representation predicates. A representation predicate is a heap predicate that describes a mutable data structure. For example, the heap predicate MList L p describes a mutable linked list whose head cell is at location p and whose elements are described by the Coq list L. In this chapter, we will see how to define MList and how to use this predicate for specifying and verifying functions that operate on mutable linked lists. We will also study representation predicates for mutable trees, as well as for counter functions, which feature an internal state. As explained in the Preface, this chapter, like all the following ones, is structured in three parts:

• The First Pass section presents the most important ideas only.
• The More Details section presents additional material explaining in more depth the meaning and the consequences of the key results. By default, readers would eventually read all this material.
• The Optional Material section contains more advanced material, for readers who can afford to invest more time in the topic.

While going through proofs, we will introduce a few additional tactics.

• xpull to extract pure facts and quantifiers from the LHS of ==>.
• xchange E for exploiting a lemma E with a conclusion of the form H₁ ==> H₂ or H₁ = H₂.
• xchange <- E for exploiting an entailment H₂ ==> H₁ in the case E is a lemma with a conclusion of the form H₁ = H₂.
• xchanges is a shorthand for xchange followed with xsimpl.
• xfun to reason about function definitions.
• xtriple to establish specifications for abstract functions.
• introv (a TLC tactic) like intros but takes as arguments only the name of the hypotheses, not of all variables.
• rew_list (a TLC tactic) to normalize list expressions.

Furthermore, TLC tactics and most x-tactics may be followed with a star symbol to invoke eauto. For example, xsimpl* is a shorthand for xsimpl; eauto. The star symbol is used to make proof scripts more concise, yet exercises can all be solved without this feature.

The List Representation Predicate

The implementation of mutable lists and trees involves the use of records. For simplicity, field names are represented as natural numbers. For example, to represent a list cell with a head and a tail field, we define head as the constant zero, and tail as the constant one.

The heap predicate p ~~~>`{ head := x; tail := q } describes a record allocated at location p, with a head field storing x and a tail field storing q. The arrow ~~~> is provided by the framework for describing records. The notation `{...} is a handy notation for a list of pairs of field names and values of arbitrary types. (Further details on the formalization of records are presented in chapter Records.) A mutable list consists of a chain of cells. Each cell stores a tail pointer that gives the location of the next cell in the chain. The last cell stores the null value in its tail field. The heap predicate MList L p describes a list whose head cell is at location p and whose elements are described by the list L. This predicate is defined recursively on the structure of L.

• If L is empty, then p is the null pointer.
• If L is of the form x::L', then p is not null, the head field of p contains x, and the tail field of p contains a pointer q such that MList L' q describes the tail of the list.

This definition is formalized as follows.

Alternative Characterizations of MList

Carrying out proofs directly with MList can be slightly cumbersome, mainly due to Coq's limited support for re-folding definitions. We find it more practical to explicitly state equalities that paraphrase the definition of MList. There is one equality for the nil case and one for the cons case.

In addition, it is also very useful in proofs to reformulate the definition of MList L p in the form of a case analysis on whether the pointer p is null or not. This corresponds to the programming pattern if p == null then ... else .... This alternative characterization of MList L p asserts the following.

• If p is null, then L is empty.
• Otherwise, L decomposes as x::L', the head field of p contains x, and the tail field of p contains a pointer q such that MList L' q describes the tail of the list.

The corresponding lemma, shown below, is stated using the If P then X else Y construction, which generalizes Coq's construction if b then X else Y to discriminate over a proposition P as opposed to a boolean value b. The If construct leverages classical logic; it is provided by the TLC library. The tactic case_if is convenient for performing the case analysis on whether P is true or false.

The proof is a bit technical: it may be skipped on a first reading.

Note that the reciprocal entailment to the one stated in MList_if is also true, but we do not need it so we do not bother proving it here. In the rest of the course, we will never unfold the definition MList, but only work with MList_nil, MList_cons, and MList_if. We therefore make the definition of MList opaque to prevent Coq from performing undesired simplifications.

In-place Concatenation of Two Mutable Lists

The function append expects two arguments: a pointer p₁ to a nonempty list, and a pointer p₂ to another list, possibly empty. The function updates the last cell from the first list in such a way that its tail points to the head cell of p₂. After this operation, the pointer p₁ points to a list that corresponds to the concatenation of the two input lists.     let rec append p₁ p₂ =
      if p₁.tail == null
        then p₁.tail <- p₂
        else append p₁.tail p₂

The append function is specified and verified as shown below. The proof pattern is representative of that of many list-manipulating functions, so it is essential that you take the time to play through every step of this proof. Several exercises will require a very similar proof pattern.

The TLC tactic introv is very convenient for providing explicit names for hypotheses without having to provide names for the variables already named in the lemma statement.

The induction principle provides a hypothesis for the tail of L₁. The predicate list_sub L₁' L₁ asserts that L₁ decomposes as x::L₁' for some x.

To begin the proof, we reveal the head cell of p₁, exploiting the assumption that p₁ ≠ null.

Using xpull, we extract the existentially quantified variables: we let q₁ denote the tail of p₁, x the head element of L₁, and L₁' the tail of L₁.

The tactic intros → is a shorthand for intros E; rewrite E; clear E.

We then reason about the if statement.

If q₁ is null, then L₁' is empty.

In this case, we reason about the assignment, then we fold back the head cell. To that end, we exploit the tactic xchange <- MList_cons, which is similar to xchange MList_cons but exploits the equality asserted by MList_cons in the reverse direction.

Above, the tactic xchange discharges the goal because the LHS, after the operation, matches the RHS. To see the details, change the line of script to: xapp. eapply himpl_trans. xchange <- MList_cons. apply himpl_refl.

Otherwise, if q₁ is not null, we reason about the recursive call using the induction hypothesis; then we re-fold the head cell.

Smart Constructors for Linked Lists

We next introduce two smart constructors for linked lists, called mnil and mcons. The operation mnil() creates an empty list. Its implementation simply returns the value null. Its specification asserts that the return value is a pointer p such that MList nil p. In the specification below, recall that funloc p ⇒ H is a notation for fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* H.

Note: in theory, we could present mnil as a constant rather than as a function that takes unit as argument. However, viewing it as a function like all the other example programs helps keep the framework minimal.

We are requested to prove that, under the empty precondition, the value null satisfies the postcondition fun (r:val) ⇒ \∃ (p:loc), \[r = val_loc p] \* (MList nil p). As the tactic xval shows, this is equivalent to proving that the precondition \[] entails ∃ p, \[null = val_loc p] \* (MList nil p)).

To conclude the proof, it suffices to instantiate p with null, and to argue that MList nil null can created out of thin air. This is indeed true because MList nil null is equivalent to \[]. The first step is to obtain an explicit statement of this equivalence, in the form of an hypothesis named E. By instantiating the lemma MList_nil, which asserts that ∀ p, MList nil p = \[p = null], we obtain the equality MList nil null = \[null = null].

Then, we invoke xchange <- E. In exchange for proving null = null, this tactic replaces the empty heap predicate \[] with MList nil null.

At this stage, the tactic xsimpl is able to automatically instantiate p with null, and auto checks that null = null.

The proof above can be greatly shortened by using the tactic xchanges, which is a shorthand for xchange <- E followed by xsimpl. In fact, we even use xchanges* <- E, to invoke xchanges <- E followed by eauto.

Observe that the specification triple_mnil does not mention the null pointer anywhere. Hence, this specification abstracts away from the implementation details of how mutable lists are represented internally. The operation mcons x q creates a fresh list cell, with x in the head field and q in the tail. Its implementation allocates and initializes a fresh record made of two fields. The allocation operation leverages the allocation construct written `{ head := 'x; tail := 'q } in the code. This construct is in fact a notation for a primitive operation called val_new_hrecord_2. The details of record constructions are explained in the chapter Record. There is no need to understand the details at this stage.

The operation mcons admits two specifications. The first one says that it produces a record described with a record heap predicate.

To prove this lemma, we need to know that the record allocation operation is in fact a notation for a call to val_new_hrecord_2, hence we need to invoke a library lemma called triple_new_hrecord_2 for reasoning about this call. (Don't worry: this proof pattern will not appear in exercises!)

The second specification asserts that mcons can be used to extend a mutable list. It assumes that the argument q comes with a list representation of the form Mlist q L, and it specifies that the function mcons produces the representation predicate Mlist p (x::L). This second specification is derivable from the first one, by folding the representation predicate MList using the tactic xchange.

In practice, this second specification is more often useful than the first one, hence we register it in the database for xapp. It remains possible to invoke xapp triple_mcons to exploit the first specification, where needed.

In what follows, we consider several classic operations on mutable lists, each illustrating an idiomatic proof pattern.

Copy Function for Lists

The function mcopy takes a mutable linked list and builds an independent copy of it, with the help of the functions mnil and mcons.     let rec mcopy p =
      if p == null
        then mnil ()
        else mcons (p.head) (mcopy p.tail)

The precondition of mcopy requires a linked list described as MList L p. The postcondition asserts that the function returns a pointer p' and a list described as MList L p', in addition to the original list MList L p. The two lists are totally disjoint and independent, as captured by the separating conjunction symbol (the star).

The proof structure is like the previous ones. While playing the script, try to spot the places where - mnil produces an empty list of the form MList nil p', - the recursive call produces a list of the form MList L' q', and - mcons produces a list of the form MList (x::L') p'.

Note that C is actually val_loc p = val_loc null, and not simply p = null. This explains why a call to subst does nothing. If needed, use the TLC tactic, inverts C or invert C to exploit the equality. In this specific proof, though, we don't need that.

A Coq expert would typically write the same proof script in a more compact fashion, as follows. Recall that the token → can be provided instead of a fresh name to indicate on-the-fly substitution, and that the star token after a tactic indicates a call to eauto.

Length Function for Lists

The function mlength computes the length of a mutable linked list.     let rec mlength p =
      if p == null
        then 0
        else 1 + mlength p.tail

Exercise: 3 stars, standard, especially useful (triple_mlength)

Prove the correctness of the function mlength. Hint: use the tactic rew_list to normalize list expressions -- in particular, to prove length L' + 1 = length (x :: L').

Alternative Length Function for Lists

In this section, we consider an alternative implementation of mlength that uses an auxiliary reference cell to keep track of the number of cells traversed so far. The list is traversed recursively, incrementing the contents of the reference once for every cell.     let rec listacc c p =
      if p == null
        then ()
        else (incr c; listacc c p.tail)

    let mlength' p =
      let c = ref 0 in
      listacc c p;
      !c

(Recall that get_and_free was defined in chapter Basic.

Exercise: 3 stars, standard, especially useful (triple_mlength')

Prove the correctness of the function mlength'. Hint: start by stating a lemma triple_acclength expressing the specification of the recursive function acclength. Make sure to generalize the appropriate variables before applying the well-founded induction tactic. Then complete the proof of the specification triple_mlength', using xapp triple_acclength to reason about the call to the auxiliary function. Recall that rew_list can be used to simplify length (x :: L') into length L' + 1 and that math can be used to prove arithmetic equalities such as (n + 1) + m = n + (m + 1).

Free Function for Lists

The operation mfree deallocates all the cells in a given list. Each cell consists of a record that can be deallocated using the primitive operation delete. The deallocation of a list is implemented by recursively traversing the list, invoking delete on each cell after reading its tail pointer.     let rec mfree p =
      if p != null then begin
        let q = p.tail in
        delete p;
        mfree q
      end

The precondition of mfree requires a full list MList L p. The postcondition is empty: the entire list is destroyed.

Exercise: 3 stars, standard, especially useful (Triple_mfree)

Verify the function mfree.

In-Place Reversal Function for Lists

The function mrev takes as argument a pointer to a mutable list, and returns a pointer on the reverse list, that is, a list with elements in the reverse order. The cells from the input list are reused for constructing the output list: the operation is said to be "in place".     let rec mrev_aux p₁ p₂ =
      if p₂ == null
        then p₁
        else (let p₃ = p₂.tail in
              p₂.tail <- p₁;
              mrev_aux p₂ p₃)

    let mrev p =
      mrev_aux null p

Exercise: 4 stars, standard, optional (triple_mrev)

Prove the correctness of the functions mrev_aux and mrev. Hint: here again, start by stating a lemma triple_mrev_aux expressing the specification of the recursive function mrev_aux. Make sure to generalize the appropriate variables before applying the well-founded induction tactic. Then complete the proof of triple_mrev, using xapp triple_mrev_aux. Hint: in triple_mrev, you will need to create an empty list out of thin air, using xchange <- (MList_nil null). Also, make sure to call rew_list before xsimpl; otherwise xsimpl might not guess the right existential variable. The syntax xsimpl v is also available if you want to specify the witness x inside a goal of the form H₁ ==> (\∃ x, H₂).

More Details

The rest of this chapter presents the formal verification of more advanced data structures and algorithms. The remaining chapters in the book explain how to construct the program verification framework that we have been using so far. The two aspects are completely orthogonal. Thus, if you have time and are interested in the practical aspects of program verification, you should complete the present chapter before moving on. On the other hand, if you are eager to dive into the construction of Separation Logic, then you may safely move on to the next chapter and come back to this later.

A Stack Represented as a List and a Size

In this section, we consider the implementation of a mutable stack featuring a constant-time access to the size of the stack. This stack structure consists of a 2-field record storing a pointer to a mutable linked list plus an integer recording the length of that list. The implementation includes a function create to allocate an empty stack, a function sizeof for reading the size, and functions push, top, and pop for manipulating the top of the stack.     type 'a stack = {
      data : 'a list;
      size : int }

    let create () =
      { data = null;
        size = 0 }

    let sizeof s =
      s.size

    let push p x =
      s.data <- mcons x s.data;
      s.size <- s.size + 1

    let top s =
      let p = s.data in
      p.head

    let pop s =
      let p = s.data in
      let x = p.head in
      let q = p.tail in
      delete p;
      s.data <- q in
      s.size <- s.size - 1;
      x The constants data and size are introduced as identifiers for the record fields of the type 'a stack.

The representation predicate for the stack takes the form Stack L s, where s denotes the location of the record describing the stack and L denotes the list of items stored in the stack. The underlying mutable list is described as MList L p, where p is the location p stored in the first field of the record. The definition of Stack is as follows.

Observe that the predicate Stack does not expose the location of the mutable list; this location is existentially quantified in the definition. It also does not expose the size of the stack, as this value can be obtained from length L. Let's start with the specification and verification of create and sizeof.

The sizeof operation returns the contents of the size field of a stack.

The push operation extends the head of the list and increments the size field.

Exercise: 3 stars, standard, especially useful (triple_push)

Prove the following specification for the push operation.

The pop operation extracts the element at the head of the list, updates the data field to the tail of the list and decrements the size field.

Exercise: 4 stars, standard, especially useful (triple_pop)

Prove the following specification for the pop operation. Hint: You'll need to unfold the definition of Stack as in the proofs above, and at some point you'll want to destruct L.

The top operation extracts the element at the head of the list.

Exercise: 2 stars, standard, optional (triple_top)

Prove the following specification for the top operation.

Formalization of the Tree Representation Predicate MTree

In this section, we generalize the ideas presented for linked lists to binary trees that store integer values in their nodes. Just as mutable lists are specified with respect to Coq's purely functional lists, mutable binary trees are specified with respect to Coq trees. Consider the following inductive definition of the type tree. A leaf is represented by the constructor Leaf, and a node takes the form Node n T₁ T₂, where n is an integer and T₁ and T₂ are its two subtrees.

In a program manipulating a mutable tree, an empty tree is represented using the null pointer, and a node is represented in memory using a three-cell record. The first field, "item", stores an integer. The other two fields, "left" and "right", store pointers to the left and right subtrees, respectively.

The heap predicate p ~~~>`{ item := n; left := p₁; right := p₂ } describes a record allocated at location p, storing the integer n and the two pointers p₁ and p₂. The representation predicate MTree T p, of type hprop, asserts that the mutable tree structure with root at location p describes the logical tree T. The predicate is defined recursively on the structure of T.

• If T is a Leaf, then p is the null pointer.
• If T is a node Node n T₁ T₂, then p is not null and at location p one finds a record with field contents n, p₁ and p₂, with MTree T₁ p₁ and MTree T₂ p₂ describing the two subtrees.

Alternative Characterization of MTree

As for MList, it is very useful for proofs to state three lemmas that paraphrase the definition of MTree. The first two lemmas correspond to the folding/unfolding rules for leaves and nodes.

The third lemma reformulates MTree T p using a case analysis on whether p is the null pointer. This formulation matches the case analysis typically performed in the code of functions that operates on trees.

Beyond this point, the definition of Mtree not longer needs to be unfolded: we make it opaque.

Additional Tooling for MTree

For reasoning about recursive functions over trees, it is useful to exploit the well-founded order associated with "immediate subtrees". Concretely, tree_sub T₁ T asserts that the tree T₁ is either the left or the right subtree of the tree T. This order may be exploited for verifying recursive functions over trees using the tactic induction_wf IH: tree_sub T. The relation tree_sub is defined as follows.

For allocating fresh tree nodes as a 3-field record, we introduce the operation mnode n p₁ p₂, defined and specified as follows.

A first specification of mnode describes the allocation of a record.

A second specification, derived from the first, asserts that, when provided two subtrees T₁ and T₂ at locations p₁ and p₂, the operation mnode n p₁ p₂ builds, at a fresh location p, a tree described by Mtree [Node n T₁ T₂] p. Compared with the first specification, this second specification is said to "transfer ownership" of the two subtrees.

Exercise: 2 stars, standard, optional (triple_mnode')

Prove the specification triple_mnode' for node allocation. Because this specification refines the previous specification triple_mnode, the proof should begin with xapp triple_mnode.

Similarly to what we had done for mnil, we could implement a function mleaf that returns the null pointer and derive a specification for it in terms of MTree. Instead, we will see through the next examples how one may directly reason about occurrences of null appearing in tree- manipulating code, using xchange <- (MTree_Leaf null) directly.

Deep-Copy of a Tree

The operation tree_copy takes as argument a pointer p on a mutable tree and returns a fresh copy of that tree. It is defined in a similar way to the function mcopy for lists.     let rec tree_copy p =
      if p = null
        then null
        else mnode p.item (tree_copy p.left) (tree_copy p.right)

Exercise: 3 stars, standard, especially useful (triple_tree_copy)

Prove the specification of tree_copy. Hint: you'll need to use xchange <- (MTree_Leaf null) twice.

Computing the Sum of the Items in a Tree

The operation mtreesum takes as argument the location p of a mutable tree, and it returns the sum of all the integers stored in the nodes of that tree. The implementation traverses the tree, using an auxiliary reference cell to maintain the sum of all the items visited so far.     let rec treeacc c p =
      if p ≠ null then (
        c := !c + p.item;
        treeacc c p.left;
        treeacc c p.right)

    let mtreesum p =
      let c = ref 0 in
      treeacc c p;
      !c

The specification of mtreesum is expressed in terms of the Coq function treesum, which computes the sum of the node items stored in a logical tree. This operation is defined by recursion over the tree.

Exercise: 4 stars, standard, optional (triple_mtreesum)

Prove the correctness of the function mtreesum. Hint: to begin with, state and prove the specification lemma triple_treeacc.

Verification of a Counter Function with Local State

This section is concerned with the verification of counter functions, which feature internal, mutable state. A counter function f is a function that, each time it is called, returns the next integer. Concretely, the first call to f() returns 1, the second call returns 2, the third returns 3, and so on. A counter function can be implemented using a reference cell, p, that stores the integer last returned by the counter. Initially, the contents of the cell is zero. Each time the counter function is called, the contents is increased by one unit, and the new value of the contents is returned to the caller. The function create_counter produces a fresh counter function. Concretely, create_counter() returns a counter function f that is independent from any other previously existing counter function.     let create_counter () =
       let p = ref 0 in
       (fun () → (incr p; !p))

In this section, we present two specifications for counter functions. The first specification is the most direct, but it exposes the existence of the reference cell, revealing implementation details about the counter function. The second specification is more abstract, hiding from the client the internal representation of the counter using an abstract representation predicate. Let us begin with the simple, direct specification. The proposition CounterSpec f p asserts that f is a counter function f whose internal state is stored in a reference cell at location p. Thus, invoking f in a state p ~~> m updates the state to p ~~> (m+1) and produces the output value m+1.

The function create_counter creates a fresh counter. Its precondition is empty. Its postcondition asserts that the function f being returned satisfies CounterSpec f p and the output state contains a cell p ~~> 0 for some existentially quantified location p.

Observe how the postcondition that appears in the triple above refers to CounterSpec, which itself involves a triple. In other words, a triple appears nested inside another triple. In technical terms, we are leveraging the "impredicativity of triples", which holds as a consequence of the "impredicativity of predicates" in the logic of Coq. The proof involves the use of a new tactic, called xfun, for reasoning about local function definitions. Here, xfun gives us the hypothesis Hf that specifies the code of f. This hypothesis is of the form: ∀ v H' Q', (PRE H' CODE B POST Q') → triple (f v) H' Q', where B denotes the code of the body of the function f instantiated on the argument v, and where H' and Q' denote arbitrary pre- and postconditions. Exploiting this assumption enables the user to subsequently derive triples about the local function f, by reasoning about the code of the f, just in the same way as when the user invokes xwp for reasoning about a top-level function.

Let us move on to the presentation of more abstract specifications. Their purpose is to hide from the client the existence of the reference cell used to represent the internal state of the counter functions. To that end, we introduce the heap predicate IsCounter f n, which relates a function f, its current value n, and the piece of memory state involved in the implementation of this function. This piece of memory is of the form p ~~> n, for some location p, such that CounterSpec f p holds.

Using IsCounter, we can reformulate the specification of create_counter with a postcondition asserting that the output function f is described by the heap predicate IsCounter f 0.

This lemma is the same as triple_create_counter, except that the reference cell p is no longer explicitly mentioned in the postcondition. In other words, the address of the reference cell p used internally by the counter becomes hidden from the user.

Next, we reformulate the specification of a call to a counter function. A call to f(), in a state satisfying IsCounter f n, produces a state satisfying IsCounter f (n+1), and returns n+1.

Exercise: 4 stars, standard, especially useful (triple_apply_counter_abstract)

Prove the abstract specification for a counter function. You will need to begin the proof using the tactic xtriple, for turning goal into a form on which other x-tactics can be invoked. Then, use xpull to extract facts from the precondition.

Finally, let us illustrate how a client might work with counter functions.     let test_counter () =
       let c₁ = create_counter () in
       let c₂ = create_counter () in
       let n₁ = c₁() in
       let n₂ = c₂() in
       let n₃ = c₁() in
       n₂ + n₃

Exercise: 2 stars, standard, optional (triple_test_counter)

Prove the example function manipulating abstract counters. In the specification below, the heap predicate \∃ H, H corresponds to the two counters, which we currently have no way of deallocating. The necessary mechanism for garbage collection will be introduced later in chapter Affine. Hint: use xapp triple_create_counter_abstract and xapp triple_apply_counter_abstract to invoke the specifications.

Optional Material

The verification of higher-order functions, and of their interaction with mutable state, was a formidable challenge prior to the introduction of Separation Logic. The rest of this chapter illustrates how to reason about imperative, higher-order programs.

Specification of a Higher-Order Repeat Operator

Consider the higher-order iterator repeat: a call to repeat f n executes n times the call f().     let rec repeat f n =
      if n > 0 then (f(); repeat f (n-1))

For simplicity, let us assume for now n ≥ 0. The specification of repeat n f can be expressed in terms of an invariant, named I, describing the state in between every two calls to f. We assume that the initial state satisfies I 0. Moreover, we assume that, for every index i in the range from 0 (inclusive) to n (exclusive), a call f() can execute in a state that satisfies I i and produce a state that satisfies I (i+1). The specification below asserts that, under these two assumptions, after the n calls to f(), the final state satisfies I n. The specification takes the form:
      n ≥ 0 →
      Hypothesis_on_f →
      triple (repeat f n)
        (I 0)
        (fun u ⇒ I n) where Hypothesis_on_f is a proposition that captures the following specification:
      ∀ i,
      0 ≤ i < n →
      triple (f ())
        (I i)
        (fun u ⇒ I (i+1)) The complete specification of repeat n f is thus as shown below.

To establish this specification, we carry out a proof by induction over a generalized specification, covering the case where there remains m iterations to perform, for any value of m between 0 and n inclusive.
      ∀ m, 0 ≤ m ≤ n →
      triple (repeat f m)
        (I (n-m))
        (fun u ⇒ I n)) We use the TLC tactics cuts, a variant of cut, to state show that the generalized specification entails the statement of triple_repeat.

We then carry a proof by induction: during the execution, the value of m decreases step by step down to 0.

We reason about the call to f

We next reason about the recursive call.

We need to exploit an arithmetic equality. We do so using math_rewrite, which is a convenient TLC tactic to assert an equality proved by the math tactic, then immediately invoke rewrite with this equality.

Finally, when m reaches zero, we check that we obtain I n.

Specification of an Iterator on Mutable Lists

The operation miter takes as argument a function f and a pointer p on a mutable list and invokes f on each of the items stored in that list.     let rec miter f p =
      if p ≠ null then (f p.head; miter f p.tail)

The specification of miter follows the same structure as that of the function repeat from the previous section, with two main differences. The first difference is that the invariant is expressed not in terms of an index i ranging from 0 to n, but in terms of a prefix of the list L being traversed. This prefix ranges from nil to the full list L. The second difference is that the operation miter f p requires in its precondition, in addition to I nil, the description of the mutable list MList L p. This predicate is returned in the postcondition, unchanged, reflecting the fact that the iteration process does not alter the contents of the list.

Exercise: 5 stars, standard, especially useful (triple_miter)

Prove the correctness of triple_miter.

For exploiting the specification triple_miter to reason about a call to miter, it is necessary to provide an invariant I of type list val → hprop, that is, of the form fun (K:list val) ⇒ .... This invariant, which generally cannot be inferred automatically, should describe the state at the point where the iteration has traversed a prefix K of the list L. Concretely, for reasoning about a call to miter, one should exploit the tactic xapp (triple_miter (fun K ⇒ ...)). An example appears next.

Computing the Length of a Mutable List using an Iterator

The function mlength_using_miter computes the length of a mutable list by iterating over that list a function that increments a reference cell once for every item.     let mlength_using_miter p =
      let c = ref 0 in
      miter (fun x → incr c) p;
      !c

Exercise: 4 stars, standard, especially useful (triple_mlength_using_miter)

Prove the correctness of mlength_using_iter. Hint: as explained earlier, use xfun; intros f Hf for reasoning about the function definition, then use xapp for reasoning about a call to f. Use of xlet is optional.

Factorial Function in Continuation-Passing Style

This section and the next one present examples of functions involving "continuations". As a warm-up, we first consider consider a function that does not involve any mutable state. The function cps_facto_aux n k performs a call to the function k on the value facto n. The function cps_facto n computes the value of facto n by applying cps_facto_aux to the identity function.     let rec cps_facto_aux n k =
      if n ≤ 1
        then k 1
        else cps_facto_aux (n-1) (fun r → k (n * r))

    let cps_facto n =
      cps_facto_aux n (fun r → r)