More tutorial / queue fixing and tidying

src/examples/queue.c

@@ -4,8 +4,8 @@
 #include "list_snoc.h"
 
 struct int_queue {
-  struct int_queueCell* front;  // Call them front and back!
-  struct int_queueCell* tail;
+  struct int_queueCell* front;  
+  struct int_queueCell* back;
 };
 
 struct int_queueCell {
@@ -17,18 +17,18 @@ struct int_queueCell {
 predicate (datatype seq) IntQueuePtr(pointer q) {
   take H = Owned<struct int_queue>(q);
   // CN bug: parser associativity needs fixing!
-  assert ((is_null(H.front) && is_null(H.tail)) || (!is_null(H.front) && !is_null(H.tail)));
-  take Q = IntQueueHT(H.front, H.tail);
+  assert ((is_null(H.front) && is_null(H.back)) || (!is_null(H.front) && !is_null(H.back)));
+  take Q = IntQueueFB(H.front, H.back);
   return Q;
 }
 
-predicate (datatype seq) IntQueueHT(pointer front, pointer tail) {
+predicate (datatype seq) IntQueueFB(pointer front, pointer back) {
   if (is_null(front)) {
     return Seq_Nil{};
   } else {
-    take T = Owned<struct int_queueCell>(tail);
+    take T = Owned<struct int_queueCell>(back);
     assert (is_null(T.next));
-    take Q = IntQueueAux (front, tail);
+    take Q = IntQueueAux (front, back);
     return snoc(Q, T.first);
   }
 }
@@ -43,7 +43,6 @@ predicate (datatype seq) IntQueueAux (pointer h, pointer t) {
     return Seq_Cons { head: C.first, tail: TL };
   }
 }
-
 @*/
 
 // ---------------------------------------------------------------------
@@ -53,7 +52,7 @@ extern struct int_queue *mallocIntQueue();
     requires true;
     ensures take u = Block<struct int_queue>(return);
             !ptr_eq(return,NULL);
-@*/ // 'return != NULL' should not be needed
+@*/ 
 
 extern void freeIntQueue (struct int_queue *p);
 /*@ spec freeIntQueue(pointer p);
@@ -67,7 +66,7 @@ extern struct int_queueCell *mallocIntQueueCell(struct int_queueCell*);
     ensures take u = Block<struct int_queueCell>(return);
             !ptr_eq(return, p);
             !is_null(return);
-@*/ // 'return != NULL' should not be needed
+@*/ 
 
 extern void freeIntQueueCell (struct int_queueCell *p);
 /*@ spec freeIntQueueCell(pointer p);
@@ -84,22 +83,23 @@ struct int_queue* IntQueue_empty ()
 {
   struct int_queue *p = mallocIntQueue();
   p->front = 0;
-  p->tail = 0;
+  p->back = 0;
   return p;
 }
+
 /*@
-lemma tl_snoc(pointer front, pointer tail, datatype seq before, i32 popped)
+lemma tl_snoc(pointer front, pointer back, datatype seq before, i32 popped)
 requires
-    take T = Owned<struct int_queueCell>(tail);
+    take T = Owned<struct int_queueCell>(back);
     is_null(T.next);
-    take Q = IntQueueAux(front, tail);
+    take Q = IntQueueAux(front, back);
     let after = snoc(Q, T.first);
     before == snoc (Seq_Cons{head: popped, tail: Q}, T.first);
 ensures
-    take T2 = Owned<struct int_queueCell>(tail);
+    take T2 = Owned<struct int_queueCell>(back);
     T == T2;
     is_null(T.next);
-    take Q2 = IntQueueAux(front, tail);
+    take Q2 = IntQueueAux(front, back);
     Q == Q2;
     after == tl(before);
     popped == hd(before);
@@ -115,7 +115,7 @@ int IntQueue_pop (struct int_queue *q)
 {
   // This is needed to unfold IntQueueAux, I guess?
   struct int_queueCell* h = q->front;
-  struct int_queueCell* t = q->tail;
+  struct int_queueCell* t = q->back;
   /*@ split_case is_null(h); @*/
   // This originally tested for h->next == 0, but this didn't seem to fit the structure of
   // the verification; this way works better, at least for the first branch.  But would
@@ -125,7 +125,7 @@ int IntQueue_pop (struct int_queue *q)
     // This line was missing originally -- good pedagogy to fix in stages??
     freeIntQueueCell(h);
     q->front = 0;
-    q->tail = 0;
+    q->back = 0;
     /*@ unfold snoc(Seq_Nil{}, x); @*/
     return x;
   } else {
@@ -134,22 +134,23 @@ int IntQueue_pop (struct int_queue *q)
     q->front = n;
     // Needs to deallocate here too!
     freeIntQueueCell(h);
-    /*@ apply tl_snoc(n, (*q).tail, before, x); @*/
+    /*@ apply tl_snoc(n, (*q).back, before, x); @*/
     return x;
   }
   // The return was originally here -- make sure to comment on why it got moved!
 }
 
 /*@
-lemma aux_induction(pointer front, pointer prev, pointer tail, datatype seq before, i32 prev_pushed)
+lemma aux_induction(pointer front, pointer prev, pointer back, 
+                    datatype seq before, i32 prev_pushed)
 requires
     take Prev = Owned<struct int_queueCell>(prev);
-    ptr_eq(Prev.next, tail);           // sanity check
-    Prev.first == prev_pushed;         // sanity check
     take Q = IntQueueAux(front, prev);
-    snoc(Q, prev_pushed) == before;    // sanity check
+    ptr_eq(Prev.next, back);                  // sanity check
+    Prev.first == prev_pushed;                // sanity check
+    snoc(Q, prev_pushed) == before;           // sanity check
 ensures
-    take Q2 = IntQueueAux(front, tail);
+    take Q2 = IntQueueAux(front, back);
     before == Q2;
 @*/
 
