List loop decreasing inference

Jan 20, 2015 at 5:50 PM
struct node {
uint8_t val;
struct node *Prev;
struct node *Next;
I would like to iterate the list. Here is the loop statement. It is not obvious what is appropriate _(decrease ) assertion?

for(p = _head_node; p->Next != NULL; p = p->Next)
Jan 20, 2015 at 8:57 PM

The appropriate decrease assertion would be about the length of the list. To do this, you might need to embed a ghost field "contents" that contains an inductively defined list of elements contained in the actual list. However, for this to work, you will also need to have, as an invariant, that your list is not circular!

I can't really help much more than this at the moment, so I hope this helps you. If it doesn't, I can try to take the time to get back into VCC, but i can't promise much. I think an example of (simply) linked list may have been in the VCC tutorials (check the main project page) back in the day, and there may be some lecture notes or exercises of Ernie's floating around the internet.

Jan 21, 2015 at 1:52 PM
Here is the example from linked list. It wrapped the node into a list struct and add val map. I am verifying some existing code which only has node struct. If I want to keep the original unannotated code unchanged, how can I incorporate this ghost field content into the annotated code?

typedef _(dynamic_owns) struct List {
Node *head;
_(ghost \bool val[int];)
_(ghost Node *find[int];)
_(invariant head != NULL ==> \mine(head))
_(invariant \forall Node *n; \mine(n) && n->nxt ==> \mine(n->nxt))
_(invariant \forall Node *n; \mine(n) ==> val[n->data])
_(invariant \forall int v; val[v] ==> \mine(find[v]) && find[v]->data == v)
_(ghost \natural idx[Node *])
_(invariant head ==> idx[head] == 0)
_(invariant \forall Node *n, *m; \mine(n) && \mine(m) ==>
  && (idx[n] == 0 ==> n==head)
  && (n->nxt ==> idx[n->nxt] == idx[n] + 1)
  && (idx[m] == idx[n] + 1 ==> m == n->nxt)
  && (idx[m] > idx[n] ==> n->nxt)
} List;