Verif_stackStack ADT implemented by linked lists

Here is a little C program, stack.c

    #include <stddef.h>

    extern void * malloc (size_t n);
    extern void free (void *p);
    extern void exit(int n);

    struct cons {
      int value;
      struct cons *next;
    };

    struct stack {
      struct cons *top;
    };

    struct stack *newstack(void) {
      struct stack *p;
      p = (struct stack * ) malloc (sizeof (struct stack));
      if (!p) exit(1);
      p->top = NULL;
      return p;
    }

    void push (struct stack *p, int i) {
      struct cons *q;
      q = (struct cons * ) malloc (sizeof (struct cons));
      if (!q) exit(1);
      q->value = i;
      q->next = p->top;
      p->top = q;
    }

    int pop (struct stack *p) {
      struct cons *q;
      int i;
      q = p->top;
      p->top = q->next;
      i = q->value;
      free(q);
      return i;
    }

This program implements a stack ADT (abstract data type).

• To create a new stack, st = newstack();
• To push integer i onto the stack, push(st,i);
• To pop from the stack, i=pop(st);

This stack is implemented as a header node (struct stack) pointing to a linked list of cons cells (struct cons).

Let's verify!

Malloc and free

When you use C's malloc/free library, you write p=malloc(n); to get a pointer p to a block of n bytes; when you're done with that block, you call free(p) to dispose of it. How does the free function know how many bytes to dispose? The answer is, the malloc/free library puts an extra "header" field just before address p, so really you get this:

      +-----------+
      | header    |
      +-----------+
  p-->|  zero     |
      +-----------+
      |  one      |
      +-----------+
      |  two      |
      +-----------+

where in this case, header=3. In separation logic, we can describe this as

• malloc_token Ews p × data_at Ews (Tstruct _mystruct noattr) (zero,one,two) p

where malloc_token Ews p describes this picture:

      +-----------+
      | header    |
      +-----------+
  p-->

Of course, the malloc/free library might have a different way of "remembering" the size that p points to, so its representation of malloc_token is not necessarily a word at offset -1. Therefore, clients of the malloc/free library treat malloc_token as an abstract predicate. Now, the function-specifications of malloc and free are something like this:

If your source program says malloc(sizeof(t)), your forward_call should supply (as a WITH-witness) the C type t. Malloc may choose to return NULL, in which case the SEP part of the postcondition is emp, or it may return a pointer, in which case you get data_at_ Ews t p, and as a free bonus you get a malloc_token Ews t p. But don't lose that malloc_token! You will need to supply it later to the free function when you dispose of the object. The SEP predicate data_at_ Ews t p is an uninitialized structure of type t. It is equivalent to, data_at Ews t (default_val t) p. The default_val is basically a struct or array full of Vundef values.

Specification of linked lists

This is much like the linked lists in Verif_reverse.

Proof automation for user-defined separation predicates works better if you disable automatic simplification, as follows:

As usual, we should populate the Hint databases saturate_local and valid_pointer

Exercise: 1 star, standard (stack_listrep_properties)

See if you can remember how to prove this; or look again at Verif_reverse to see how it's done.

See if you can remember how to prove this; or look again at Verif_reverse to see how it's done.

Specification of stack data structure

Our stack data structure looks like this:

      +-----------+
      | token     |
      +-----------+       +---------
  p-->|  top------+---q-->| linked list...
      +-----------+       +---------

The stack object p points to a header node with one field top (plus a malloc token); the contents of the top field is some pointer q that points to a linked list.

Exercise: 1 star, standard (stack_properties)

Function specifications for the stack operations

Putting all the funspecs together:

Proofs of the function bodies

An Abstract Data Type (ADT) is a type provided with a representation and a set of operations. Clients of the ADT never see the representation, they only call upon the operations. Implementations of the operations do need to manipulate the representation directly. In this case, stack is our ADT. The operations are newstack, push, and pop. Clients of these operations see only stack il p, where il is the list of values that the client has pushed onto the stack, and p is the client's "handle", the address of the representation of the stack. The client does not know whether the abstract list il is represented in C data structures by a singly linked list, a doubly linked list, an array, or some other data structure. The client never unfolds the Definition stack. The operations newstack, push, pop are implemented in C, and they directly manipulate (in this case) a singly linked list. In proving the correctness of newstack, push, pop, we need to know the representation. Therefore, Hint: At the beginning of body_pop, of body_push, and of body_newstack, the first thing you should do is unfold stack in ×.

Exercise: 2 stars, standard (body_pop)

Exercise: 2 stars, standard (body_push)

Exercise: 2 stars, standard (body_newstack)