@@ -162,32 +163,27 @@ void IntQueue_push (int x, struct int_queue *q)
   struct int_queueCell *c = mallocIntQueueCell(q->front);
   c->first = x;
   c->next = 0;
-  if (q->tail == 0) {
+  if (q->back == 0) {
     /*@ assert (before == Seq_Nil{}); @*/
     q->front = c;
-    q->tail = c;
+    q->back = c;
     return;
   } else {
-    /*@ split_case ptr_eq((*q).front, (*q).tail); @*/
-    struct int_queueCell *prev = q->tail;
-    q->tail->next = c;
-    q->tail = c;
+    /*@ split_case ptr_eq((*q).front, (*q).back); @*/
+    struct int_queueCell *prev = q->back;
+    q->back->next = c;
+    q->back = c;
     /*@ apply aux_induction((*q).front, prev, c, before, (*prev).first); @*/
     return;
   }
 }
 
 // Notes:
-// - When I tried /*@ unfold IntQueueAux (H.front, H.tail, T.first); @*/
+// - When I tried /*@ unfold IntQueueAux (H.front, H.back, T.first); @*/
 //   I was confused by "the specification function `IntQueueAux' is not
 //   declared".
 //   I guess this is, again, the distinction between functions and
 //   predicates...?
-// - Seq_Cons is awkward for several reasons:
-//     - long / verbose (nothing to do about that, I guess)
-//     - Seq is capitalized, but it means seq
-//     - most important part is buried in the middle
-//     - What are the established C conventions here??
 // - lastVal can be eliminated, I think  (maybe?!)
 // - The fact that some of the Constraints in the error report are forced while
 //   others are random values filled in by the SMT solver is pretty problematic

src/tutorial.adoc

@@ -884,7 +884,7 @@ looks like on the Coq side!
 The specification of list reversal in CN relies on the familiar
 recursive list reverse function, with a recursive helper.
 
-include_example(exercises/list_snoc_cn.h)
+include_example(exercises/list_snoc.h)
 include_example(exercises/list_rev.h)
 
 To reason about the C implementation of list reverse, we need to help
@@ -941,22 +941,40 @@ Further exercises:
     declarations, etc.
 
 Misc things to do:
-  - remove the file name headers
   - replace 0 with NULL in specs
-  - rename == to ptr_eq everywhere in specs
-  - rename list to seq in filenames.  or go more radical and rename seq to cnlist
-  - consider renaming IntList to just List (and int_list to just list,
-    etc.) everywhere (since we are only dealing with one kind of list
-    in the tutorial, the extra pedantry is not getting us much; and
-    this simplification would avoid trying to fix conventions that all
-    CN code should use everywhere...)
+
+  - naming issues
+        - rename == to ptr_eq everywhere in specs
+        - rename list to seq in filenames.  or go more radical and rename seq to cnlist
+        - consider renaming IntList to just List (and int_list to just list,
+          etc.) everywhere (since we are only dealing with one kind of list
+          in the tutorial, the extra pedantry is not getting us much; and
+          this simplification would avoid trying to fix conventions that all
+          CN code should use everywhere...)
+       - related: the name Seq_Cons is awkward for several reasons:
+           - long / verbose (nothing to do about that, I guess)
+           - Seq is capitalized, but it means seq
+           - most important part is buried in the middle
+           - What are the established C conventions here??
+
   - some of the examples use int while the exercises that follow use
     unsigned int.  This is a needless source of potential confusion.
-  - Nb: take V = Owned<t>(p) === p |-t-> V
+
+  - everyplace we do storage allocation, we should really allow the
+    malloc call to return NULL if it wants to; the caller should
+    explicitly check that it didn't get back NULL.  This requires
+    defining an "exit" function" with trivial pre- and postconditions
+    (true / false).
+
+______________________
+For later:
 
 Alternative formatting tools to consider at some point (not now!):
   probably the best fit:
     https://myst-parser.readthedocs.io/en/latest/
   another very standard one to consider:
     alternative: https://www.sphinx-doc.org/en/master/index.html
+
+Misc notes:
+  - Nb: take V = Owned<t>(p) === p |-t-> V
 ////