Skip to content

Commit

Permalink
Modify examples to use a->b syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
septract committed Jul 23, 2024
1 parent 43f29e3 commit d7056a3
Show file tree
Hide file tree
Showing 7 changed files with 15 additions and 18 deletions.
4 changes: 2 additions & 2 deletions src/examples/Dbl_Linked_List/add.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}

Expand Down
4 changes: 2 additions & 2 deletions src/examples/Dbl_Linked_List/remove.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
4 changes: 2 additions & 2 deletions src/examples/queue_pop.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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;
Expand Down
4 changes: 2 additions & 2 deletions src/examples/queue_pop_unified.c
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
2 changes: 1 addition & 1 deletion src/examples/queue_push.c
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
}
2 changes: 1 addition & 1 deletion src/queue-example-notes.md
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
13 changes: 5 additions & 8 deletions src/tutorial.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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.

// ======================================================================

Expand All @@ -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+`
Expand Down Expand Up @@ -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.


Expand Down Expand Up @@ -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
Expand Down

0 comments on commit d7056a3

Please sign in to comment.