Lists, verified

Now let's see what's needed to fully verify linked-list operations.

The basic definitions collected in the file lists/headers.verif.h are pretty much the same as for the testing version of lists. The only difference is that, as before, we need to define slightly different functions for allocating and deallocating linked list cells.

Append

The specification of append is identical to the testing version:

exercises/list/append.h

/*@
function [rec] (datatype List) Append(datatype List L1, datatype List L2) {
  match L1 {
    Nil {} => {
      L2
    }
    Cons {Head : H, Tail : T}  => {
      Cons {Head: H, Tail: Append(T, L2)}
    }
  }
}
@*/

And here is the verified code for a simple destructive implementation of append. Note the two uses of the unfold annotation in the body, which are needed to help the CN typechecker. This annotation is an instruction to CN to replace a call to a recursive (CN) function (in this case append) with its definition, and is necessary because CN is unable to automatically determine when and where to expand recursive definitions on its own.

exercises/list/append.verif.c

#include "./headers.verif.h"
#include "./append.h"

struct sllist* IntList_append(struct sllist* xs, struct sllist* ys)
/*@ requires take L1 = SLList_At(xs);
             take L2 = SLList_At(ys); 
    ensures take L3 = SLList_At(return);
            L3 == Append(L1, L2); @*/
{
  if (xs == 0) {
    /*@ unfold Append(L1, L2); @*/
    return ys;
  } else {
    /*@ unfold Append(L1, L2); @*/
    struct sllist *new_tail = IntList_append(xs->tail, ys);
    xs->tail = new_tail;
    return xs;
  }
}

List copy

The verified version of the list copy function is identical to the testing version. No additional annotations are needed.

Merge sort

Finally, here is in-place mergesort, with all necessary unfold annotations so that it is accepted by the CN verifier.

solutions/list/mergesort.verif.c

#include "./headers.verif.h"

/*@
function [rec] ({datatype List fst, datatype List snd})
                 Split_list (datatype List xs)
{
  match xs {
    Nil {} => {
      {fst: Nil{}, snd: Nil{}}
    }
    Cons {Head: h1, Tail: Nil{}} => {
      {fst: Nil{}, snd: xs}
    }
    Cons {Head: h1, Tail: Cons {Head : h2, Tail : tl2 }} => {
      let P = Split_list(tl2);
      {fst: Cons { Head: h1, Tail: P.fst},
       snd: Cons { Head: h2, Tail: P.snd}}
    }
  }
}

function [rec] (datatype List) merge(datatype List xs, datatype List ys) {
  match xs {
      Nil {} => { ys }
      Cons {Head: x, Tail: xs1} => {
        match ys {
          Nil {} => { xs }
          Cons{ Head: y, Tail: ys1} => {
            (x < y) ?
              (Cons{ Head: x, Tail: merge(xs1, ys) })
            : (Cons{ Head: y, Tail: merge(xs, ys1) })
          }
        }
      }
  }
}

function [rec] (datatype List) merge_sort(datatype List xs) {
  match xs {
      Nil{} => { xs }
      Cons{Head: x, Tail: Nil{}} => { xs }
      Cons{Head: x, Tail: Cons{Head: y, Tail: zs}} => {
        let P = Split_list(xs);
        let L1 = merge_sort(P.fst);
        let L2 = merge_sort(P.snd);
        merge(L1, L2)
      }
    }
}
@*/

struct sllist_pair {
  struct sllist* fst;
  struct sllist* snd;
};

struct sllist_pair split_list(struct sllist *xs)
/*@ requires take Xs = SLList_At(xs);
    ensures take Ys = SLList_At(return.fst);
            take Zs = SLList_At(return.snd);
            {fst: Ys, snd: Zs} == Split_list(Xs); @*/
{
  if (xs == 0) {
    /*@ unfold Split_list(Xs); @*/
    struct sllist_pair r = {.fst = 0, .snd = 0};
    return r;
  } else {
    struct sllist *cdr = xs -> tail;
    if (cdr == 0) {
      /*@ unfold Split_list(Xs); @*/
      struct sllist_pair r = {.fst = 0, .snd = xs};
      return r;
    } else {
      /*@ unfold Split_list(Xs); @*/
      struct sllist_pair p = split_list(cdr->tail);
      xs->tail = p.fst;
      cdr->tail = p.snd;
      struct sllist_pair r = {.fst = xs, .snd = cdr};
      return r;
    }
  }
}

