Merge pull request #60 from rems-project/mdd/use-arrow-syntax

Modify tutorial examples to use new arrow / `a->b` assertion syntax

src/examples/Dbl_Linked_List/add.c

@@ -20,12 +20,12 @@ struct node *add(int element, struct node *n)
         new_node->next = 0;
         return new_node;
     } else { 
-        /*@ split_case(is_null((*n).prev)); @*/
+        /*@ split_case(is_null(n->prev)); @*/
         new_node->next = n->next;
         new_node->prev = n;
 
         if (n->next !=0) {
-            /*@ split_case(is_null((*(*n).next).next)); @*/
+            /*@ split_case(is_null(n->next->next)); @*/
             n->next->prev = new_node;
         }
 

src/examples/Dbl_Linked_List/remove.c

@@ -17,12 +17,12 @@ struct node_and_int *remove(struct node *n)
 {
     struct node *temp = 0;
     if (n->prev != 0) {
-        /*@ split_case(is_null((*(*n).prev).prev)); @*/
+        /*@ split_case(is_null(n->prev->prev); @*/
         n->prev->next = n->next;
         temp = n->prev;
     }
     if (n->next != 0) {
-        /*@ split_case(is_null((*(*n).next).next)); @*/
+        /*@ split_case(is_null(n->next->next); @*/
         n->next->prev = n->prev;
         temp = n->next;
     }

src/examples/queue_pop.c

@@ -9,7 +9,7 @@ int IntQueue_pop (struct int_queue *q)
             return == hd(before);
 @*/
 {
-  /*@ split_case is_null((*q).front); @*/
+  /*@ split_case is_null(q->front); @*/
   struct int_queueCell* h = q->front;
   if (h == q->back) {
     int x = h->first;
@@ -20,7 +20,7 @@ int IntQueue_pop (struct int_queue *q)
     return x;
   } else {
     int x = h->first;
-    /*@ apply snoc_facts((*h).next, (*q).back, x); @*/
+    /*@ apply snoc_facts(h->next, q->back, x); @*/
     q->front = h->next;
     freeIntQueueCell(h);
     return x;

src/examples/queue_pop_unified.c

@@ -58,9 +58,9 @@ int IntQueue_pop (struct int_queue *q)
             return == hd(before);
 @*/
 {
-  /*@ split_case is_null((*q).front); @*/
+  /*@ split_case is_null(q->front); @*/
   struct int_queueCell* h = q->front;
-  /*@ split_case ptr_eq(h,(*q).back); @*/
+  /*@ split_case ptr_eq(h, q->back); @*/
   int x = h->first;
   q->front = h->next;
   freeIntQueueCell(h);

src/examples/queue_push.c

@@ -18,7 +18,7 @@ void IntQueue_push (int x, struct int_queue *q)
     struct int_queueCell *oldback = q->back;
     q->back->next = c;
     q->back = c;
-    /*@ apply push_lemma ((*q).front, oldback); @*/
+    /*@ apply push_lemma (q->front, oldback); @*/
     return;
   }
 }

src/queue-example-notes.md

@@ -153,7 +153,7 @@ This tells us to look at snoc, which turns out to be very wrong!
       c->first = x;
       c->next = 0;
       if (q->tail == 0) {
-        /*@ split_case (*q).head == NULL; @*/
+        /*@ split_case q->head == NULL; @*/
         /*@ apply snac_nil(x); @*/
         q->head = c;
         q->tail = c;

src/tutorial.adoc

@@ -1143,10 +1143,10 @@ as part of the rest (so that the new `+back+` cell can now be treated
 specially).
 
 One interesting technicality is worth noting: After the assignment
-`+q->back = c+` we can no longer prove `+IntQueueFB((*q).front,
+`+q->back = c+` we can no longer prove `+IntQueueFB(q->front,
 oldback)+`, but we don't care, since we want to prove
-`+IntQueueFB((*q).front, (*q).back)+`. However, crucially,
-`+IntQueueAux((*q).front, oldback)+` is still true.
+`+IntQueueFB(q->front, q->back)+`. However, crucially,
+`+IntQueueAux(q->front, oldback)+` is still true.
 
 // ======================================================================
 
@@ -1165,7 +1165,7 @@ include_example(exercises/queue_pop.c)
 
 There are three annotations to explain.  Let's consider them in order.
 
-First, the `+split_case+` on `+is_null((*q).front)+` is needed to tell
+First, the `+split_case+` on `+is_null(q->front)+` is needed to tell
 CN which of the branches of the `+if+` at the beginning of the
 `+IntQueueFB+` predicate it can "unpack".  (`+IntQueuePtr+` can be
 unpacked immediately because it is unconditional, but `+IntQueueFB+`
@@ -1354,7 +1354,7 @@ and the right part of the list is the same as before.
 Now, let's look at the annotations in the function body.
 CN can figure out the empty list case for itself, but it needs some help with the non-empty list case. The
 `split_case` on `is_null((\*n).prev)` tells CN to unpack the `Own_Backwards` predicate. Without this annotation,
-CN cannot reason that we didn't lose the left half of the list before we return, and will claim we are missing a resource for returning. The `split_case` on `is_null((*(*n).next).next)` is similar, but for unpacking the `Own_Forwards` predicate. Note that we 
+CN cannot reason that we didn't lose the left half of the list before we return, and will claim we are missing a resource for returning. The `split_case` on `is_null(n->next->next)` is similar, but for unpacking the `Own_Forwards` predicate. Note that we 
 have to go one more node forward to make sure that everything past `n->next` is still owned at the end of the function.
 
 
@@ -1485,9 +1485,6 @@ Further exercises:
 Misc things to do:
   - replace 0 with NULL in specs
 
-  - why do we have to write (*(*q).front).next instead of
-    q->front->next in CN expressions?  (Answer: not implemented yet!)
-
   - naming issues
         - rename == to ptr_eq everywhere in specs
         - rename list to seq in filenames.  or go more radical and rename seq to cnlist