How to prove while/for in Isabelle/HOL

Question

I have this C code:

while(p->next)   p = p->next;

I want to prove that no matter how long the list is, when this loop is over, p->next equals NULL, and EIP refers to the next instruction after this loop.

But I can't. Does anyone know how to prove loops in Isabelle/HOL?

Answer 1

A set of tools (disclaimer: I am the author of the latter) that allows you to import C code into Isabelle/HOL for further reasoning is Michael Norrish's C Parser and AutoCorres.

Using AutoCorres, I can parse the following C file:

struct node {
    struct node *next;
    int data;
};

struct node * traverse_list(struct node *list)
{
    while (list)
        list = list->next;
    return list;
}

into Isabelle using the commands:

theory List
imports AutoCorres
begin

install_C_file "list.c"
autocorres [ts_rules = nondet] "list.c"

We can then prove a Hoare triple which states that, for any input state, the return value of the function will be NULL:

lemma "⦃ λs. True ⦄ traverse_list' l ⦃ λrv s. rv = NULL ⦄"
  (* Unfold the function definition. *)
  apply (unfold traverse_list'_def)

  (* Add an invariant to the while loop. *)
  apply (subst whileLoop_add_inv [where I="λnext s. True"])

  (* Run a VCG, and solve the conditions using the simplified. *)
  apply wp
  apply simp
  done

This is a partial correctness theorem, which somewhat states what you asked for. (In particular, it states that if the function terminates, and if it doesn't fault, then the post-condition is true).

For a more complete proof, you would need to add a few more things to the above:

1. You need to know that the list is valid; for instance, that intermediate nodes don't point to invalid addresses (for instance, unaligned addresses), and that the list doesn't form an loop (meaning that the while loop would never terminate).

2. You will also want to prove termination. This is related to the second condition above, but you will likely still need to make an argument about why it is true. (A typical method would be to say that the length of the list always decreases, and hence the loop will eventually terminate).

AutoCorres does not direct concept of an instruction pointer (typically these concepts only exist at the assembly level), but a proof of termination would be similar.

AutoCorres provides some basic libraries for reasoning about linked lists in DataStructures.thy, which would be a good starting point.