struct sllist* merge(struct sllist *xs, struct sllist *ys)
/*@ requires take Xs = SLList_At(xs);
             take Ys = SLList_At(ys);
    ensures take Zs = SLList_At(return);
            Zs == merge(Xs, Ys); @*/
{
  if (xs == 0) {
    /*@ unfold merge(Xs, Ys); @*/
    return ys;
  } else {
    /*@ unfold merge(Xs, Ys); @*/
    if (ys == 0) {
      /*@ unfold merge(Xs, Ys); @*/
      return xs;
    } else {
      /*@ unfold merge(Xs, Ys); @*/
      if (xs->head < ys->head) {
        struct sllist *zs = merge(xs->tail, ys);
        xs->tail = zs;
        return xs;
      } else {
        struct sllist *zs = merge(xs, ys->tail);
        ys->tail = zs;
        return ys;
      }
    }
  }
}

struct sllist* merge_sort(struct sllist *xs)
/*@ requires take Xs = SLList_At(xs);
    ensures take Ys = SLList_At(return);
            Ys == merge_sort(Xs); @*/
{
  if (xs == 0) {
    /*@ unfold merge_sort(Xs); @*/
    return xs;
  } else {
    struct sllist *tail = xs->tail;
    if (tail == 0) {
      /*@ unfold merge_sort(Xs); @*/
      return xs;
    } else {
      /*@ unfold merge_sort(Xs); @*/
      struct sllist_pair p = split_list(xs);
      p.fst = merge_sort(p.fst);
      p.snd = merge_sort(p.snd);
      return merge(p.fst, p.snd);
    }
  }
}

Exercises

Exercise. Fill in the CN annotations on the IntList_append2 function below. (You will need some in the body as well as at the top.)

exercises/list/append2.c

#include "./headers.verif.h"
#include "./append.h"

struct sllist* IntList_copy (struct sllist *xs)
/*@ requires take Xs = SLList_At(xs);
    ensures take Xs_post = SLList_At(xs);
            take R = SLList_At(return);
            Xs == Xs_post;
            Xs == R;
@*/
{
  if (xs == 0) {
    return slnil();
  } else {
    struct sllist *new_tail = IntList_copy(xs->tail);
    return slcons(xs->head, new_tail);
  }
}

struct sllist* IntList_append2 (struct sllist *xs, struct sllist *ys)
{
  if (xs == 0) {
    return IntList_copy(ys);
  } else {
    struct sllist *new_tail = IntList_append2(xs->tail, ys);
    return slcons(xs->head, new_tail);
  }
}

Exercise. Add annotations to length as appropriate:

exercises/list/length.c

#include "./headers.verif.h"

unsigned int length (struct sllist *l)
{
  if (l == 0) {
    return 0;
  } else {
    return 1 + length(l->tail);
  }
}

Exercise. Fill in the body of the following list deallocation function and add annotations as appropriate:

exercises/list/free.c

#include "./headers.verif.h"

void free__rec_sllist(struct sllist* l)
// You fill in the rest...

Exercise. Add annotations as appropriate:

exercises/slf_length_acc.c

#include "list/headers.verif.h"
#include "ref.h"
#include "free.h"

/*@
function [rec] (u32) length(datatype List xs) {
  match xs {
    Nil {} => {
      0u32
    }
    Cons {Head: h, Tail: zs}  => {
      1u32 + length(zs)
    }
  }
}
@*/

void IntList_length_acc_aux (struct sllist *xs, unsigned int *p)
{
  if (xs == 0) {
  } else {
    *p = *p + 1;
    IntList_length_acc_aux (xs->tail, p);
  }
}

unsigned int IntList_length_acc (struct sllist *xs)
{
  unsigned int *p = refUnsignedInt(0);
  IntList_length_acc_aux(xs, p);
  unsigned int x = *p;
  free__unsigned_int(p);
  return x;
}