diff --git a/src/examples/Dbl_Linked_List/add.c b/src/examples/Dbl_Linked_List/add.c index 0bd50510..b988d9a4 100644 --- a/src/examples/Dbl_Linked_List/add.c +++ b/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; } diff --git a/src/examples/Dbl_Linked_List/remove.c b/src/examples/Dbl_Linked_List/remove.c index 21199609..5f63c124 100644 --- a/src/examples/Dbl_Linked_List/remove.c +++ b/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; } diff --git a/src/examples/queue_pop.c b/src/examples/queue_pop.c index ed6e0837..d1053c25 100644 --- a/src/examples/queue_pop.c +++ b/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; diff --git a/src/examples/queue_pop_unified.c b/src/examples/queue_pop_unified.c index 3f67d305..da0b8018 100644 --- a/src/examples/queue_pop_unified.c +++ b/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); diff --git a/src/examples/queue_push.c b/src/examples/queue_push.c index bffa378c..e22dd152 100644 --- a/src/examples/queue_push.c +++ b/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; } } diff --git a/src/queue-example-notes.md b/src/queue-example-notes.md index 6150a10b..09eb24c9 100644 --- a/src/queue-example-notes.md +++ b/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; diff --git a/src/tutorial.adoc b/src/tutorial.adoc index b2b17434..efafaa5c 100644 --- a/src/tutorial.adoc +++ b/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