diff --git a/src/examples/queue.c b/src/examples/queue.c index 3bd4cde1..633481dd 100644 --- a/src/examples/queue.c +++ b/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(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(tail); + take T = Owned(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(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(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(tail); + take T = Owned(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(tail); + take T2 = Owned(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(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 diff --git a/src/tutorial.adoc b/src/tutorial.adoc index c7d9f33e..059e6454 100644 --- a/src/tutorial.adoc +++ b/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(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(p) === p |-t-> V ////