From ac537891cc7bf16dc4b1a8e7322b33ca6f7b8857 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Fri, 19 Jul 2024 17:16:39 -0400 Subject: [PATCH 01/20] create preliminary functions for doubly ended queue --- src/examples/Dbl_Queue/WIP.c | 418 +++++++++++++++++++++++++++++++++++ 1 file changed, 418 insertions(+) create mode 100644 src/examples/Dbl_Queue/WIP.c diff --git a/src/examples/Dbl_Queue/WIP.c b/src/examples/Dbl_Queue/WIP.c new file mode 100644 index 00000000..dc571dcb --- /dev/null +++ b/src/examples/Dbl_Queue/WIP.c @@ -0,0 +1,418 @@ +#include "../list_c_types.h" +#include "../list_cn_types.h" +#include "../list_hdtl.h" +#include "../list_rev.h" + +struct dbl_queue { + struct node* front; + struct node* back; +}; + +struct node { + int data; + struct node* prev; + struct node* next; +}; + +/*@ + +// This predicate owns the outer queue structure and +// asserts that the front and back pointers are either +// both null or both point to a node. It then takes +// ownership of the nodes in the list in the forwards +// direction through a call to FB_Forwards. It returns +// a sequence of integers representing the data in the queue. +predicate (datatype seq) Dbl_Queue_Forwards (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = FB_Forwards(L.front, L.back); + return inner; + } +} + + +// This predicate owns the front and back nodes in the queue, and then +// takes calls Own_Forwards to take ownership of the rest of the nodes +// in the queue. It asserts that the front node has a null prev pointer +// and that the back node has a null next pointer. It then returns a +// sequence of integers representing the data in the queue. +predicate (datatype seq) FB_Forwards (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + // Only one node in the list, so only one node to own + take F = Owned(front); + assert (is_null(F.next)); + assert (is_null(F.prev)); + return Seq_Cons {head: F.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + take Rest = Own_Forwards(F.next, front, F, back, B.data); + return Seq_Cons{ head: F.data, tail: Rest}; + } + } +} + +// This recursive predicate takes ownership of a node in the queue, +// and includes checks that the queue is properly doubly linked. It +// also asserts that any node owned in this predicate is not the front +// or the back node. It calls itself recursively, walking forwards until +// it reaches the last node in the list, which was already owned in the +// `FB_Forwards` predicate. The base case puts the back node into the sequence, +// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. +predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, i32 b_data) { + if (ptr_eq(p,b)) { + return Seq_Cons{head: b_data, tail: Seq_Nil{}}; + } else { + take n = Owned(p); + assert (ptr_eq(n.prev, prev_pointer)); + assert(ptr_eq(prev_node.next, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Forwards(n.next, p, n, b, b_data); + return Seq_Cons{head: n.data, tail: Rest}; + } +} + +// This predicate owns the outer queue structure and +// asserts that the front and back pointers are either +// both null or both point to a node. It then takes +// ownership of the nodes in the list in the backwards +// direction through a call to FB_Backwards. It returns +// a sequence of integers representing the data in the queue +// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Forwards. +predicate (datatype seq) Dbl_Queue_Backwards (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = FB_Backwards(L.front, L.back); + return inner; + } +} + +// This predicate owns the front and back nodes in the queue, and then +// takes calls Own_Backwards to take ownership of the rest of the nodes +// in the queue. It asserts that the front node has a null prev pointer +// and that the back node has a null next pointer. It then returns a +// sequence of integers representing the data in the queue BACKWARDS. +predicate (datatype seq) FB_Backwards (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + take B = Owned(back); + assert (is_null(B.next)); + assert (is_null(B.prev)); + return Seq_Cons {head: B.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + take Rest = Own_Backwards(B.prev, back, B, front, F.data); + return Seq_Cons{ head: B.data, tail: Rest}; + } + } +} + +// This recursive predicate takes ownership of a node in the queue, +// and includes checks that the queue is properly doubly linked. It +// also asserts that any node owned in this predicate is not the front +// or the back node. It calls itself recursively, walking backwards until +// it reaches the first node in the list, which was already owned in the +// `FB_Backwards` predicate. The base case puts the front node into the sequence, +// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. +// Note that the front is put in the back because this sequence is backwards. +predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, i32 f_data) { + if (ptr_eq(p,f)) { + return Seq_Cons{head: f_data, tail: Seq_Nil{}}; + } else { + take n = Owned(p); + assert (ptr_eq(n.next, next_pointer)); + assert(ptr_eq(next_node.prev, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Backwards(n.prev, p, n, f, f_data); + return Seq_Cons{head: n.data, tail: Rest}; + } +} +@*/ + +extern struct dbl_queue *malloc_dbl_queue(); +/*@ spec malloc_dbl_queue(); + requires true; + ensures take u = Block(return); + !ptr_eq(return,NULL); +@*/ + +extern void free_dbl_queue (struct dbl_queue *p); +/*@ spec free_dbl_queue(pointer p); + requires take u = Block(p); + ensures true; +@*/ + +extern struct node *malloc_node(); +/*@ spec malloc_node(); + requires true; + ensures take u = Block(return); + !is_null(return); +@*/ + +extern void free_node (struct node *p); +/*@ spec free_node(pointer p); + requires take u = Block(p); + ensures true; +@*/ + +struct dbl_queue *empty_dbl_queue() +/*@ ensures take ret = Dbl_Queue_Forwards(return); + ret == Seq_Nil{}; +@*/ +{ + struct dbl_queue *q = malloc_dbl_queue(); + q->front = 0; + q->back = 0; + return q; +} + +// Given a dbl queue pointer, inserts a new node +// to the front of the list +void push_front (struct dbl_queue* q, int element) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Forwards(q); + ensures take After = Dbl_Queue_Forwards(q); + After == Seq_Cons{head: element, tail: Before}; +@*/ +{ + struct node *new_node = malloc_node(); + new_node->data = element; + new_node->next = q->front; + new_node->prev = 0; + /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ + + if (q->front != 0) { + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + q->front->prev = new_node; + q->front = new_node; + + } else { + // in this case, the queue is empty + q->back = new_node; + q->front = new_node; + } +} + + +int pop_front (struct dbl_queue* q) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Forwards(q); + Before != Seq_Nil{}; + ensures take After = Dbl_Queue_Forwards(q); + After == tl(Before); + hd(Before) == return; +@*/ +{ + if (q->front == 0){ + // impossible case from preconditions + return 0; + } else { + // /*@ split_case is_null((*q).front); @*/ + // /*@ apply empty_queue_seq_nil(q); @*/ + // /*@ assert(Before != Seq_Nil{} implies !is_null((*q).front); @*/ + // /*@ assert(!is_null((*q).front)); @*/ + if (q->front == q->back) { // singleton list case + int data = q->front->data; + free_node(q->front); + q->front = 0; + q->back = 0; + return data; + + } else { + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + struct node *front = q->front; + int data = front->data; + front->next->prev = 0; + q->front = front->next; + free_node(front); + + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + return data; + } + } +} + +// Given a dbl queue pointer, inserts a new node +// to the back of the list +void push_back (struct dbl_queue* q, int element) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Backwards(q); + ensures take After = Dbl_Queue_Backwards(q); + After == Seq_Cons{head: element, tail: Before}; + // Before == snoc(After, element); // reverse??? +@*/ +{ + struct node *new_node = malloc_node(); + new_node->data = element; + new_node->next = 0; + new_node->prev = q->back; + /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ + + if (q->back != 0) { + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + q->back->next = new_node; + q->back = new_node; + return; + + } else { + // in this case, the queue is empty + q->back = new_node; + q->front = new_node; + return; + } +} + +int pop_back (struct dbl_queue* q) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Backwards(q); + Before != Seq_Nil{}; + ensures take After = Dbl_Queue_Backwards(q); + After == tl(Before); + hd(Before) == return; +@*/ +{ + if (q->front == 0){ + // impossible case from preconditions + return 0; + } else { + if (q->front == q->back) { // singleton list case + int data = q->back->data; + free_node(q->back); + q->front = 0; + q->back = 0; + return data; + + } else { + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + struct node *back = q->back; + int data = back->data; + back->prev->next = 0; + q->back = back->prev; + free_node(back); + + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + return data; + } + } +} + + +void forwards_eq_backwards(struct dbl_queue *q) +/*@ + requires take for1 = Dbl_Queue_Forwards(q); + take back1 = Dbl_Queue_Backwards(q); + ensures take for2 = Dbl_Queue_Forwards(q); + take back2 = Dbl_Queue_Backwards(q); + for1 == for2; + back1 == back2; + for1 == rev(back1); + rev(for1) == back1; +@*/ +{ + if (q == 0) + { + /*@ unfold rev(for1); @*/ + /*@ unfold rev(back1); @*/ + return; + } +} + +// void switch_direction(struct dbl_queue *q) +// /*@ +// requires take forwards = Dbl_Queue_Forwards(q); +// ensures take backwards = Dbl_Queue_Backwards(q); +// // for1 == for2; +// // back1 == back2; +// // for1 == rev(back1); +// // rev(for1) == back1; +// @*/ +// { +// if (q == 0) +// { +// return; +// } else { +// if (q->front == 0) { +// /*@ assert(is_null((*q).back)); @*/ +// return; +// } +// else if (q->front == q->back){ +// return; +// } else { +// switch_direction(); +// return; +// } +// } +// } + +// void switch_direction(struct node *front, struct node *back) +// /*@ +// requires take forwards = FB_Forwards(front, back); +// ensures take backwards = FB_Backwards(front, back); +// // for1 == for2; +// // back1 == back2; +// // for1 == rev(back1); +// // rev(for1) == back1; +// @*/ +// { +// if (front == 0) { +// return; +// } +// else if (front == back){ +// return; +// } else { +// /*@ split_case(is_null(front)); @*/ +// /*@ split_case(is_null(back)); @*/ +// /*@ split_case(ptr_eq(front,back)); @*/ + +// switch_direction(front->next, back); +// return; +// } +// } + +void switch_direction(struct node *front, struct node *back) +/*@ + requires take forwards = FB_Forwards(front, back); + ensures take backwards = FB_Backwards(front, back); + // for1 == for2; + // back1 == back2; + // for1 == rev(back1); + // rev(for1) == back1; +@*/ +{ + if (front == 0) { + return; + } + else if (front == back){ + return; + } else { + /*@ split_case(is_null(front)); @*/ + /*@ split_case(is_null(back)); @*/ + /*@ split_case(ptr_eq(front,back)); @*/ + + switch_direction(front->next, back); + return; + } +} + From 199ab9b9f5563c1db4ec6ede65d39c908fef36fb Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Mon, 22 Jul 2024 13:01:42 -0400 Subject: [PATCH 02/20] Work on ownership lemmas --- src/examples/Dbl_Queue/WIP.c | 429 ++++++++++++++++---------------- src/examples/Dbl_Queue/lemmas.c | 70 ++++++ 2 files changed, 286 insertions(+), 213 deletions(-) create mode 100644 src/examples/Dbl_Queue/lemmas.c diff --git a/src/examples/Dbl_Queue/WIP.c b/src/examples/Dbl_Queue/WIP.c index dc571dcb..a40ca6c3 100644 --- a/src/examples/Dbl_Queue/WIP.c +++ b/src/examples/Dbl_Queue/WIP.c @@ -56,7 +56,7 @@ predicate (datatype seq) FB_Forwards (pointer front, pointer back) { assert (is_null(B.next)); take F = Owned(front); assert(is_null(F.prev)); - take Rest = Own_Forwards(F.next, front, F, back, B.data); + take Rest = Own_Forwards(F.next, front, F, back, B); return Seq_Cons{ head: F.data, tail: Rest}; } } @@ -69,16 +69,17 @@ predicate (datatype seq) FB_Forwards (pointer front, pointer back) { // it reaches the last node in the list, which was already owned in the // `FB_Forwards` predicate. The base case puts the back node into the sequence, // in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, i32 b_data) { +predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { if (ptr_eq(p,b)) { - return Seq_Cons{head: b_data, tail: Seq_Nil{}}; + assert(ptr_eq(Back.prev, prev_pointer)); + return Seq_Cons{head: Back.data, tail: Seq_Nil{}}; } else { take n = Owned(p); assert (ptr_eq(n.prev, prev_pointer)); assert(ptr_eq(prev_node.next, p)); assert(!is_null(n.next)); assert(!is_null(n.prev)); - take Rest = Own_Forwards(n.next, p, n, b, b_data); + take Rest = Own_Forwards(n.next, p, n, b, Back); return Seq_Cons{head: n.data, tail: Rest}; } } @@ -122,7 +123,7 @@ predicate (datatype seq) FB_Backwards (pointer front, pointer back) { assert (is_null(B.next)); take F = Owned(front); assert(is_null(F.prev)); - take Rest = Own_Backwards(B.prev, back, B, front, F.data); + take Rest = Own_Backwards(B.prev, back, B, front, F); return Seq_Cons{ head: B.data, tail: Rest}; } } @@ -136,16 +137,17 @@ predicate (datatype seq) FB_Backwards (pointer front, pointer back) { // `FB_Backwards` predicate. The base case puts the front node into the sequence, // in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. // Note that the front is put in the back because this sequence is backwards. -predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, i32 f_data) { +predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { if (ptr_eq(p,f)) { - return Seq_Cons{head: f_data, tail: Seq_Nil{}}; + assert(ptr_eq(Front.next, next_pointer)); + return Seq_Cons{head: Front.data, tail: Seq_Nil{}}; } else { take n = Owned(p); assert (ptr_eq(n.next, next_pointer)); assert(ptr_eq(next_node.prev, p)); assert(!is_null(n.next)); assert(!is_null(n.prev)); - take Rest = Own_Backwards(n.prev, p, n, f, f_data); + take Rest = Own_Backwards(n.prev, p, n, f, Front); return Seq_Cons{head: n.data, tail: Rest}; } } @@ -188,231 +190,232 @@ struct dbl_queue *empty_dbl_queue() return q; } -// Given a dbl queue pointer, inserts a new node -// to the front of the list -void push_front (struct dbl_queue* q, int element) -/*@ requires (!is_null(q)); - take Before = Dbl_Queue_Forwards(q); - ensures take After = Dbl_Queue_Forwards(q); - After == Seq_Cons{head: element, tail: Before}; -@*/ -{ - struct node *new_node = malloc_node(); - new_node->data = element; - new_node->next = q->front; - new_node->prev = 0; - /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ - - if (q->front != 0) { - /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ - q->front->prev = new_node; - q->front = new_node; - - } else { - // in this case, the queue is empty - q->back = new_node; - q->front = new_node; - } -} - - -int pop_front (struct dbl_queue* q) -/*@ requires (!is_null(q)); - take Before = Dbl_Queue_Forwards(q); - Before != Seq_Nil{}; - ensures take After = Dbl_Queue_Forwards(q); - After == tl(Before); - hd(Before) == return; -@*/ -{ - if (q->front == 0){ - // impossible case from preconditions - return 0; - } else { - // /*@ split_case is_null((*q).front); @*/ - // /*@ apply empty_queue_seq_nil(q); @*/ - // /*@ assert(Before != Seq_Nil{} implies !is_null((*q).front); @*/ - // /*@ assert(!is_null((*q).front)); @*/ - if (q->front == q->back) { // singleton list case - int data = q->front->data; - free_node(q->front); - q->front = 0; - q->back = 0; - return data; - - } else { - /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ - struct node *front = q->front; - int data = front->data; - front->next->prev = 0; - q->front = front->next; - free_node(front); - - /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ - return data; - } - } -} - -// Given a dbl queue pointer, inserts a new node -// to the back of the list -void push_back (struct dbl_queue* q, int element) -/*@ requires (!is_null(q)); - take Before = Dbl_Queue_Backwards(q); - ensures take After = Dbl_Queue_Backwards(q); - After == Seq_Cons{head: element, tail: Before}; - // Before == snoc(After, element); // reverse??? -@*/ -{ - struct node *new_node = malloc_node(); - new_node->data = element; - new_node->next = 0; - new_node->prev = q->back; - /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ - - if (q->back != 0) { - /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ - q->back->next = new_node; - q->back = new_node; - return; - - } else { - // in this case, the queue is empty - q->back = new_node; - q->front = new_node; - return; - } -} +// // Given a dbl queue pointer, inserts a new node +// // to the front of the list +// void push_front (struct dbl_queue* q, int element) +// /*@ requires (!is_null(q)); +// take Before = Dbl_Queue_Forwards(q); +// ensures take After = Dbl_Queue_Forwards(q); +// After == Seq_Cons{head: element, tail: Before}; +// @*/ +// { +// struct node *new_node = malloc_node(); +// new_node->data = element; +// new_node->next = q->front; +// new_node->prev = 0; +// /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ -int pop_back (struct dbl_queue* q) -/*@ requires (!is_null(q)); - take Before = Dbl_Queue_Backwards(q); - Before != Seq_Nil{}; - ensures take After = Dbl_Queue_Backwards(q); - After == tl(Before); - hd(Before) == return; -@*/ -{ - if (q->front == 0){ - // impossible case from preconditions - return 0; - } else { - if (q->front == q->back) { // singleton list case - int data = q->back->data; - free_node(q->back); - q->front = 0; - q->back = 0; - return data; - - } else { - /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ - struct node *back = q->back; - int data = back->data; - back->prev->next = 0; - q->back = back->prev; - free_node(back); - - /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ - return data; - } - } -} +// if (q->front != 0) { +// /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ +// q->front->prev = new_node; +// q->front = new_node; +// } else { +// // in this case, the queue is empty +// q->back = new_node; +// q->front = new_node; +// } +// } -void forwards_eq_backwards(struct dbl_queue *q) -/*@ - requires take for1 = Dbl_Queue_Forwards(q); - take back1 = Dbl_Queue_Backwards(q); - ensures take for2 = Dbl_Queue_Forwards(q); - take back2 = Dbl_Queue_Backwards(q); - for1 == for2; - back1 == back2; - for1 == rev(back1); - rev(for1) == back1; -@*/ -{ - if (q == 0) - { - /*@ unfold rev(for1); @*/ - /*@ unfold rev(back1); @*/ - return; - } -} -// void switch_direction(struct dbl_queue *q) -// /*@ -// requires take forwards = Dbl_Queue_Forwards(q); -// ensures take backwards = Dbl_Queue_Backwards(q); -// // for1 == for2; -// // back1 == back2; -// // for1 == rev(back1); -// // rev(for1) == back1; +// int pop_front (struct dbl_queue* q) +// /*@ requires (!is_null(q)); +// take Before = Dbl_Queue_Forwards(q); +// Before != Seq_Nil{}; +// ensures take After = Dbl_Queue_Forwards(q); +// After == tl(Before); +// hd(Before) == return; // @*/ // { -// if (q == 0) -// { -// return; +// if (q->front == 0){ +// // impossible case from preconditions +// return 0; // } else { -// if (q->front == 0) { -// /*@ assert(is_null((*q).back)); @*/ -// return; -// } -// else if (q->front == q->back){ -// return; +// // /*@ split_case is_null((*q).front); @*/ +// // /*@ apply empty_queue_seq_nil(q); @*/ +// // /*@ assert(Before != Seq_Nil{} implies !is_null((*q).front); @*/ +// // /*@ assert(!is_null((*q).front)); @*/ +// if (q->front == q->back) { // singleton list case +// int data = q->front->data; +// free_node(q->front); +// q->front = 0; +// q->back = 0; +// return data; + // } else { -// switch_direction(); -// return; +// /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ +// struct node *front = q->front; +// int data = front->data; +// front->next->prev = 0; +// q->front = front->next; +// free_node(front); + +// /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ +// return data; // } // } // } -// void switch_direction(struct node *front, struct node *back) -// /*@ -// requires take forwards = FB_Forwards(front, back); -// ensures take backwards = FB_Backwards(front, back); -// // for1 == for2; -// // back1 == back2; -// // for1 == rev(back1); -// // rev(for1) == back1; +// // Given a dbl queue pointer, inserts a new node +// // to the back of the list +// void push_back (struct dbl_queue* q, int element) +// /*@ requires (!is_null(q)); +// take Before = Dbl_Queue_Backwards(q); +// ensures take After = Dbl_Queue_Backwards(q); +// After == Seq_Cons{head: element, tail: Before}; +// // Before == snoc(After, element); // reverse??? // @*/ // { -// if (front == 0) { +// struct node *new_node = malloc_node(); +// new_node->data = element; +// new_node->next = 0; +// new_node->prev = q->back; +// /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ + +// if (q->back != 0) { +// /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ +// q->back->next = new_node; +// q->back = new_node; // return; -// } -// else if (front == back){ + +// } else { +// // in this case, the queue is empty +// q->back = new_node; +// q->front = new_node; // return; +// } +// } + +// int pop_back (struct dbl_queue* q) +// /*@ requires (!is_null(q)); +// take Before = Dbl_Queue_Backwards(q); +// Before != Seq_Nil{}; +// ensures take After = Dbl_Queue_Backwards(q); +// After == tl(Before); +// hd(Before) == return; +// @*/ +// { +// if (q->front == 0){ +// // impossible case from preconditions +// return 0; // } else { -// /*@ split_case(is_null(front)); @*/ -// /*@ split_case(is_null(back)); @*/ -// /*@ split_case(ptr_eq(front,back)); @*/ +// if (q->front == q->back) { // singleton list case +// int data = q->back->data; +// free_node(q->back); +// q->front = 0; +// q->back = 0; +// return data; -// switch_direction(front->next, back); -// return; +// } else { +// /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ +// struct node *back = q->back; +// int data = back->data; +// back->prev->next = 0; +// q->back = back->prev; +// free_node(back); + +// /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ +// return data; +// } // } // } -void switch_direction(struct node *front, struct node *back) -/*@ - requires take forwards = FB_Forwards(front, back); - ensures take backwards = FB_Backwards(front, back); - // for1 == for2; - // back1 == back2; - // for1 == rev(back1); - // rev(for1) == back1; -@*/ -{ - if (front == 0) { - return; - } - else if (front == back){ - return; - } else { - /*@ split_case(is_null(front)); @*/ - /*@ split_case(is_null(back)); @*/ - /*@ split_case(ptr_eq(front,back)); @*/ - switch_direction(front->next, back); - return; - } -} +// // void forwards_eq_backwards(struct dbl_queue *q) +// // /*@ +// // requires take for1 = Dbl_Queue_Forwards(q); +// // take back1 = Dbl_Queue_Backwards(q); +// // ensures take for2 = Dbl_Queue_Forwards(q); +// // take back2 = Dbl_Queue_Backwards(q); +// // for1 == for2; +// // back1 == back2; +// // for1 == rev(back1); +// // rev(for1) == back1; +// // @*/ +// // { +// // if (q == 0) +// // { +// // /*@ unfold rev(for1); @*/ +// // /*@ unfold rev(back1); @*/ +// // return; +// // } +// // } + +// // void switch_direction(struct dbl_queue *q) +// // /*@ +// // requires take forwards = Dbl_Queue_Forwards(q); +// // ensures take backwards = Dbl_Queue_Backwards(q); +// // // for1 == for2; +// // // back1 == back2; +// // // for1 == rev(back1); +// // // rev(for1) == back1; +// // @*/ +// // { +// // if (q == 0) +// // { +// // return; +// // } else { +// // if (q->front == 0) { +// // /*@ assert(is_null((*q).back)); @*/ +// // return; +// // } +// // else if (q->front == q->back){ +// // return; +// // } else { +// // forwards_eq_backwards(q); +// // // switch_direction(); +// // return; +// // } +// // } +// // } + +// // void switch_direction(struct node *front, struct node *back) +// // /*@ +// // requires take forwards = FB_Forwards(front, back); +// // ensures take backwards = FB_Backwards(front, back); +// // // for1 == for2; +// // // back1 == back2; +// // // for1 == rev(back1); +// // // rev(for1) == back1; +// // @*/ +// // { +// // if (front == 0) { +// // return; +// // } +// // else if (front == back){ +// // return; +// // } else { +// // /*@ split_case(is_null(front)); @*/ +// // /*@ split_case(is_null(back)); @*/ +// // /*@ split_case(ptr_eq(front,back)); @*/ + +// // switch_direction(front->next, back); +// // return; +// // } +// // } + +// // void switch_direction(struct node *front, struct node *back) +// // /*@ +// // requires take forwards = FB_Forwards(front, back); +// // ensures take backwards = FB_Backwards(front, back); +// // // for1 == for2; +// // // back1 == back2; +// // // for1 == rev(back1); +// // // rev(for1) == back1; +// // @*/ +// // { +// // if (front == 0) { +// // return; +// // } +// // else if (front == back){ +// // return; +// // } else { +// // /*@ split_case(is_null(front)); @*/ +// // /*@ split_case(is_null(back)); @*/ +// // /*@ split_case(ptr_eq(front,back)); @*/ + +// // switch_direction(front->next, back); +// // return; +// // } +// // } diff --git a/src/examples/Dbl_Queue/lemmas.c b/src/examples/Dbl_Queue/lemmas.c new file mode 100644 index 00000000..9372ebf2 --- /dev/null +++ b/src/examples/Dbl_Queue/lemmas.c @@ -0,0 +1,70 @@ +#include "./WIP.c" + +void own_forwards_backwards(struct node *front, struct node *back) +/*@ requires + take B = Owned(back); + is_null(B.next); + take F = Owned(front); + // ptr_eq(F.next,back) implies ptr_eq(B.prev, front); + // ptr_eq(B.prev, front) implies ptr_eq(F.next,back); + + // (is_null(F.next) && is_null(B.prev)) || (!is_null(F.next) && !is_null(B.prev)); + + // is_null(F.prev); // doesn't work because of recursive call + take Fwd = Own_Forwards(F.next, front, F, back, B); + ensures + take B2 = Owned(back); + B == B2; + take F2 = Owned(front); + F == F2; + take Bwd = Own_Backwards(B.prev, back, B, front, F); + Seq_Cons{head: F.data, tail: Fwd} == rev (Seq_Cons{head: B.data, tail: Bwd}); +@*/ +{ + if (front == 0) { + return; + } else { + if (front == back) { + return; + } else { + /*@ split_case(ptr_eq(front, back)); @*/ + /*@ split_case(is_null((*front).next)); @*/ + /*@ unfold rev(Seq_Cons {head: (*front).data, tail: Seq_Nil {}}); @*/ + /*@ unfold rev(Seq_Nil{}); @*/ + /*@ unfold snoc(Seq_Nil{}, (*front).data); @*/ + if (front->next == 0) { + return; + } else { + if (front->next == back) { + /*@ split_case(ptr_eq(front, back)); @*/ + /*@ split_case(is_null((*front).next)); @*/ + /*@ split_case(ptr_eq((*front).next, back)); @*/ + /*@ assert(ptr_eq((*back).prev, front)); @*/ + return; + } else { + /*@ assert(!is_null((*front).next)); @*/ + /*@ assert(!is_null((*(*front).next).next)); @*/ + /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ + /*@ assert(!is_null((*back).prev)); @*/ + // /*@ assert(!is_null((*(*back).prev).prev)); @*/ + own_forwards_backwards(front->next, back); + /*@ assert(!is_null((*front).next)); @*/ + /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ + + /*@ split_case(ptr_eq(front, back)); @*/ + /*@ split_case(is_null((*front).next)); @*/ + /*@ split_case(ptr_eq((*front).next, back)); @*/ + + /*@ split_case(ptr_eq((*(*front).next).next, back)); @*/ + + /*@ split_case(ptr_eq((*back).prev, front)); @*/ + + // /*@ split_case(ptr_eq((*(*back).prev).prev, front)); @*/ + + + return; + } + } + } + } +} \ No newline at end of file From 255d0ff66f6eed08b03281a2621765f972f29d69 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Mon, 22 Jul 2024 19:59:44 -0400 Subject: [PATCH 03/20] verify append lemma for own_forwards and backwards --- src/examples/Dbl_Queue/lemmas_other.c | 129 +++++++++++++++++++++ src/examples/Dbl_Queue/preds_other.c | 156 ++++++++++++++++++++++++++ 2 files changed, 285 insertions(+) create mode 100644 src/examples/Dbl_Queue/lemmas_other.c create mode 100644 src/examples/Dbl_Queue/preds_other.c diff --git a/src/examples/Dbl_Queue/lemmas_other.c b/src/examples/Dbl_Queue/lemmas_other.c new file mode 100644 index 00000000..91a7fdda --- /dev/null +++ b/src/examples/Dbl_Queue/lemmas_other.c @@ -0,0 +1,129 @@ +#include "./preds_other.c" + +//WIP, doesn't verify +// void own_forwards_backwards(struct node *front, struct node *back) +// /*@ requires +// take B = Owned(back); +// is_null(B.next); +// take F = Owned(front); +// // ptr_eq(F.next,back) implies ptr_eq(B.prev, front); +// // ptr_eq(B.prev, front) implies ptr_eq(F.next,back); + +// // (is_null(F.next) && is_null(B.prev)) || (!is_null(F.next) && !is_null(B.prev)); + +// // is_null(F.prev); // doesn't work because of recursive call +// take Fwd = Own_Forwards(F.next, front, F, back, B); +// ensures +// take B2 = Owned(back); +// B == B2; +// take F2 = Owned(front); +// F == F2; +// take Bwd = Own_Backwards(B.prev, back, B, front, F); +// Seq_Cons{head: F.data, tail: Fwd} == rev (Seq_Cons{head: B.data, tail: Bwd}); +// @*/ +// { +// if (front == 0) { +// return; +// } else { +// if (front == back) { +// return; +// } else { +// /*@ split_case(ptr_eq(front, back)); @*/ +// /*@ split_case(is_null((*front).next)); @*/ +// /*@ unfold rev(Seq_Cons {head: (*front).data, tail: Seq_Nil {}}); @*/ +// /*@ unfold rev(Seq_Nil{}); @*/ +// /*@ unfold snoc(Seq_Nil{}, (*front).data); @*/ +// if (front->next == 0) { +// return; +// } else { +// if (front->next == back) { +// /*@ split_case(ptr_eq(front, back)); @*/ +// /*@ split_case(is_null((*front).next)); @*/ +// /*@ split_case(ptr_eq((*front).next, back)); @*/ +// /*@ assert(ptr_eq((*back).prev, front)); @*/ +// return; +// } else { +// /*@ assert(!is_null((*front).next)); @*/ +// /*@ assert(!is_null((*(*front).next).next)); @*/ +// /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ +// /*@ assert(!is_null((*back).prev)); @*/ +// // /*@ assert(!is_null((*(*back).prev).prev)); @*/ +// own_forwards_backwards(front->next, back); +// /*@ assert(!is_null((*front).next)); @*/ +// /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ + +// /*@ split_case(ptr_eq(front, back)); @*/ +// /*@ split_case(is_null((*front).next)); @*/ +// /*@ split_case(ptr_eq((*front).next, back)); @*/ + +// /*@ split_case(ptr_eq((*(*front).next).next, back)); @*/ + +// /*@ split_case(ptr_eq((*back).prev, front)); @*/ + +// // /*@ split_case(ptr_eq((*(*back).prev).prev, front)); @*/ + + +// return; +// } +// } +// } +// } +// } + +void own_forwards_append_lemma(struct node *front, struct node *second_last, struct node *last) +/*@ + requires + take F = Owned(front); + take Second_last = Owned(second_last); + take Fwd = Own_Forwards(F.next, front, F, second_last, Second_last); + ptr_eq(Second_last.next, last); + take Last = Owned(last); + ptr_eq(Last.prev, second_last); + ensures + take F2 = Owned(front); + take Last2 = Owned(last); + take Fwd2 = Own_Forwards(F.next, front, F, last, Last2); + Fwd2 == snoc(Fwd, Second_last.data); + Last == Last2; + F2 == F; +@*/ +{ + /*@ unfold snoc(Seq_Nil{}, (*second_last).data); @*/ + /*@ unfold snoc(Fwd, (*second_last).data); @*/ + + if (front->next == second_last) { + return; + } else { + own_forwards_append_lemma(front->next, second_last, last); + return; + } +} + +void own_backwards_append_lemma(struct node *front, struct node *second_front, struct node *last) +/*@ + requires + take F = Owned(front); + take Second_front = Owned(second_front); + take Last = Owned(last); + take Bwd = Own_Backwards(Last.prev, last, Last, second_front, Second_front); + ptr_eq(Second_front.prev, front); + ptr_eq(F.next, second_front); + ensures + take F2 = Owned(front); + take Last2 = Owned(last); + take Bwd2 = Own_Backwards(Last.prev, last, Last, front, F2); + Bwd2 == snoc(Bwd, Second_front.data); + Last == Last2; + F2 == F; +@*/ +{ + /*@ unfold snoc(Seq_Nil{}, (*second_front).data); @*/ + /*@ unfold snoc(Bwd, (*second_front).data); @*/ + + if (last->prev == second_front) { + return; + } else { + own_backwards_append_lemma(front, second_front, last->prev); + return; + } +} diff --git a/src/examples/Dbl_Queue/preds_other.c b/src/examples/Dbl_Queue/preds_other.c new file mode 100644 index 00000000..fc790c3a --- /dev/null +++ b/src/examples/Dbl_Queue/preds_other.c @@ -0,0 +1,156 @@ +#include "../list_c_types.h" +#include "../list_cn_types.h" +#include "../list_hdtl.h" +#include "../list_rev.h" + +struct dbl_queue { + struct node* front; + struct node* back; +}; + +struct node { + int data; + struct node* prev; + struct node* next; +}; + +/*@ + +// This predicate owns the outer queue structure and +// asserts that the front and back pointers are either +// both null or both point to a node. It then takes +// ownership of the nodes in the list in the forwards +// direction through a call to FB_Forwards. It returns +// a sequence of integers representing the data in the queue. +predicate (datatype seq) Dbl_Queue_Forwards (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = FB_Forwards(L.front, L.back); + return inner; + } +} + + +// This predicate owns the front and back nodes in the queue, and then +// takes calls Own_Forwards to take ownership of the rest of the nodes +// in the queue. It asserts that the front node has a null prev pointer +// and that the back node has a null next pointer. It then returns a +// sequence of integers representing the data in the queue. +predicate (datatype seq) FB_Forwards (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + // Only one node in the list, so only one node to own + take F = Owned(front); + assert (is_null(F.next)); + assert (is_null(F.prev)); + return Seq_Cons {head: F.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + take Rest = Own_Forwards(F.next, front, F, back, B); + return Seq_Cons{ head: F.data, tail: snoc(Rest, B.data)}; + } + } +} + +// This recursive predicate takes ownership of a node in the queue, +// and includes checks that the queue is properly doubly linked. It +// also asserts that any node owned in this predicate is not the front +// or the back node. It calls itself recursively, walking forwards until +// it reaches the last node in the list, which was already owned in the +// `FB_Forwards` predicate. The base case puts the back node into the sequence, +// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. +predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { + if (ptr_eq(p,b)) { + assert(ptr_eq(Back.prev, prev_pointer)); + assert(ptr_eq(prev_node.next, b)); + return Seq_Nil{}; + } else { + take n = Owned(p); + assert (ptr_eq(n.prev, prev_pointer)); + assert(ptr_eq(prev_node.next, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Forwards(n.next, p, n, b, Back); + return Seq_Cons{head: n.data, tail: Rest}; + } +} + +// This predicate owns the outer queue structure and +// asserts that the front and back pointers are either +// both null or both point to a node. It then takes +// ownership of the nodes in the list in the backwards +// direction through a call to FB_Backwards. It returns +// a sequence of integers representing the data in the queue +// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Forwards. +predicate (datatype seq) Dbl_Queue_Backwards (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = FB_Backwards(L.front, L.back); + return inner; + } +} + +// This predicate owns the front and back nodes in the queue, and then +// takes calls Own_Backwards to take ownership of the rest of the nodes +// in the queue. It asserts that the front node has a null prev pointer +// and that the back node has a null next pointer. It then returns a +// sequence of integers representing the data in the queue BACKWARDS. +predicate (datatype seq) FB_Backwards (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + take B = Owned(back); + assert (is_null(B.next)); + assert (is_null(B.prev)); + return Seq_Cons {head: B.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + take Rest = Own_Backwards(B.prev, back, B, front, F); + return Seq_Cons{ head: B.data, tail: snoc(Rest, F.data)}; + } + } +} + +// This recursive predicate takes ownership of a node in the queue, +// and includes checks that the queue is properly doubly linked. It +// also asserts that any node owned in this predicate is not the front +// or the back node. It calls itself recursively, walking backwards until +// it reaches the first node in the list, which was already owned in the +// `FB_Backwards` predicate. The base case puts the front node into the sequence, +// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. +// Note that the front is put in the back because this sequence is backwards. +predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { + if (ptr_eq(p,f)) { + assert(ptr_eq(Front.next, next_pointer)); + assert(ptr_eq(next_node.prev, f)); + return Seq_Nil{}; + } else { + take n = Owned(p); + assert (ptr_eq(n.next, next_pointer)); + assert(ptr_eq(next_node.prev, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Backwards(n.prev, p, n, f, Front); + return Seq_Cons{head: n.data, tail: Rest}; + } +} +@*/ \ No newline at end of file From 1b4421538bcd545ed4e7b04e05661897334f69da Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Tue, 23 Jul 2024 10:23:14 -0400 Subject: [PATCH 04/20] prove forwards equals backwards lemma --- src/examples/Dbl_Queue/lemmas_other.c | 114 ++++++++++---------------- src/examples/Dbl_Queue/preds_other.c | 3 + 2 files changed, 47 insertions(+), 70 deletions(-) diff --git a/src/examples/Dbl_Queue/lemmas_other.c b/src/examples/Dbl_Queue/lemmas_other.c index 91a7fdda..88b0a5d5 100644 --- a/src/examples/Dbl_Queue/lemmas_other.c +++ b/src/examples/Dbl_Queue/lemmas_other.c @@ -1,75 +1,5 @@ #include "./preds_other.c" -//WIP, doesn't verify -// void own_forwards_backwards(struct node *front, struct node *back) -// /*@ requires -// take B = Owned(back); -// is_null(B.next); -// take F = Owned(front); -// // ptr_eq(F.next,back) implies ptr_eq(B.prev, front); -// // ptr_eq(B.prev, front) implies ptr_eq(F.next,back); - -// // (is_null(F.next) && is_null(B.prev)) || (!is_null(F.next) && !is_null(B.prev)); - -// // is_null(F.prev); // doesn't work because of recursive call -// take Fwd = Own_Forwards(F.next, front, F, back, B); -// ensures -// take B2 = Owned(back); -// B == B2; -// take F2 = Owned(front); -// F == F2; -// take Bwd = Own_Backwards(B.prev, back, B, front, F); -// Seq_Cons{head: F.data, tail: Fwd} == rev (Seq_Cons{head: B.data, tail: Bwd}); -// @*/ -// { -// if (front == 0) { -// return; -// } else { -// if (front == back) { -// return; -// } else { -// /*@ split_case(ptr_eq(front, back)); @*/ -// /*@ split_case(is_null((*front).next)); @*/ -// /*@ unfold rev(Seq_Cons {head: (*front).data, tail: Seq_Nil {}}); @*/ -// /*@ unfold rev(Seq_Nil{}); @*/ -// /*@ unfold snoc(Seq_Nil{}, (*front).data); @*/ -// if (front->next == 0) { -// return; -// } else { -// if (front->next == back) { -// /*@ split_case(ptr_eq(front, back)); @*/ -// /*@ split_case(is_null((*front).next)); @*/ -// /*@ split_case(ptr_eq((*front).next, back)); @*/ -// /*@ assert(ptr_eq((*back).prev, front)); @*/ -// return; -// } else { -// /*@ assert(!is_null((*front).next)); @*/ -// /*@ assert(!is_null((*(*front).next).next)); @*/ -// /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ -// /*@ assert(!is_null((*back).prev)); @*/ -// // /*@ assert(!is_null((*(*back).prev).prev)); @*/ -// own_forwards_backwards(front->next, back); -// /*@ assert(!is_null((*front).next)); @*/ -// /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ - -// /*@ split_case(ptr_eq(front, back)); @*/ -// /*@ split_case(is_null((*front).next)); @*/ -// /*@ split_case(ptr_eq((*front).next, back)); @*/ - -// /*@ split_case(ptr_eq((*(*front).next).next, back)); @*/ - -// /*@ split_case(ptr_eq((*back).prev, front)); @*/ - -// // /*@ split_case(ptr_eq((*(*back).prev).prev, front)); @*/ - - -// return; -// } -// } -// } -// } -// } - void own_forwards_append_lemma(struct node *front, struct node *second_last, struct node *last) /*@ requires @@ -115,6 +45,9 @@ void own_backwards_append_lemma(struct node *front, struct node *second_front, s Bwd2 == snoc(Bwd, Second_front.data); Last == Last2; F2 == F; + ptr_eq(F.next, second_front); + {front} unchanged; {second_front} unchanged; {last} unchanged; + @*/ { /*@ unfold snoc(Seq_Nil{}, (*second_front).data); @*/ @@ -127,3 +60,44 @@ void own_backwards_append_lemma(struct node *front, struct node *second_front, s return; } } + +void own_fwd_eq_bwd_lemma(struct node *front, struct node *back) +/*@ requires + !ptr_eq(front, back); + + take B = Owned(back); + is_null(B.next); + !is_null(B.prev); + + take F = Owned(front); + !is_null(F.next); + + take Fwd = Own_Forwards(F.next, front, F, back, B); + ptr_eq(F.next, back) implies Fwd == Seq_Nil{}; + + Fwd == Seq_Nil{} implies ptr_eq(F.next, back); + + ensures + take B2 = Owned(back); + B == B2; + take F2 = Owned(front); + F == F2; + take Bwd = Own_Backwards(B.prev, back, B, front, F); + rev(Fwd) == Bwd; +@*/ +{ + /*@ unfold rev(Seq_Nil{}); @*/ + if (front->next == 0) { + return; + } else { + if (front->next == back) { + return; + } else { + /*@ split_case(ptr_eq(front->next->next, back)); @*/ + own_fwd_eq_bwd_lemma(front->next, back); + own_backwards_append_lemma(front, front->next, back); + /*@ unfold rev(Fwd); @*/ + return; + } + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/preds_other.c b/src/examples/Dbl_Queue/preds_other.c index fc790c3a..46e053ff 100644 --- a/src/examples/Dbl_Queue/preds_other.c +++ b/src/examples/Dbl_Queue/preds_other.c @@ -73,6 +73,7 @@ predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct no if (ptr_eq(p,b)) { assert(ptr_eq(Back.prev, prev_pointer)); assert(ptr_eq(prev_node.next, b)); + assert(ptr_eq(p,b)); return Seq_Nil{}; } else { take n = Owned(p); @@ -80,7 +81,9 @@ predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct no assert(ptr_eq(prev_node.next, p)); assert(!is_null(n.next)); assert(!is_null(n.prev)); + assert(!ptr_eq(p,b)); take Rest = Own_Forwards(n.next, p, n, b, Back); + assert(!(Seq_Cons{head: n.data, tail: Rest} == Seq_Nil{})); return Seq_Cons{head: n.data, tail: Rest}; } } From 3d8c7a3c7ad3b5a158c972fbfd387faef6c32faa Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Tue, 23 Jul 2024 10:28:59 -0400 Subject: [PATCH 05/20] prove backwards direction --- src/examples/Dbl_Queue/lemmas_other.c | 41 +++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) diff --git a/src/examples/Dbl_Queue/lemmas_other.c b/src/examples/Dbl_Queue/lemmas_other.c index 88b0a5d5..2d941deb 100644 --- a/src/examples/Dbl_Queue/lemmas_other.c +++ b/src/examples/Dbl_Queue/lemmas_other.c @@ -100,4 +100,45 @@ void own_fwd_eq_bwd_lemma(struct node *front, struct node *back) return; } } +} + +void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) +/*@ requires + !ptr_eq(front, back); + + take B = Owned(back); + !is_null(B.prev); + + take F = Owned(front); + !is_null(F.next); + is_null(F.prev); + + take Bwd = Own_Backwards(B.prev, back, B, front, F); + + ptr_eq(B.prev, front) implies Bwd == Seq_Nil{}; + Bwd == Seq_Nil{} implies ptr_eq(B.prev, front); + + ensures + take B2 = Owned(back); + B == B2; + take F2 = Owned(front); + F == F2; + take Fwd = Own_Forwards(F.next, front, F, back, B); + rev(Bwd) == Fwd; +@*/ +{ + /*@ unfold rev(Seq_Nil{}); @*/ + if (back->prev == 0) { + return; + } else { + if (back->prev == front) { + return; + } else { + /*@ split_case(ptr_eq(back->prev->prev, front)); @*/ + own_bwd_eq_fwd_lemma(front, back->prev); + own_forwards_append_lemma(front, back->prev, back); + /*@ unfold rev(Bwd); @*/ + return; + } + } } \ No newline at end of file From 9412a681c3e9567989960867088ed6ebb143d669 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Thu, 25 Jul 2024 14:36:25 -0400 Subject: [PATCH 06/20] nit --- src/examples/Dbl_Queue/preds_other.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/examples/Dbl_Queue/preds_other.c b/src/examples/Dbl_Queue/preds_other.c index 46e053ff..b2c1f5ec 100644 --- a/src/examples/Dbl_Queue/preds_other.c +++ b/src/examples/Dbl_Queue/preds_other.c @@ -52,11 +52,13 @@ predicate (datatype seq) FB_Forwards (pointer front, pointer back) { assert (is_null(F.prev)); return Seq_Cons {head: F.data, tail: Seq_Nil{}}; } else { - take B = Owned(back); + take B = Owned(back); //idea: own LAST assert (is_null(B.next)); take F = Owned(front); assert(is_null(F.prev)); take Rest = Own_Forwards(F.next, front, F, back, B); + assert(ptr_eq(F.next, back) implies Rest == Seq_Nil{}); + assert(Rest == Seq_Nil{} implies ptr_eq(F.next, back)); return Seq_Cons{ head: F.data, tail: snoc(Rest, B.data)}; } } @@ -128,6 +130,8 @@ predicate (datatype seq) FB_Backwards (pointer front, pointer back) { take F = Owned(front); assert(is_null(F.prev)); take Rest = Own_Backwards(B.prev, back, B, front, F); + assert(ptr_eq(B.prev, front) implies Rest == Seq_Nil{}); + assert(Rest == Seq_Nil{} implies ptr_eq(B.prev, front)); return Seq_Cons{ head: B.data, tail: snoc(Rest, F.data)}; } } From 13db1ebbeb4a8509b4fade61fdf884b616062dbb Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Thu, 25 Jul 2024 18:34:27 -0400 Subject: [PATCH 07/20] prove lemmas about predicates that go with proveable functions --- src/examples/Dbl_Queue/lemmas.c | 169 +++++++++++++++++++++++----- src/examples/Dbl_Queue/predicates.c | 154 +++++++++++++++++++++++++ 2 files changed, 292 insertions(+), 31 deletions(-) create mode 100644 src/examples/Dbl_Queue/predicates.c diff --git a/src/examples/Dbl_Queue/lemmas.c b/src/examples/Dbl_Queue/lemmas.c index 9372ebf2..bf1756d3 100644 --- a/src/examples/Dbl_Queue/lemmas.c +++ b/src/examples/Dbl_Queue/lemmas.c @@ -1,16 +1,74 @@ -#include "./WIP.c" +#include "./predicates.c" -void own_forwards_backwards(struct node *front, struct node *back) +void own_forwards_append_lemma(struct node *front, struct node *second_last, struct node *last) +/*@ + requires + take F = Owned(front); + take Second_last = Owned(second_last); + take Fwd = Own_Forwards(F.next, front, F, second_last, Second_last); + ptr_eq(Second_last.next, last); + take Last = Owned(last); + ptr_eq(Last.prev, second_last); + ensures + take F2 = Owned(front); + take Last2 = Owned(last); + take Fwd2 = Own_Forwards(F.next, front, F, last, Last2); + Fwd2 == snoc(Fwd, Last.data); + Last == Last2; + F2 == F; +@*/ +{ + /*@ unfold snoc(Seq_Nil{}, last->data); @*/ + /*@ unfold snoc(Fwd, last->data); @*/ + + if (front->next == second_last) { + return; + } else { + own_forwards_append_lemma(front->next, second_last, last); + return; + } +} + +void own_backwards_append_lemma(struct node *front, struct node *second_front, struct node *last) +/*@ + requires + take F = Owned(front); + take Second_front = Owned(second_front); + take Last = Owned(last); + take Bwd = Own_Backwards(Last.prev, last, Last, second_front, Second_front); + ptr_eq(Second_front.prev, front); + ptr_eq(F.next, second_front); + ensures + take F2 = Owned(front); + take Last2 = Owned(last); + take Bwd2 = Own_Backwards(Last.prev, last, Last, front, F2); + Bwd2 == snoc(Bwd, F.data); + Last == Last2; + F2 == F; +@*/ +{ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + /*@ unfold snoc(Bwd, front->data); @*/ + + if (last->prev == second_front) { + return; + } else { + own_backwards_append_lemma(front, second_front, last->prev); + return; + } +} + +void own_fwd_eq_bwd_lemma(struct node *front, struct node *back) /*@ requires + !ptr_eq(front, back); + take B = Owned(back); is_null(B.next); + !is_null(B.prev); + take F = Owned(front); - // ptr_eq(F.next,back) implies ptr_eq(B.prev, front); - // ptr_eq(B.prev, front) implies ptr_eq(F.next,back); - - // (is_null(F.next) && is_null(B.prev)) || (!is_null(F.next) && !is_null(B.prev)); + !is_null(F.next); - // is_null(F.prev); // doesn't work because of recursive call take Fwd = Own_Forwards(F.next, front, F, back, B); ensures take B2 = Owned(back); @@ -18,7 +76,7 @@ void own_forwards_backwards(struct node *front, struct node *back) take F2 = Owned(front); F == F2; take Bwd = Own_Backwards(B.prev, back, B, front, F); - Seq_Cons{head: F.data, tail: Fwd} == rev (Seq_Cons{head: B.data, tail: Bwd}); + rev(Seq_Cons{head: F.data, tail: Fwd}) == Seq_Cons{head: B.data, tail: Bwd}; @*/ { if (front == 0) { @@ -27,41 +85,90 @@ void own_forwards_backwards(struct node *front, struct node *back) if (front == back) { return; } else { - /*@ split_case(ptr_eq(front, back)); @*/ - /*@ split_case(is_null((*front).next)); @*/ - /*@ unfold rev(Seq_Cons {head: (*front).data, tail: Seq_Nil {}}); @*/ - /*@ unfold rev(Seq_Nil{}); @*/ - /*@ unfold snoc(Seq_Nil{}, (*front).data); @*/ if (front->next == 0) { return; } else { if (front->next == back) { - /*@ split_case(ptr_eq(front, back)); @*/ - /*@ split_case(is_null((*front).next)); @*/ - /*@ split_case(ptr_eq((*front).next, back)); @*/ - /*@ assert(ptr_eq((*back).prev, front)); @*/ + /*@ unfold rev(Seq_Nil{}); @*/ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + + /*@ unfold rev(Seq_Cons{head: back->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ + + /*@ unfold rev(Seq_Cons{head: front->data, tail: Seq_Cons{head: back->data, tail: Seq_Nil{}}}); @*/ + + /*@ unfold snoc(Seq_Cons{head: back->data, tail: Seq_Nil{}}, front->data); @*/ + return; } else { - /*@ assert(!is_null((*front).next)); @*/ - /*@ assert(!is_null((*(*front).next).next)); @*/ - /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ - /*@ assert(!is_null((*back).prev)); @*/ - // /*@ assert(!is_null((*(*back).prev).prev)); @*/ - own_forwards_backwards(front->next, back); - /*@ assert(!is_null((*front).next)); @*/ - /*@ assert(ptr_eq((*(*front).next).prev, front)); @*/ + + own_fwd_eq_bwd_lemma(front->next, back); + + own_backwards_append_lemma(front, front->next, back); + + + /*@ unfold rev(Seq_Cons{ head: front->data, tail: Fwd}); @*/ + /*@ unfold snoc(rev(Fwd), front->data); @*/ + + + return; + } + } + } + } +} - /*@ split_case(ptr_eq(front, back)); @*/ - /*@ split_case(is_null((*front).next)); @*/ - /*@ split_case(ptr_eq((*front).next, back)); @*/ +void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) +/*@ requires + !ptr_eq(front, back); - /*@ split_case(ptr_eq((*(*front).next).next, back)); @*/ + take B = Owned(back); + !is_null(B.prev); + + take F = Owned(front); + !is_null(F.next); + is_null(F.prev); - /*@ split_case(ptr_eq((*back).prev, front)); @*/ + take Bwd = Own_Backwards(B.prev, back, B, front, F); + ensures + take B2 = Owned(back); + B == B2; + take F2 = Owned(front); + F == F2; + take Fwd = Own_Forwards(F.next, front, F, back, B); + rev(Seq_Cons{head: B.data, tail: Bwd}) == Seq_Cons{head: F.data, tail: Fwd}; +@*/ +{ + if (back == 0) { + return; + } else { + if (front == back) { + return; + } else { + if (back->prev == 0) { + return; + } else { + if (back->prev == front) { + /*@ unfold rev(Seq_Nil{}); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ - // /*@ split_case(ptr_eq((*(*back).prev).prev, front)); @*/ + /*@ unfold rev(Seq_Cons{head: front->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + /*@ unfold rev(Seq_Cons{head: back->data, tail: Seq_Cons{head: front->data, tail: Seq_Nil{}}}); @*/ + + /*@ unfold snoc(Seq_Cons{head: front->data, tail: Seq_Nil{}}, back->data); @*/ + + return; + } else { + + own_bwd_eq_fwd_lemma(front, back->prev); + + own_forwards_append_lemma(front, back->prev, back); + + /*@ unfold rev(Seq_Cons{ head: back->data, tail: Bwd}); @*/ + /*@ unfold snoc(rev(Bwd), back->data); @*/ return; } } diff --git a/src/examples/Dbl_Queue/predicates.c b/src/examples/Dbl_Queue/predicates.c new file mode 100644 index 00000000..3d1cefed --- /dev/null +++ b/src/examples/Dbl_Queue/predicates.c @@ -0,0 +1,154 @@ +#include "../list_c_types.h" +#include "../list_cn_types.h" +#include "../list_hdtl.h" +#include "../list_rev.h" + +struct dbl_queue { + struct node* front; + struct node* back; +}; + +struct node { + int data; + struct node* prev; + struct node* next; +}; + +/*@ + +// This predicate owns the outer queue structure and +// asserts that the front and back pointers are either +// both null or both point to a node. It then takes +// ownership of the nodes in the list in the forwards +// direction through a call to FB_Forwards. It returns +// a sequence of integers representing the data in the queue. +predicate (datatype seq) Dbl_Queue_Forwards (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = FB_Forwards(L.front, L.back); + return inner; + } +} + + +// This predicate owns the front and back nodes in the queue, and then +// takes calls Own_Forwards to take ownership of the rest of the nodes +// in the queue. It asserts that the front node has a null prev pointer +// and that the back node has a null next pointer. It then returns a +// sequence of integers representing the data in the queue. +predicate (datatype seq) FB_Forwards (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + // Only one node in the list, so only one node to own + take F = Owned(front); + assert (is_null(F.next)); + assert (is_null(F.prev)); + return Seq_Cons {head: F.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + take Rest = Own_Forwards(F.next, front, F, back, B); + return Seq_Cons{ head: F.data, tail: Rest}; + } + } +} + +// This recursive predicate takes ownership of a node in the queue, +// and includes checks that the queue is properly doubly linked. It +// also asserts that any node owned in this predicate is not the front +// or the back node. It calls itself recursively, walking forwards until +// it reaches the last node in the list, which was already owned in the +// `FB_Forwards` predicate. The base case puts the back node into the sequence, +// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. +predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { + if (ptr_eq(p,b)) { + assert(ptr_eq(Back.prev, prev_pointer)); + return Seq_Cons{head: Back.data, tail: Seq_Nil{}}; + } else { + take n = Owned(p); + assert (ptr_eq(n.prev, prev_pointer)); + assert(ptr_eq(prev_node.next, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Forwards(n.next, p, n, b, Back); + return Seq_Cons{head: n.data, tail: Rest}; + } +} + +// This predicate owns the outer queue structure and +// asserts that the front and back pointers are either +// both null or both point to a node. It then takes +// ownership of the nodes in the list in the backwards +// direction through a call to FB_Backwards. It returns +// a sequence of integers representing the data in the queue +// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Forwards. +predicate (datatype seq) Dbl_Queue_Backwards (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = FB_Backwards(L.front, L.back); + return inner; + } +} + +// This predicate owns the front and back nodes in the queue, and then +// takes calls Own_Backwards to take ownership of the rest of the nodes +// in the queue. It asserts that the front node has a null prev pointer +// and that the back node has a null next pointer. It then returns a +// sequence of integers representing the data in the queue BACKWARDS. +predicate (datatype seq) FB_Backwards (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + take B = Owned(back); + assert (is_null(B.next)); + assert (is_null(B.prev)); + return Seq_Cons {head: B.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + take Rest = Own_Backwards(B.prev, back, B, front, F); + return Seq_Cons{ head: B.data, tail: Rest}; + } + } +} + +// This recursive predicate takes ownership of a node in the queue, +// and includes checks that the queue is properly doubly linked. It +// also asserts that any node owned in this predicate is not the front +// or the back node. It calls itself recursively, walking backwards until +// it reaches the first node in the list, which was already owned in the +// `FB_Backwards` predicate. The base case puts the front node into the sequence, +// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. +// Note that the front is put in the back because this sequence is backwards. +predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { + if (ptr_eq(p,f)) { + assert(ptr_eq(Front.next, next_pointer)); + return Seq_Cons{head: Front.data, tail: Seq_Nil{}}; + } else { + take n = Owned(p); + assert (ptr_eq(n.next, next_pointer)); + assert(ptr_eq(next_node.prev, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Backwards(n.prev, p, n, f, Front); + return Seq_Cons{head: n.data, tail: Rest}; + } +} +@*/ \ No newline at end of file From 235e4f335dacc9fa50a46c413cd366047b44d920 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Thu, 25 Jul 2024 19:39:08 -0400 Subject: [PATCH 08/20] prove everything --- src/examples/Dbl_Queue/WIP.c | 421 ---------------------------- src/examples/Dbl_Queue/functions.c | 167 +++++++++++ src/examples/Dbl_Queue/lemmas.c | 100 +++++++ src/examples/Dbl_Queue/predicates.c | 6 + 4 files changed, 273 insertions(+), 421 deletions(-) delete mode 100644 src/examples/Dbl_Queue/WIP.c create mode 100644 src/examples/Dbl_Queue/functions.c diff --git a/src/examples/Dbl_Queue/WIP.c b/src/examples/Dbl_Queue/WIP.c deleted file mode 100644 index a40ca6c3..00000000 --- a/src/examples/Dbl_Queue/WIP.c +++ /dev/null @@ -1,421 +0,0 @@ -#include "../list_c_types.h" -#include "../list_cn_types.h" -#include "../list_hdtl.h" -#include "../list_rev.h" - -struct dbl_queue { - struct node* front; - struct node* back; -}; - -struct node { - int data; - struct node* prev; - struct node* next; -}; - -/*@ - -// This predicate owns the outer queue structure and -// asserts that the front and back pointers are either -// both null or both point to a node. It then takes -// ownership of the nodes in the list in the forwards -// direction through a call to FB_Forwards. It returns -// a sequence of integers representing the data in the queue. -predicate (datatype seq) Dbl_Queue_Forwards (pointer l) { - if (is_null(l)) { - return Seq_Nil{}; - } - else { - take L = Owned(l); - assert ( (is_null(L.front) && is_null(L.back)) - || (!is_null(L.front) && !is_null(L.back))); - take inner = FB_Forwards(L.front, L.back); - return inner; - } -} - - -// This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Forwards to take ownership of the rest of the nodes -// in the queue. It asserts that the front node has a null prev pointer -// and that the back node has a null next pointer. It then returns a -// sequence of integers representing the data in the queue. -predicate (datatype seq) FB_Forwards (pointer front, pointer back) { - if (is_null(front)) { - return Seq_Nil{}; - } else { - if (ptr_eq(front, back)) { - // Only one node in the list, so only one node to own - take F = Owned(front); - assert (is_null(F.next)); - assert (is_null(F.prev)); - return Seq_Cons {head: F.data, tail: Seq_Nil{}}; - } else { - take B = Owned(back); - assert (is_null(B.next)); - take F = Owned(front); - assert(is_null(F.prev)); - take Rest = Own_Forwards(F.next, front, F, back, B); - return Seq_Cons{ head: F.data, tail: Rest}; - } - } -} - -// This recursive predicate takes ownership of a node in the queue, -// and includes checks that the queue is properly doubly linked. It -// also asserts that any node owned in this predicate is not the front -// or the back node. It calls itself recursively, walking forwards until -// it reaches the last node in the list, which was already owned in the -// `FB_Forwards` predicate. The base case puts the back node into the sequence, -// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { - if (ptr_eq(p,b)) { - assert(ptr_eq(Back.prev, prev_pointer)); - return Seq_Cons{head: Back.data, tail: Seq_Nil{}}; - } else { - take n = Owned(p); - assert (ptr_eq(n.prev, prev_pointer)); - assert(ptr_eq(prev_node.next, p)); - assert(!is_null(n.next)); - assert(!is_null(n.prev)); - take Rest = Own_Forwards(n.next, p, n, b, Back); - return Seq_Cons{head: n.data, tail: Rest}; - } -} - -// This predicate owns the outer queue structure and -// asserts that the front and back pointers are either -// both null or both point to a node. It then takes -// ownership of the nodes in the list in the backwards -// direction through a call to FB_Backwards. It returns -// a sequence of integers representing the data in the queue -// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Forwards. -predicate (datatype seq) Dbl_Queue_Backwards (pointer l) { - if (is_null(l)) { - return Seq_Nil{}; - } - else { - take L = Owned(l); - assert ( (is_null(L.front) && is_null(L.back)) - || (!is_null(L.front) && !is_null(L.back))); - take inner = FB_Backwards(L.front, L.back); - return inner; - } -} - -// This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Backwards to take ownership of the rest of the nodes -// in the queue. It asserts that the front node has a null prev pointer -// and that the back node has a null next pointer. It then returns a -// sequence of integers representing the data in the queue BACKWARDS. -predicate (datatype seq) FB_Backwards (pointer front, pointer back) { - if (is_null(front)) { - return Seq_Nil{}; - } else { - if (ptr_eq(front, back)) { - take B = Owned(back); - assert (is_null(B.next)); - assert (is_null(B.prev)); - return Seq_Cons {head: B.data, tail: Seq_Nil{}}; - } else { - take B = Owned(back); - assert (is_null(B.next)); - take F = Owned(front); - assert(is_null(F.prev)); - take Rest = Own_Backwards(B.prev, back, B, front, F); - return Seq_Cons{ head: B.data, tail: Rest}; - } - } -} - -// This recursive predicate takes ownership of a node in the queue, -// and includes checks that the queue is properly doubly linked. It -// also asserts that any node owned in this predicate is not the front -// or the back node. It calls itself recursively, walking backwards until -// it reaches the first node in the list, which was already owned in the -// `FB_Backwards` predicate. The base case puts the front node into the sequence, -// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -// Note that the front is put in the back because this sequence is backwards. -predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { - if (ptr_eq(p,f)) { - assert(ptr_eq(Front.next, next_pointer)); - return Seq_Cons{head: Front.data, tail: Seq_Nil{}}; - } else { - take n = Owned(p); - assert (ptr_eq(n.next, next_pointer)); - assert(ptr_eq(next_node.prev, p)); - assert(!is_null(n.next)); - assert(!is_null(n.prev)); - take Rest = Own_Backwards(n.prev, p, n, f, Front); - return Seq_Cons{head: n.data, tail: Rest}; - } -} -@*/ - -extern struct dbl_queue *malloc_dbl_queue(); -/*@ spec malloc_dbl_queue(); - requires true; - ensures take u = Block(return); - !ptr_eq(return,NULL); -@*/ - -extern void free_dbl_queue (struct dbl_queue *p); -/*@ spec free_dbl_queue(pointer p); - requires take u = Block(p); - ensures true; -@*/ - -extern struct node *malloc_node(); -/*@ spec malloc_node(); - requires true; - ensures take u = Block(return); - !is_null(return); -@*/ - -extern void free_node (struct node *p); -/*@ spec free_node(pointer p); - requires take u = Block(p); - ensures true; -@*/ - -struct dbl_queue *empty_dbl_queue() -/*@ ensures take ret = Dbl_Queue_Forwards(return); - ret == Seq_Nil{}; -@*/ -{ - struct dbl_queue *q = malloc_dbl_queue(); - q->front = 0; - q->back = 0; - return q; -} - -// // Given a dbl queue pointer, inserts a new node -// // to the front of the list -// void push_front (struct dbl_queue* q, int element) -// /*@ requires (!is_null(q)); -// take Before = Dbl_Queue_Forwards(q); -// ensures take After = Dbl_Queue_Forwards(q); -// After == Seq_Cons{head: element, tail: Before}; -// @*/ -// { -// struct node *new_node = malloc_node(); -// new_node->data = element; -// new_node->next = q->front; -// new_node->prev = 0; -// /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ - -// if (q->front != 0) { -// /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ -// q->front->prev = new_node; -// q->front = new_node; - -// } else { -// // in this case, the queue is empty -// q->back = new_node; -// q->front = new_node; -// } -// } - - -// int pop_front (struct dbl_queue* q) -// /*@ requires (!is_null(q)); -// take Before = Dbl_Queue_Forwards(q); -// Before != Seq_Nil{}; -// ensures take After = Dbl_Queue_Forwards(q); -// After == tl(Before); -// hd(Before) == return; -// @*/ -// { -// if (q->front == 0){ -// // impossible case from preconditions -// return 0; -// } else { -// // /*@ split_case is_null((*q).front); @*/ -// // /*@ apply empty_queue_seq_nil(q); @*/ -// // /*@ assert(Before != Seq_Nil{} implies !is_null((*q).front); @*/ -// // /*@ assert(!is_null((*q).front)); @*/ -// if (q->front == q->back) { // singleton list case -// int data = q->front->data; -// free_node(q->front); -// q->front = 0; -// q->back = 0; -// return data; - -// } else { -// /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ -// struct node *front = q->front; -// int data = front->data; -// front->next->prev = 0; -// q->front = front->next; -// free_node(front); - -// /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ -// return data; -// } -// } -// } - -// // Given a dbl queue pointer, inserts a new node -// // to the back of the list -// void push_back (struct dbl_queue* q, int element) -// /*@ requires (!is_null(q)); -// take Before = Dbl_Queue_Backwards(q); -// ensures take After = Dbl_Queue_Backwards(q); -// After == Seq_Cons{head: element, tail: Before}; -// // Before == snoc(After, element); // reverse??? -// @*/ -// { -// struct node *new_node = malloc_node(); -// new_node->data = element; -// new_node->next = 0; -// new_node->prev = q->back; -// /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ - -// if (q->back != 0) { -// /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ -// q->back->next = new_node; -// q->back = new_node; -// return; - -// } else { -// // in this case, the queue is empty -// q->back = new_node; -// q->front = new_node; -// return; -// } -// } - -// int pop_back (struct dbl_queue* q) -// /*@ requires (!is_null(q)); -// take Before = Dbl_Queue_Backwards(q); -// Before != Seq_Nil{}; -// ensures take After = Dbl_Queue_Backwards(q); -// After == tl(Before); -// hd(Before) == return; -// @*/ -// { -// if (q->front == 0){ -// // impossible case from preconditions -// return 0; -// } else { -// if (q->front == q->back) { // singleton list case -// int data = q->back->data; -// free_node(q->back); -// q->front = 0; -// q->back = 0; -// return data; - -// } else { -// /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ -// struct node *back = q->back; -// int data = back->data; -// back->prev->next = 0; -// q->back = back->prev; -// free_node(back); - -// /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ -// return data; -// } -// } -// } - - -// // void forwards_eq_backwards(struct dbl_queue *q) -// // /*@ -// // requires take for1 = Dbl_Queue_Forwards(q); -// // take back1 = Dbl_Queue_Backwards(q); -// // ensures take for2 = Dbl_Queue_Forwards(q); -// // take back2 = Dbl_Queue_Backwards(q); -// // for1 == for2; -// // back1 == back2; -// // for1 == rev(back1); -// // rev(for1) == back1; -// // @*/ -// // { -// // if (q == 0) -// // { -// // /*@ unfold rev(for1); @*/ -// // /*@ unfold rev(back1); @*/ -// // return; -// // } -// // } - -// // void switch_direction(struct dbl_queue *q) -// // /*@ -// // requires take forwards = Dbl_Queue_Forwards(q); -// // ensures take backwards = Dbl_Queue_Backwards(q); -// // // for1 == for2; -// // // back1 == back2; -// // // for1 == rev(back1); -// // // rev(for1) == back1; -// // @*/ -// // { -// // if (q == 0) -// // { -// // return; -// // } else { -// // if (q->front == 0) { -// // /*@ assert(is_null((*q).back)); @*/ -// // return; -// // } -// // else if (q->front == q->back){ -// // return; -// // } else { -// // forwards_eq_backwards(q); -// // // switch_direction(); -// // return; -// // } -// // } -// // } - -// // void switch_direction(struct node *front, struct node *back) -// // /*@ -// // requires take forwards = FB_Forwards(front, back); -// // ensures take backwards = FB_Backwards(front, back); -// // // for1 == for2; -// // // back1 == back2; -// // // for1 == rev(back1); -// // // rev(for1) == back1; -// // @*/ -// // { -// // if (front == 0) { -// // return; -// // } -// // else if (front == back){ -// // return; -// // } else { -// // /*@ split_case(is_null(front)); @*/ -// // /*@ split_case(is_null(back)); @*/ -// // /*@ split_case(ptr_eq(front,back)); @*/ - -// // switch_direction(front->next, back); -// // return; -// // } -// // } - -// // void switch_direction(struct node *front, struct node *back) -// // /*@ -// // requires take forwards = FB_Forwards(front, back); -// // ensures take backwards = FB_Backwards(front, back); -// // // for1 == for2; -// // // back1 == back2; -// // // for1 == rev(back1); -// // // rev(for1) == back1; -// // @*/ -// // { -// // if (front == 0) { -// // return; -// // } -// // else if (front == back){ -// // return; -// // } else { -// // /*@ split_case(is_null(front)); @*/ -// // /*@ split_case(is_null(back)); @*/ -// // /*@ split_case(ptr_eq(front,back)); @*/ - -// // switch_direction(front->next, back); -// // return; -// // } -// // } - diff --git a/src/examples/Dbl_Queue/functions.c b/src/examples/Dbl_Queue/functions.c new file mode 100644 index 00000000..d06c351f --- /dev/null +++ b/src/examples/Dbl_Queue/functions.c @@ -0,0 +1,167 @@ +#include "./predicates.c" +extern struct dbl_queue *malloc_dbl_queue(); +/*@ spec malloc_dbl_queue(); + requires true; + ensures take u = Block(return); + !ptr_eq(return,NULL); +@*/ + +extern void free_dbl_queue (struct dbl_queue *p); +/*@ spec free_dbl_queue(pointer p); + requires take u = Block(p); + ensures true; +@*/ + +extern struct node *malloc_node(); +/*@ spec malloc_node(); + requires true; + ensures take u = Block(return); + !is_null(return); +@*/ + +extern void free_node (struct node *p); +/*@ spec free_node(pointer p); + requires take u = Block(p); + ensures true; +@*/ + +struct dbl_queue *empty_dbl_queue() +/*@ ensures take ret = Dbl_Queue_Forwards(return); + ret == Seq_Nil{}; +@*/ +{ + struct dbl_queue *q = malloc_dbl_queue(); + q->front = 0; + q->back = 0; + return q; +} + +// Given a dbl queue pointer, inserts a new node +// to the front of the list +void push_front (struct dbl_queue* q, int element) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Forwards(q); + ensures take After = Dbl_Queue_Forwards(q); + After == Seq_Cons{head: element, tail: Before}; +@*/ +{ + struct node *new_node = malloc_node(); + new_node->data = element; + new_node->next = q->front; + new_node->prev = 0; + /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ + + if (q->front != 0) { + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + q->front->prev = new_node; + q->front = new_node; + + } else { + // in this case, the queue is empty + q->back = new_node; + q->front = new_node; + } +} + + +int pop_front (struct dbl_queue* q) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Forwards(q); + Before != Seq_Nil{}; + ensures take After = Dbl_Queue_Forwards(q); + After == tl(Before); + hd(Before) == return; +@*/ +{ + if (q->front == 0){ + // impossible case from preconditions + return 0; + } else { + // /*@ split_case is_null((*q).front); @*/ + // /*@ apply empty_queue_seq_nil(q); @*/ + // /*@ assert(Before != Seq_Nil{} implies !is_null((*q).front); @*/ + // /*@ assert(!is_null((*q).front)); @*/ + if (q->front == q->back) { // singleton list case + int data = q->front->data; + free_node(q->front); + q->front = 0; + q->back = 0; + return data; + + } else { + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + struct node *front = q->front; + int data = front->data; + front->next->prev = 0; + q->front = front->next; + free_node(front); + + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + return data; + } + } +} + +// Given a dbl queue pointer, inserts a new node +// to the back of the list +void push_back (struct dbl_queue* q, int element) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Backwards(q); + ensures take After = Dbl_Queue_Backwards(q); + After == Seq_Cons{head: element, tail: Before}; + // Before == snoc(After, element); // reverse??? +@*/ +{ + struct node *new_node = malloc_node(); + new_node->data = element; + new_node->next = 0; + new_node->prev = q->back; + /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ + + if (q->back != 0) { + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + q->back->next = new_node; + q->back = new_node; + return; + + } else { + // in this case, the queue is empty + q->back = new_node; + q->front = new_node; + return; + } +} + +int pop_back (struct dbl_queue* q) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Backwards(q); + Before != Seq_Nil{}; + ensures take After = Dbl_Queue_Backwards(q); + After == tl(Before); + hd(Before) == return; +@*/ +{ + if (q->front == 0){ + // impossible case from preconditions + return 0; + } else { + if (q->front == q->back) { // singleton list case + int data = q->back->data; + free_node(q->back); + q->front = 0; + q->back = 0; + return data; + + } else { + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + struct node *back = q->back; + int data = back->data; + back->prev->next = 0; + q->back = back->prev; + free_node(back); + + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + return data; + } + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/lemmas.c b/src/examples/Dbl_Queue/lemmas.c index bf1756d3..9f439045 100644 --- a/src/examples/Dbl_Queue/lemmas.c +++ b/src/examples/Dbl_Queue/lemmas.c @@ -174,4 +174,104 @@ void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) } } } +} + +void FB_Forwards_eq_backwards(struct node *front, struct node *back) +/*@ requires + (is_null(front) && is_null(back)) || (!is_null(front) && !is_null(back)); + take Q_Fwd = FB_Forwards(front, back); + ensures + take Q_Bwd = FB_Backwards(front, back); + rev(Q_Fwd) == Q_Bwd; +@*/ +{ + /*@ unfold rev(Seq_Nil{}); @*/ + if (front == 0) { + return; + } else { + if (front == back) { + /*@ unfold rev(Seq_Cons{head: back->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ + return; + } else { + if (front->next == back) + { + /*@ unfold rev(Seq_Cons{head: back->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ + /*@ unfold rev(Q_Fwd); @*/ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + /*@ unfold snoc(Seq_Cons{head: back->data, tail: Seq_Nil{}}, front->data); @*/ + + return; + } + else { + own_fwd_eq_bwd_lemma(front, back); + return; + } + } + } +} + +void FB_Backwards_eq_Forwards(struct node *front, struct node *back) +/*@ requires + (is_null(front) && is_null(back)) || (!is_null(front) && !is_null(back)); + take Q_Bwd = FB_Backwards(front, back); + ensures + take Q_Fwd = FB_Forwards(front, back); + rev(Q_Bwd) == Q_Fwd; +@*/ +{ + /*@ unfold rev(Seq_Nil{}); @*/ + if (back == 0) { + return; + } else { + if (front == back) { + /*@ unfold rev(Seq_Cons{head: front->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + return; + } else { + if (back->prev == front) + { + /*@ unfold rev(Seq_Cons{head: front->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + /*@ unfold rev(Q_Bwd); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ + /*@ unfold snoc(Seq_Cons{head: front->data, tail: Seq_Nil{}}, back->data); @*/ + + return; + } + else { + own_bwd_eq_fwd_lemma(front, back); + return; + } + } + } +} + +void Dbl_Queue_Forwards_eq_backwards(struct dbl_queue *q) +/*@ requires take Q_Fwd = Dbl_Queue_Forwards(q); + ensures take Q_Bwd = Dbl_Queue_Backwards(q); + rev(Q_Fwd) == Q_Bwd; +@*/ +{ + /*@ unfold rev(Seq_Nil{}); @*/ + if (q == 0) { + return; + } else { + FB_Forwards_eq_backwards(q->front, q->back); + } +} + +void Dbl_Queue_Backwards_eq_Forwards(struct dbl_queue *q) +/*@ requires take Q_Bwd = Dbl_Queue_Backwards(q); + ensures take Q_Fwd = Dbl_Queue_Forwards(q); + rev(Q_Bwd) == Q_Fwd; +@*/ +{ + /*@ unfold rev(Seq_Nil{}); @*/ + if (q == 0) { + return; + } else { + FB_Backwards_eq_Forwards(q->front, q->back); + } } \ No newline at end of file diff --git a/src/examples/Dbl_Queue/predicates.c b/src/examples/Dbl_Queue/predicates.c index 3d1cefed..53ab8824 100644 --- a/src/examples/Dbl_Queue/predicates.c +++ b/src/examples/Dbl_Queue/predicates.c @@ -56,6 +56,8 @@ predicate (datatype seq) FB_Forwards (pointer front, pointer back) { assert (is_null(B.next)); take F = Owned(front); assert(is_null(F.prev)); + assert(!is_null(F.next)); + assert(!is_null(B.prev)); take Rest = Own_Forwards(F.next, front, F, back, B); return Seq_Cons{ head: F.data, tail: Rest}; } @@ -72,6 +74,7 @@ predicate (datatype seq) FB_Forwards (pointer front, pointer back) { predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { if (ptr_eq(p,b)) { assert(ptr_eq(Back.prev, prev_pointer)); + assert(ptr_eq(prev_node.next, p)); return Seq_Cons{head: Back.data, tail: Seq_Nil{}}; } else { take n = Owned(p); @@ -123,6 +126,8 @@ predicate (datatype seq) FB_Backwards (pointer front, pointer back) { assert (is_null(B.next)); take F = Owned(front); assert(is_null(F.prev)); + assert(!is_null(F.next)); + assert(!is_null(B.prev)); take Rest = Own_Backwards(B.prev, back, B, front, F); return Seq_Cons{ head: B.data, tail: Rest}; } @@ -140,6 +145,7 @@ predicate (datatype seq) FB_Backwards (pointer front, pointer back) { predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { if (ptr_eq(p,f)) { assert(ptr_eq(Front.next, next_pointer)); + assert(ptr_eq(next_node.prev, p)); return Seq_Cons{head: Front.data, tail: Seq_Nil{}}; } else { take n = Owned(p); From 32f702050045442ecf045e29eb42c077c2f8d1b8 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Thu, 25 Jul 2024 19:40:49 -0400 Subject: [PATCH 09/20] delete old files --- src/examples/Dbl_Queue/lemmas_other.c | 144 ----------------------- src/examples/Dbl_Queue/preds_other.c | 163 -------------------------- 2 files changed, 307 deletions(-) delete mode 100644 src/examples/Dbl_Queue/lemmas_other.c delete mode 100644 src/examples/Dbl_Queue/preds_other.c diff --git a/src/examples/Dbl_Queue/lemmas_other.c b/src/examples/Dbl_Queue/lemmas_other.c deleted file mode 100644 index 2d941deb..00000000 --- a/src/examples/Dbl_Queue/lemmas_other.c +++ /dev/null @@ -1,144 +0,0 @@ -#include "./preds_other.c" - -void own_forwards_append_lemma(struct node *front, struct node *second_last, struct node *last) -/*@ - requires - take F = Owned(front); - take Second_last = Owned(second_last); - take Fwd = Own_Forwards(F.next, front, F, second_last, Second_last); - ptr_eq(Second_last.next, last); - take Last = Owned(last); - ptr_eq(Last.prev, second_last); - ensures - take F2 = Owned(front); - take Last2 = Owned(last); - take Fwd2 = Own_Forwards(F.next, front, F, last, Last2); - Fwd2 == snoc(Fwd, Second_last.data); - Last == Last2; - F2 == F; -@*/ -{ - /*@ unfold snoc(Seq_Nil{}, (*second_last).data); @*/ - /*@ unfold snoc(Fwd, (*second_last).data); @*/ - - if (front->next == second_last) { - return; - } else { - own_forwards_append_lemma(front->next, second_last, last); - return; - } -} - -void own_backwards_append_lemma(struct node *front, struct node *second_front, struct node *last) -/*@ - requires - take F = Owned(front); - take Second_front = Owned(second_front); - take Last = Owned(last); - take Bwd = Own_Backwards(Last.prev, last, Last, second_front, Second_front); - ptr_eq(Second_front.prev, front); - ptr_eq(F.next, second_front); - ensures - take F2 = Owned(front); - take Last2 = Owned(last); - take Bwd2 = Own_Backwards(Last.prev, last, Last, front, F2); - Bwd2 == snoc(Bwd, Second_front.data); - Last == Last2; - F2 == F; - ptr_eq(F.next, second_front); - {front} unchanged; {second_front} unchanged; {last} unchanged; - -@*/ -{ - /*@ unfold snoc(Seq_Nil{}, (*second_front).data); @*/ - /*@ unfold snoc(Bwd, (*second_front).data); @*/ - - if (last->prev == second_front) { - return; - } else { - own_backwards_append_lemma(front, second_front, last->prev); - return; - } -} - -void own_fwd_eq_bwd_lemma(struct node *front, struct node *back) -/*@ requires - !ptr_eq(front, back); - - take B = Owned(back); - is_null(B.next); - !is_null(B.prev); - - take F = Owned(front); - !is_null(F.next); - - take Fwd = Own_Forwards(F.next, front, F, back, B); - ptr_eq(F.next, back) implies Fwd == Seq_Nil{}; - - Fwd == Seq_Nil{} implies ptr_eq(F.next, back); - - ensures - take B2 = Owned(back); - B == B2; - take F2 = Owned(front); - F == F2; - take Bwd = Own_Backwards(B.prev, back, B, front, F); - rev(Fwd) == Bwd; -@*/ -{ - /*@ unfold rev(Seq_Nil{}); @*/ - if (front->next == 0) { - return; - } else { - if (front->next == back) { - return; - } else { - /*@ split_case(ptr_eq(front->next->next, back)); @*/ - own_fwd_eq_bwd_lemma(front->next, back); - own_backwards_append_lemma(front, front->next, back); - /*@ unfold rev(Fwd); @*/ - return; - } - } -} - -void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) -/*@ requires - !ptr_eq(front, back); - - take B = Owned(back); - !is_null(B.prev); - - take F = Owned(front); - !is_null(F.next); - is_null(F.prev); - - take Bwd = Own_Backwards(B.prev, back, B, front, F); - - ptr_eq(B.prev, front) implies Bwd == Seq_Nil{}; - Bwd == Seq_Nil{} implies ptr_eq(B.prev, front); - - ensures - take B2 = Owned(back); - B == B2; - take F2 = Owned(front); - F == F2; - take Fwd = Own_Forwards(F.next, front, F, back, B); - rev(Bwd) == Fwd; -@*/ -{ - /*@ unfold rev(Seq_Nil{}); @*/ - if (back->prev == 0) { - return; - } else { - if (back->prev == front) { - return; - } else { - /*@ split_case(ptr_eq(back->prev->prev, front)); @*/ - own_bwd_eq_fwd_lemma(front, back->prev); - own_forwards_append_lemma(front, back->prev, back); - /*@ unfold rev(Bwd); @*/ - return; - } - } -} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/preds_other.c b/src/examples/Dbl_Queue/preds_other.c deleted file mode 100644 index b2c1f5ec..00000000 --- a/src/examples/Dbl_Queue/preds_other.c +++ /dev/null @@ -1,163 +0,0 @@ -#include "../list_c_types.h" -#include "../list_cn_types.h" -#include "../list_hdtl.h" -#include "../list_rev.h" - -struct dbl_queue { - struct node* front; - struct node* back; -}; - -struct node { - int data; - struct node* prev; - struct node* next; -}; - -/*@ - -// This predicate owns the outer queue structure and -// asserts that the front and back pointers are either -// both null or both point to a node. It then takes -// ownership of the nodes in the list in the forwards -// direction through a call to FB_Forwards. It returns -// a sequence of integers representing the data in the queue. -predicate (datatype seq) Dbl_Queue_Forwards (pointer l) { - if (is_null(l)) { - return Seq_Nil{}; - } - else { - take L = Owned(l); - assert ( (is_null(L.front) && is_null(L.back)) - || (!is_null(L.front) && !is_null(L.back))); - take inner = FB_Forwards(L.front, L.back); - return inner; - } -} - - -// This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Forwards to take ownership of the rest of the nodes -// in the queue. It asserts that the front node has a null prev pointer -// and that the back node has a null next pointer. It then returns a -// sequence of integers representing the data in the queue. -predicate (datatype seq) FB_Forwards (pointer front, pointer back) { - if (is_null(front)) { - return Seq_Nil{}; - } else { - if (ptr_eq(front, back)) { - // Only one node in the list, so only one node to own - take F = Owned(front); - assert (is_null(F.next)); - assert (is_null(F.prev)); - return Seq_Cons {head: F.data, tail: Seq_Nil{}}; - } else { - take B = Owned(back); //idea: own LAST - assert (is_null(B.next)); - take F = Owned(front); - assert(is_null(F.prev)); - take Rest = Own_Forwards(F.next, front, F, back, B); - assert(ptr_eq(F.next, back) implies Rest == Seq_Nil{}); - assert(Rest == Seq_Nil{} implies ptr_eq(F.next, back)); - return Seq_Cons{ head: F.data, tail: snoc(Rest, B.data)}; - } - } -} - -// This recursive predicate takes ownership of a node in the queue, -// and includes checks that the queue is properly doubly linked. It -// also asserts that any node owned in this predicate is not the front -// or the back node. It calls itself recursively, walking forwards until -// it reaches the last node in the list, which was already owned in the -// `FB_Forwards` predicate. The base case puts the back node into the sequence, -// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { - if (ptr_eq(p,b)) { - assert(ptr_eq(Back.prev, prev_pointer)); - assert(ptr_eq(prev_node.next, b)); - assert(ptr_eq(p,b)); - return Seq_Nil{}; - } else { - take n = Owned(p); - assert (ptr_eq(n.prev, prev_pointer)); - assert(ptr_eq(prev_node.next, p)); - assert(!is_null(n.next)); - assert(!is_null(n.prev)); - assert(!ptr_eq(p,b)); - take Rest = Own_Forwards(n.next, p, n, b, Back); - assert(!(Seq_Cons{head: n.data, tail: Rest} == Seq_Nil{})); - return Seq_Cons{head: n.data, tail: Rest}; - } -} - -// This predicate owns the outer queue structure and -// asserts that the front and back pointers are either -// both null or both point to a node. It then takes -// ownership of the nodes in the list in the backwards -// direction through a call to FB_Backwards. It returns -// a sequence of integers representing the data in the queue -// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Forwards. -predicate (datatype seq) Dbl_Queue_Backwards (pointer l) { - if (is_null(l)) { - return Seq_Nil{}; - } - else { - take L = Owned(l); - assert ( (is_null(L.front) && is_null(L.back)) - || (!is_null(L.front) && !is_null(L.back))); - take inner = FB_Backwards(L.front, L.back); - return inner; - } -} - -// This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Backwards to take ownership of the rest of the nodes -// in the queue. It asserts that the front node has a null prev pointer -// and that the back node has a null next pointer. It then returns a -// sequence of integers representing the data in the queue BACKWARDS. -predicate (datatype seq) FB_Backwards (pointer front, pointer back) { - if (is_null(front)) { - return Seq_Nil{}; - } else { - if (ptr_eq(front, back)) { - take B = Owned(back); - assert (is_null(B.next)); - assert (is_null(B.prev)); - return Seq_Cons {head: B.data, tail: Seq_Nil{}}; - } else { - take B = Owned(back); - assert (is_null(B.next)); - take F = Owned(front); - assert(is_null(F.prev)); - take Rest = Own_Backwards(B.prev, back, B, front, F); - assert(ptr_eq(B.prev, front) implies Rest == Seq_Nil{}); - assert(Rest == Seq_Nil{} implies ptr_eq(B.prev, front)); - return Seq_Cons{ head: B.data, tail: snoc(Rest, F.data)}; - } - } -} - -// This recursive predicate takes ownership of a node in the queue, -// and includes checks that the queue is properly doubly linked. It -// also asserts that any node owned in this predicate is not the front -// or the back node. It calls itself recursively, walking backwards until -// it reaches the first node in the list, which was already owned in the -// `FB_Backwards` predicate. The base case puts the front node into the sequence, -// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -// Note that the front is put in the back because this sequence is backwards. -predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { - if (ptr_eq(p,f)) { - assert(ptr_eq(Front.next, next_pointer)); - assert(ptr_eq(next_node.prev, f)); - return Seq_Nil{}; - } else { - take n = Owned(p); - assert (ptr_eq(n.next, next_pointer)); - assert(ptr_eq(next_node.prev, p)); - assert(!is_null(n.next)); - assert(!is_null(n.prev)); - take Rest = Own_Backwards(n.prev, p, n, f, Front); - return Seq_Cons{head: n.data, tail: Rest}; - } -} -@*/ \ No newline at end of file From 519fe8bed858d8109e259ba01dbef4064498441f Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Thu, 25 Jul 2024 19:55:56 -0400 Subject: [PATCH 10/20] make empty ensure return is not null --- src/examples/Dbl_Queue/functions.c | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/examples/Dbl_Queue/functions.c b/src/examples/Dbl_Queue/functions.c index d06c351f..2764f61e 100644 --- a/src/examples/Dbl_Queue/functions.c +++ b/src/examples/Dbl_Queue/functions.c @@ -26,8 +26,10 @@ extern void free_node (struct node *p); @*/ struct dbl_queue *empty_dbl_queue() -/*@ ensures take ret = Dbl_Queue_Forwards(return); - ret == Seq_Nil{}; +/*@ ensures + !is_null(return); + take ret = Dbl_Queue_Forwards(return); + ret == Seq_Nil{}; @*/ { struct dbl_queue *q = malloc_dbl_queue(); From 35ef8e2da41c47bb39f435a4fe2b4e94dc7bde54 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Fri, 26 Jul 2024 09:57:56 -0400 Subject: [PATCH 11/20] prove impossible case in pop --- src/examples/Dbl_Queue/functions.c | 84 ++++++++++++++---------------- 1 file changed, 38 insertions(+), 46 deletions(-) diff --git a/src/examples/Dbl_Queue/functions.c b/src/examples/Dbl_Queue/functions.c index 2764f61e..f96274c9 100644 --- a/src/examples/Dbl_Queue/functions.c +++ b/src/examples/Dbl_Queue/functions.c @@ -75,32 +75,26 @@ int pop_front (struct dbl_queue* q) hd(Before) == return; @*/ { - if (q->front == 0){ - // impossible case from preconditions - return 0; + /*@ split_case(is_null(q->back)); @*/ + /*@ assert(!is_null(q->front)); @*/ + + if (q->front == q->back) { // singleton list case + int data = q->front->data; + free_node(q->front); + q->front = 0; + q->back = 0; + return data; + } else { - // /*@ split_case is_null((*q).front); @*/ - // /*@ apply empty_queue_seq_nil(q); @*/ - // /*@ assert(Before != Seq_Nil{} implies !is_null((*q).front); @*/ - // /*@ assert(!is_null((*q).front)); @*/ - if (q->front == q->back) { // singleton list case - int data = q->front->data; - free_node(q->front); - q->front = 0; - q->back = 0; - return data; - - } else { - /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ - struct node *front = q->front; - int data = front->data; - front->next->prev = 0; - q->front = front->next; - free_node(front); - - /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ - return data; - } + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + struct node *front = q->front; + int data = front->data; + front->next->prev = 0; + q->front = front->next; + free_node(front); + + /*@ split_case(ptr_eq((*(*q).front).next, (*q).back)); @*/ + return data; } } @@ -143,27 +137,25 @@ int pop_back (struct dbl_queue* q) hd(Before) == return; @*/ { - if (q->front == 0){ - // impossible case from preconditions - return 0; + /*@ split_case(is_null(q->back)); @*/ + /*@ assert(!is_null(q->front)); @*/ + + if (q->front == q->back) { // singleton list case + int data = q->back->data; + free_node(q->back); + q->front = 0; + q->back = 0; + return data; + } else { - if (q->front == q->back) { // singleton list case - int data = q->back->data; - free_node(q->back); - q->front = 0; - q->back = 0; - return data; - - } else { - /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ - struct node *back = q->back; - int data = back->data; - back->prev->next = 0; - q->back = back->prev; - free_node(back); - - /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ - return data; - } + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + struct node *back = q->back; + int data = back->data; + back->prev->next = 0; + q->back = back->prev; + free_node(back); + + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + return data; } } \ No newline at end of file From 99bd4c3c48ae76c490cfe71fc55937d0c4d59486 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Fri, 26 Jul 2024 10:23:53 -0400 Subject: [PATCH 12/20] work on main function --- src/examples/Dbl_Queue/main.c | 92 +++++++++++++++++++++++++++++++++++ 1 file changed, 92 insertions(+) create mode 100644 src/examples/Dbl_Queue/main.c diff --git a/src/examples/Dbl_Queue/main.c b/src/examples/Dbl_Queue/main.c new file mode 100644 index 00000000..caf3382a --- /dev/null +++ b/src/examples/Dbl_Queue/main.c @@ -0,0 +1,92 @@ +// WIP, currently does not pass + +// #include "./predicates.c" +#include "./functions.c" +#include "./lemmas.c" +int main() +{ + struct dbl_queue *q = empty_dbl_queue(); + /*@ assert(!is_null(q)); @*/ + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + + + push_front(q, 1); + /*@ split_case(is_null(q)); @*/ + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(is_null(q->back)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + /*@ assert(ptr_eq(q->front, q->back)); @*/ + /*@ assert(q->front->data == 1i32); @*/ + /*@ assert(q->back->data == 1i32); @*/ + + + Dbl_Queue_Forwards_eq_backwards(q); + /*@ split_case(is_null(q)); @*/ + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(is_null(q->back)); @*/ + + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + /*@ assert(ptr_eq(q->front, q->back)); @*/ + // /*@ assert(q->front->data == 1i32); @*/ + // /*@ assert(q->back->data == 1i32); @*/ + + + push_back(q, 2); + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + // /*@ assert(q->front->data == 1i32); @*/ + // /*@ assert(q->back->data == 2i32); @*/ + /*@ assert(!ptr_eq(q->front, q->back)); @*/ + /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ + /*@ assert(ptr_eq(q->back->prev, q->front)); @*/ + // /*@ assert(q->front->data == 1i32); @*/ + // /*@ assert(q->back->data == 2i32); @*/ + + Dbl_Queue_Backwards_eq_Forwards(q); + push_front(q, 3); + + + /*@ split_case(is_null(q)); @*/ + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + /*@ assert(q->front->data == 3i32); @*/ + // /*@ assert(q->front->next->data == 1i32); @*/ + /*@ assert(q->back->data == 2i32); @*/ + + /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ + /*@ split_case(ptr_eq(q->front->next->next, q->back)); @*/ + /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ + + + + + int three = pop_front(q); + + + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(is_null(q->back)); @*/ + + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + + /*@ assert(!is_null(q)); @*/ + /*@ assert(!is_null(q->front)); @*/ + /*@ assert(!is_null(q->back)); @*/ + /*@ assert(q->front->data == 3i32); @*/ + /*@ assert(q->back->data == 2i32); @*/ + + Dbl_Queue_Forwards_eq_backwards(q); + /*@ split_case(is_null(q)); @*/ + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(is_null(q->back)); @*/ + + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + + /*@ unfold rev(Seq_Nil{}); @*/ + // /*@ assert(!is_null(q->front)); @*/ + + + int two = pop_back(q); + int one = pop_back(q); + free_dbl_queue(q); +} \ No newline at end of file From 0c1ef615ef63524177f18c0210c24ea9df696f62 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Fri, 26 Jul 2024 11:16:36 -0400 Subject: [PATCH 13/20] make names more intuitive --- src/examples/Dbl_Queue/functions.c | 18 +++--- src/examples/Dbl_Queue/lemmas.c | 94 +++++++++++++++-------------- src/examples/Dbl_Queue/predicates.c | 38 ++++++------ 3 files changed, 76 insertions(+), 74 deletions(-) diff --git a/src/examples/Dbl_Queue/functions.c b/src/examples/Dbl_Queue/functions.c index f96274c9..b7741126 100644 --- a/src/examples/Dbl_Queue/functions.c +++ b/src/examples/Dbl_Queue/functions.c @@ -28,7 +28,7 @@ extern void free_node (struct node *p); struct dbl_queue *empty_dbl_queue() /*@ ensures !is_null(return); - take ret = Dbl_Queue_Forwards(return); + take ret = Dbl_Queue_Fwd_At(return); ret == Seq_Nil{}; @*/ { @@ -42,8 +42,8 @@ struct dbl_queue *empty_dbl_queue() // to the front of the list void push_front (struct dbl_queue* q, int element) /*@ requires (!is_null(q)); - take Before = Dbl_Queue_Forwards(q); - ensures take After = Dbl_Queue_Forwards(q); + take Before = Dbl_Queue_Fwd_At(q); + ensures take After = Dbl_Queue_Fwd_At(q); After == Seq_Cons{head: element, tail: Before}; @*/ { @@ -68,9 +68,9 @@ void push_front (struct dbl_queue* q, int element) int pop_front (struct dbl_queue* q) /*@ requires (!is_null(q)); - take Before = Dbl_Queue_Forwards(q); + take Before = Dbl_Queue_Fwd_At(q); Before != Seq_Nil{}; - ensures take After = Dbl_Queue_Forwards(q); + ensures take After = Dbl_Queue_Fwd_At(q); After == tl(Before); hd(Before) == return; @*/ @@ -102,8 +102,8 @@ int pop_front (struct dbl_queue* q) // to the back of the list void push_back (struct dbl_queue* q, int element) /*@ requires (!is_null(q)); - take Before = Dbl_Queue_Backwards(q); - ensures take After = Dbl_Queue_Backwards(q); + take Before = Dbl_Queue_Bwd_At(q); + ensures take After = Dbl_Queue_Bwd_At(q); After == Seq_Cons{head: element, tail: Before}; // Before == snoc(After, element); // reverse??? @*/ @@ -130,9 +130,9 @@ void push_back (struct dbl_queue* q, int element) int pop_back (struct dbl_queue* q) /*@ requires (!is_null(q)); - take Before = Dbl_Queue_Backwards(q); + take Before = Dbl_Queue_Bwd_At(q); Before != Seq_Nil{}; - ensures take After = Dbl_Queue_Backwards(q); + ensures take After = Dbl_Queue_Bwd_At(q); After == tl(Before); hd(Before) == return; @*/ diff --git a/src/examples/Dbl_Queue/lemmas.c b/src/examples/Dbl_Queue/lemmas.c index 9f439045..ca00212f 100644 --- a/src/examples/Dbl_Queue/lemmas.c +++ b/src/examples/Dbl_Queue/lemmas.c @@ -1,18 +1,18 @@ #include "./predicates.c" -void own_forwards_append_lemma(struct node *front, struct node *second_last, struct node *last) +void Own_Inner_fwds_append_lemma(struct node *front, struct node *second_last, struct node *last) /*@ requires take F = Owned(front); take Second_last = Owned(second_last); - take Fwd = Own_Forwards(F.next, front, F, second_last, Second_last); + take Fwd = Own_Inner_Fwds(F.next, front, F, second_last, Second_last); ptr_eq(Second_last.next, last); take Last = Owned(last); ptr_eq(Last.prev, second_last); ensures take F2 = Owned(front); take Last2 = Owned(last); - take Fwd2 = Own_Forwards(F.next, front, F, last, Last2); + take Fwd2 = Own_Inner_Fwds(F.next, front, F, last, Last2); Fwd2 == snoc(Fwd, Last.data); Last == Last2; F2 == F; @@ -24,24 +24,24 @@ void own_forwards_append_lemma(struct node *front, struct node *second_last, str if (front->next == second_last) { return; } else { - own_forwards_append_lemma(front->next, second_last, last); + Own_Inner_fwds_append_lemma(front->next, second_last, last); return; } } -void own_backwards_append_lemma(struct node *front, struct node *second_front, struct node *last) +void Own_Inner_bwds_append_lemma(struct node *front, struct node *second_front, struct node *last) /*@ requires take F = Owned(front); take Second_front = Owned(second_front); take Last = Owned(last); - take Bwd = Own_Backwards(Last.prev, last, Last, second_front, Second_front); + take Bwd = Own_Inner_Bwds(Last.prev, last, Last, second_front, Second_front); ptr_eq(Second_front.prev, front); ptr_eq(F.next, second_front); ensures take F2 = Owned(front); take Last2 = Owned(last); - take Bwd2 = Own_Backwards(Last.prev, last, Last, front, F2); + take Bwd2 = Own_Inner_Bwds(Last.prev, last, Last, front, F2); Bwd2 == snoc(Bwd, F.data); Last == Last2; F2 == F; @@ -53,30 +53,30 @@ void own_backwards_append_lemma(struct node *front, struct node *second_front, s if (last->prev == second_front) { return; } else { - own_backwards_append_lemma(front, second_front, last->prev); + Own_Inner_bwds_append_lemma(front, second_front, last->prev); return; } } -void own_fwd_eq_bwd_lemma(struct node *front, struct node *back) +void Own_Inner_fwds_eq_bwd_lemma(struct node *front, struct node *back) /*@ requires - !ptr_eq(front, back); + !ptr_eq(front, back); - take B = Owned(back); - is_null(B.next); - !is_null(B.prev); - - take F = Owned(front); - !is_null(F.next); + take B = Owned(back); + is_null(B.next); + !is_null(B.prev); + + take F = Owned(front); + !is_null(F.next); - take Fwd = Own_Forwards(F.next, front, F, back, B); + take Fwd = Own_Inner_Fwds(F.next, front, F, back, B); ensures - take B2 = Owned(back); - B == B2; - take F2 = Owned(front); - F == F2; - take Bwd = Own_Backwards(B.prev, back, B, front, F); - rev(Seq_Cons{head: F.data, tail: Fwd}) == Seq_Cons{head: B.data, tail: Bwd}; + take B2 = Owned(back); + B == B2; + take F2 = Owned(front); + F == F2; + take Bwd = Own_Inner_Bwds(B.prev, back, B, front, F); + rev(Seq_Cons{head: F.data, tail: Fwd}) == Seq_Cons{head: B.data, tail: Bwd}; @*/ { if (front == 0) { @@ -102,9 +102,9 @@ void own_fwd_eq_bwd_lemma(struct node *front, struct node *back) return; } else { - own_fwd_eq_bwd_lemma(front->next, back); + Own_Inner_fwds_eq_bwd_lemma(front->next, back); - own_backwards_append_lemma(front, front->next, back); + Own_Inner_bwds_append_lemma(front, front->next, back); /*@ unfold rev(Seq_Cons{ head: front->data, tail: Fwd}); @*/ @@ -118,7 +118,7 @@ void own_fwd_eq_bwd_lemma(struct node *front, struct node *back) } } -void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) +void Own_Inner_bwds_eq_fwd_lemma(struct node *front, struct node *back) /*@ requires !ptr_eq(front, back); @@ -129,13 +129,13 @@ void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) !is_null(F.next); is_null(F.prev); - take Bwd = Own_Backwards(B.prev, back, B, front, F); + take Bwd = Own_Inner_Bwds(B.prev, back, B, front, F); ensures take B2 = Owned(back); B == B2; take F2 = Owned(front); F == F2; - take Fwd = Own_Forwards(F.next, front, F, back, B); + take Fwd = Own_Inner_Fwds(F.next, front, F, back, B); rev(Seq_Cons{head: B.data, tail: Bwd}) == Seq_Cons{head: F.data, tail: Fwd}; @*/ { @@ -162,9 +162,9 @@ void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) return; } else { - own_bwd_eq_fwd_lemma(front, back->prev); + Own_Inner_bwds_eq_fwd_lemma(front, back->prev); - own_forwards_append_lemma(front, back->prev, back); + Own_Inner_fwds_append_lemma(front, back->prev, back); /*@ unfold rev(Seq_Cons{ head: back->data, tail: Bwd}); @*/ @@ -176,12 +176,12 @@ void own_bwd_eq_fwd_lemma(struct node *front, struct node *back) } } -void FB_Forwards_eq_backwards(struct node *front, struct node *back) +void Own_Front_Back_fwds_eq_bwds_lemma(struct node *front, struct node *back) /*@ requires (is_null(front) && is_null(back)) || (!is_null(front) && !is_null(back)); - take Q_Fwd = FB_Forwards(front, back); + take Q_Fwd = Own_Front_Back_Fwds(front, back); ensures - take Q_Bwd = FB_Backwards(front, back); + take Q_Bwd = Own_Front_Back_Bwds(front, back); rev(Q_Fwd) == Q_Bwd; @*/ { @@ -205,19 +205,19 @@ void FB_Forwards_eq_backwards(struct node *front, struct node *back) return; } else { - own_fwd_eq_bwd_lemma(front, back); + Own_Inner_fwds_eq_bwd_lemma(front, back); return; } } } } -void FB_Backwards_eq_Forwards(struct node *front, struct node *back) +void Own_Front_Back_bwds_eq_fwds_lemma(struct node *front, struct node *back) /*@ requires (is_null(front) && is_null(back)) || (!is_null(front) && !is_null(back)); - take Q_Bwd = FB_Backwards(front, back); + take Q_Bwd = Own_Front_Back_Bwds(front, back); ensures - take Q_Fwd = FB_Forwards(front, back); + take Q_Fwd = Own_Front_Back_Fwds(front, back); rev(Q_Bwd) == Q_Fwd; @*/ { @@ -241,37 +241,39 @@ void FB_Backwards_eq_Forwards(struct node *front, struct node *back) return; } else { - own_bwd_eq_fwd_lemma(front, back); + Own_Inner_bwds_eq_fwd_lemma(front, back); return; } } } } -void Dbl_Queue_Forwards_eq_backwards(struct dbl_queue *q) -/*@ requires take Q_Fwd = Dbl_Queue_Forwards(q); - ensures take Q_Bwd = Dbl_Queue_Backwards(q); +void Dbl_Queue_Fwd_At_eq_Bwd_lemma(struct dbl_queue *q) +/*@ requires take Q_Fwd = Dbl_Queue_Fwd_At(q); + ensures take Q_Bwd = Dbl_Queue_Bwd_At(q); rev(Q_Fwd) == Q_Bwd; + {q} unchanged; @*/ { /*@ unfold rev(Seq_Nil{}); @*/ if (q == 0) { return; } else { - FB_Forwards_eq_backwards(q->front, q->back); + Own_Front_Back_fwds_eq_bwds_lemma(q->front, q->back); } } -void Dbl_Queue_Backwards_eq_Forwards(struct dbl_queue *q) -/*@ requires take Q_Bwd = Dbl_Queue_Backwards(q); - ensures take Q_Fwd = Dbl_Queue_Forwards(q); +void Dbl_Queue_Bwd_At_eq_Fwd_lemma(struct dbl_queue *q) +/*@ requires take Q_Bwd = Dbl_Queue_Bwd_At(q); + ensures take Q_Fwd = Dbl_Queue_Fwd_At(q); rev(Q_Bwd) == Q_Fwd; + {q} unchanged; @*/ { /*@ unfold rev(Seq_Nil{}); @*/ if (q == 0) { return; } else { - FB_Backwards_eq_Forwards(q->front, q->back); + Own_Front_Back_bwds_eq_fwds_lemma(q->front, q->back); } } \ No newline at end of file diff --git a/src/examples/Dbl_Queue/predicates.c b/src/examples/Dbl_Queue/predicates.c index 53ab8824..9bff56ae 100644 --- a/src/examples/Dbl_Queue/predicates.c +++ b/src/examples/Dbl_Queue/predicates.c @@ -20,9 +20,9 @@ struct node { // asserts that the front and back pointers are either // both null or both point to a node. It then takes // ownership of the nodes in the list in the forwards -// direction through a call to FB_Forwards. It returns +// direction through a call to Own_Front_Back_Fwds. It returns // a sequence of integers representing the data in the queue. -predicate (datatype seq) Dbl_Queue_Forwards (pointer l) { +predicate (datatype seq) Dbl_Queue_Fwd_At (pointer l) { if (is_null(l)) { return Seq_Nil{}; } @@ -30,18 +30,18 @@ predicate (datatype seq) Dbl_Queue_Forwards (pointer l) { take L = Owned(l); assert ( (is_null(L.front) && is_null(L.back)) || (!is_null(L.front) && !is_null(L.back))); - take inner = FB_Forwards(L.front, L.back); + take inner = Own_Front_Back_Fwds(L.front, L.back); return inner; } } // This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Forwards to take ownership of the rest of the nodes +// takes calls Own_Inner_Fwds to take ownership of the rest of the nodes // in the queue. It asserts that the front node has a null prev pointer // and that the back node has a null next pointer. It then returns a // sequence of integers representing the data in the queue. -predicate (datatype seq) FB_Forwards (pointer front, pointer back) { +predicate (datatype seq) Own_Front_Back_Fwds (pointer front, pointer back) { if (is_null(front)) { return Seq_Nil{}; } else { @@ -58,7 +58,7 @@ predicate (datatype seq) FB_Forwards (pointer front, pointer back) { assert(is_null(F.prev)); assert(!is_null(F.next)); assert(!is_null(B.prev)); - take Rest = Own_Forwards(F.next, front, F, back, B); + take Rest = Own_Inner_Fwds(F.next, front, F, back, B); return Seq_Cons{ head: F.data, tail: Rest}; } } @@ -69,9 +69,9 @@ predicate (datatype seq) FB_Forwards (pointer front, pointer back) { // also asserts that any node owned in this predicate is not the front // or the back node. It calls itself recursively, walking forwards until // it reaches the last node in the list, which was already owned in the -// `FB_Forwards` predicate. The base case puts the back node into the sequence, +// `Own_Front_Back_Fwds` predicate. The base case puts the back node into the sequence, // in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { +predicate (datatype seq) Own_Inner_Fwds(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { if (ptr_eq(p,b)) { assert(ptr_eq(Back.prev, prev_pointer)); assert(ptr_eq(prev_node.next, p)); @@ -82,7 +82,7 @@ predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct no assert(ptr_eq(prev_node.next, p)); assert(!is_null(n.next)); assert(!is_null(n.prev)); - take Rest = Own_Forwards(n.next, p, n, b, Back); + take Rest = Own_Inner_Fwds(n.next, p, n, b, Back); return Seq_Cons{head: n.data, tail: Rest}; } } @@ -91,10 +91,10 @@ predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct no // asserts that the front and back pointers are either // both null or both point to a node. It then takes // ownership of the nodes in the list in the backwards -// direction through a call to FB_Backwards. It returns +// direction through a call to Own_Front_Back_Bwds. It returns // a sequence of integers representing the data in the queue -// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Forwards. -predicate (datatype seq) Dbl_Queue_Backwards (pointer l) { +// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Fwd_At. +predicate (datatype seq) Dbl_Queue_Bwd_At (pointer l) { if (is_null(l)) { return Seq_Nil{}; } @@ -102,17 +102,17 @@ predicate (datatype seq) Dbl_Queue_Backwards (pointer l) { take L = Owned(l); assert ( (is_null(L.front) && is_null(L.back)) || (!is_null(L.front) && !is_null(L.back))); - take inner = FB_Backwards(L.front, L.back); + take inner = Own_Front_Back_Bwds(L.front, L.back); return inner; } } // This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Backwards to take ownership of the rest of the nodes +// takes calls Own_Inner_Bwds to take ownership of the rest of the nodes // in the queue. It asserts that the front node has a null prev pointer // and that the back node has a null next pointer. It then returns a // sequence of integers representing the data in the queue BACKWARDS. -predicate (datatype seq) FB_Backwards (pointer front, pointer back) { +predicate (datatype seq) Own_Front_Back_Bwds (pointer front, pointer back) { if (is_null(front)) { return Seq_Nil{}; } else { @@ -128,7 +128,7 @@ predicate (datatype seq) FB_Backwards (pointer front, pointer back) { assert(is_null(F.prev)); assert(!is_null(F.next)); assert(!is_null(B.prev)); - take Rest = Own_Backwards(B.prev, back, B, front, F); + take Rest = Own_Inner_Bwds(B.prev, back, B, front, F); return Seq_Cons{ head: B.data, tail: Rest}; } } @@ -139,10 +139,10 @@ predicate (datatype seq) FB_Backwards (pointer front, pointer back) { // also asserts that any node owned in this predicate is not the front // or the back node. It calls itself recursively, walking backwards until // it reaches the first node in the list, which was already owned in the -// `FB_Backwards` predicate. The base case puts the front node into the sequence, +// `Own_Front_Back_Bwds` predicate. The base case puts the front node into the sequence, // in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. // Note that the front is put in the back because this sequence is backwards. -predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { +predicate (datatype seq) Own_Inner_Bwds(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { if (ptr_eq(p,f)) { assert(ptr_eq(Front.next, next_pointer)); assert(ptr_eq(next_node.prev, p)); @@ -153,7 +153,7 @@ predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct n assert(ptr_eq(next_node.prev, p)); assert(!is_null(n.next)); assert(!is_null(n.prev)); - take Rest = Own_Backwards(n.prev, p, n, f, Front); + take Rest = Own_Inner_Bwds(n.prev, p, n, f, Front); return Seq_Cons{head: n.data, tail: Rest}; } } From fda7f2b531997f4dd4696e37d233047f20d4d013 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Fri, 26 Jul 2024 11:19:06 -0400 Subject: [PATCH 14/20] fix names in main --- src/examples/Dbl_Queue/main.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/examples/Dbl_Queue/main.c b/src/examples/Dbl_Queue/main.c index caf3382a..22bde2bd 100644 --- a/src/examples/Dbl_Queue/main.c +++ b/src/examples/Dbl_Queue/main.c @@ -21,7 +21,7 @@ int main() /*@ assert(q->back->data == 1i32); @*/ - Dbl_Queue_Forwards_eq_backwards(q); + Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); /*@ split_case(is_null(q)); @*/ /*@ split_case(is_null(q->front)); @*/ /*@ split_case(is_null(q->back)); @*/ @@ -43,7 +43,7 @@ int main() // /*@ assert(q->front->data == 1i32); @*/ // /*@ assert(q->back->data == 2i32); @*/ - Dbl_Queue_Backwards_eq_Forwards(q); + Dbl_Queue_Bwd_At_eq_Fwd_lemma(q); push_front(q, 3); @@ -75,7 +75,7 @@ int main() /*@ assert(q->front->data == 3i32); @*/ /*@ assert(q->back->data == 2i32); @*/ - Dbl_Queue_Forwards_eq_backwards(q); + Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); /*@ split_case(is_null(q)); @*/ /*@ split_case(is_null(q->front)); @*/ /*@ split_case(is_null(q->back)); @*/ From 75969a65c778bbf05e0d692f3d4aca1f62db379b Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Mon, 29 Jul 2024 10:41:09 -0400 Subject: [PATCH 15/20] add more examples --- src/examples/Dbl_Queue/lemmas.c | 2 +- src/examples/Dbl_Queue/main.c | 200 ++++++++++++++++++++++++-------- 2 files changed, 152 insertions(+), 50 deletions(-) diff --git a/src/examples/Dbl_Queue/lemmas.c b/src/examples/Dbl_Queue/lemmas.c index ca00212f..b38e7af7 100644 --- a/src/examples/Dbl_Queue/lemmas.c +++ b/src/examples/Dbl_Queue/lemmas.c @@ -1,4 +1,4 @@ -#include "./predicates.c" +// #include "./predicates.c" void Own_Inner_fwds_append_lemma(struct node *front, struct node *second_last, struct node *last) /*@ diff --git a/src/examples/Dbl_Queue/main.c b/src/examples/Dbl_Queue/main.c index 22bde2bd..98fccec5 100644 --- a/src/examples/Dbl_Queue/main.c +++ b/src/examples/Dbl_Queue/main.c @@ -12,81 +12,183 @@ int main() push_front(q, 1); - /*@ split_case(is_null(q)); @*/ - /*@ split_case(is_null(q->front)); @*/ - /*@ split_case(is_null(q->back)); @*/ - /*@ split_case(ptr_eq(q->front, q->back)); @*/ - /*@ assert(ptr_eq(q->front, q->back)); @*/ - /*@ assert(q->front->data == 1i32); @*/ - /*@ assert(q->back->data == 1i32); @*/ + // /*@ split_case(is_null(q)); @*/ + // /*@ split_case(is_null(q->front)); @*/ + // /*@ split_case(is_null(q->back)); @*/ + // /*@ split_case(ptr_eq(q->front, q->back)); @*/ + // /*@ assert(ptr_eq(q->front, q->back)); @*/ + // /*@ assert(q->front->data == 1i32); @*/ + // /*@ assert(q->back->data == 1i32); @*/ - Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); - /*@ split_case(is_null(q)); @*/ - /*@ split_case(is_null(q->front)); @*/ - /*@ split_case(is_null(q->back)); @*/ + // Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + // /*@ split_case(is_null(q)); @*/ + // /*@ split_case(is_null(q->front)); @*/ + // /*@ split_case(is_null(q->back)); @*/ - /*@ split_case(ptr_eq(q->front, q->back)); @*/ - /*@ assert(ptr_eq(q->front, q->back)); @*/ - // /*@ assert(q->front->data == 1i32); @*/ - // /*@ assert(q->back->data == 1i32); @*/ + // /*@ split_case(ptr_eq(q->front, q->back)); @*/ + // /*@ assert(ptr_eq(q->front, q->back)); @*/ + // // /*@ assert(q->front->data == 1i32); @*/ + // // /*@ assert(q->back->data == 1i32); @*/ - push_back(q, 2); - /*@ split_case(is_null(q->front)); @*/ - /*@ split_case(ptr_eq(q->front, q->back)); @*/ - // /*@ assert(q->front->data == 1i32); @*/ - // /*@ assert(q->back->data == 2i32); @*/ - /*@ assert(!ptr_eq(q->front, q->back)); @*/ - /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ - /*@ assert(ptr_eq(q->back->prev, q->front)); @*/ - // /*@ assert(q->front->data == 1i32); @*/ - // /*@ assert(q->back->data == 2i32); @*/ + // push_back(q, 2); + // /*@ split_case(is_null(q->front)); @*/ + // /*@ split_case(ptr_eq(q->front, q->back)); @*/ + // // /*@ assert(q->front->data == 1i32); @*/ + // // /*@ assert(q->back->data == 2i32); @*/ + // /*@ assert(!ptr_eq(q->front, q->back)); @*/ + // /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ + // /*@ assert(ptr_eq(q->back->prev, q->front)); @*/ + // // /*@ assert(q->front->data == 1i32); @*/ + // // /*@ assert(q->back->data == 2i32); @*/ - Dbl_Queue_Bwd_At_eq_Fwd_lemma(q); - push_front(q, 3); + // Dbl_Queue_Bwd_At_eq_Fwd_lemma(q); + // push_front(q, 3); - /*@ split_case(is_null(q)); @*/ - /*@ split_case(is_null(q->front)); @*/ - /*@ split_case(ptr_eq(q->front, q->back)); @*/ - /*@ assert(q->front->data == 3i32); @*/ - // /*@ assert(q->front->next->data == 1i32); @*/ - /*@ assert(q->back->data == 2i32); @*/ + // /*@ split_case(is_null(q)); @*/ + // /*@ split_case(is_null(q->front)); @*/ + // /*@ split_case(ptr_eq(q->front, q->back)); @*/ + // /*@ assert(q->front->data == 3i32); @*/ + // // /*@ assert(q->front->next->data == 1i32); @*/ + // /*@ assert(q->back->data == 2i32); @*/ - /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ - /*@ split_case(ptr_eq(q->front->next->next, q->back)); @*/ - /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ + // /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ + // /*@ split_case(ptr_eq(q->front->next->next, q->back)); @*/ + // /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ - int three = pop_front(q); + // int three = pop_front(q); - /*@ split_case(is_null(q->front)); @*/ - /*@ split_case(is_null(q->back)); @*/ + // /*@ split_case(is_null(q->front)); @*/ + // /*@ split_case(is_null(q->back)); @*/ + + // /*@ split_case(ptr_eq(q->front, q->back)); @*/ + + // /*@ assert(!is_null(q)); @*/ + // /*@ assert(!is_null(q->front)); @*/ + // /*@ assert(!is_null(q->back)); @*/ + // /*@ assert(q->front->data == 3i32); @*/ + // /*@ assert(q->back->data == 2i32); @*/ + + // Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + // /*@ split_case(is_null(q)); @*/ + // /*@ split_case(is_null(q->front)); @*/ + // /*@ split_case(is_null(q->back)); @*/ + // /*@ split_case(ptr_eq(q->front, q->back)); @*/ + + // /*@ unfold rev(Seq_Nil{}); @*/ + // // /*@ assert(!is_null(q->front)); @*/ + + + // int two = pop_back(q); + + + + int one = pop_front(q); + /*@ assert(one == 1i32); @*/ + /*@ split_case(is_null(q->front)); @*/ /*@ split_case(ptr_eq(q->front, q->back)); @*/ + free_dbl_queue(q); +} - /*@ assert(!is_null(q)); @*/ - /*@ assert(!is_null(q->front)); @*/ - /*@ assert(!is_null(q->back)); @*/ - /*@ assert(q->front->data == 3i32); @*/ - /*@ assert(q->back->data == 2i32); @*/ +void ex_front() +{ + struct dbl_queue *q = empty_dbl_queue(); + push_front(q, 1); + + int one = pop_front(q); + /*@ assert(one == 1i32); @*/ - Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); - /*@ split_case(is_null(q)); @*/ /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + free_dbl_queue(q); +} + +void ex_back() +{ + struct dbl_queue *q = empty_dbl_queue(); + /*@ split_case(is_null(q->back)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + + push_back(q, 1); + + int one = pop_back(q); + /*@ assert(one == 1i32); @*/ + /*@ split_case(is_null(q->front)); @*/ /*@ split_case(ptr_eq(q->front, q->back)); @*/ + + free_dbl_queue(q); +} + +// void ex_switch() +// { +// struct dbl_queue *q = empty_dbl_queue(); +// push_front(q, 1); +// /*@ split_case(is_null(q->front)); @*/ +// /*@ split_case(is_null(q->back)); @*/ +// /*@ split_case(ptr_eq(q->front, q->back)); @*/ +// /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ +// /*@ split_case(is_null(q)); @*/ +// /*@ unfold rev(Seq_Nil{}); @*/ +// /*@ assert(q->front->data == 1i32); @*/ +// /*@ assert(!is_null(q->front)); @*/ +// /*@ assert(!is_null(q->back)); @*/ + +// Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); +// /*@ assert(!is_null(q->front)); @*/ +// /*@ assert(!is_null(q->back)); @*/ + +// /*@ assert(q->back->data == 1i32); @*/ + +// /*@ unfold rev(Seq_Cons{head: 1i32, tail: Seq_Nil{}}); @*/ +// /*@ unfold rev(Seq_Nil{}); @*/ +// /*@ split_case(is_null(q)); @*/ +// /*@ split_case(is_null(q->front)); @*/ +// /*@ split_case(is_null(q->back)); @*/ +// // /*@ split_case(ptr_eq(q->front, q->back->prev)); @*/ + + +// /*@ split_case(ptr_eq(q->front, q->back)); @*/ +// int one = pop_back(q); +// /*@ assert(one == 1i32); @*/ + +// /*@ split_case(is_null(q->front)); @*/ +// /*@ split_case(ptr_eq(q->front, q->back)); @*/ +// free_dbl_queue(q); +// } + +void ex_switch() +{ + struct dbl_queue *q = empty_dbl_queue(); + push_front(q, 1); + Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + push_back(q, 2); + int two = pop_back(q); + int one = pop_back(q); + /*@ assert(one == 1i32); @*/ + /*@ assert(two == 2i32); @*/ - /*@ unfold rev(Seq_Nil{}); @*/ - // /*@ assert(!is_null(q->front)); @*/ + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + free_dbl_queue(q); +} - int two = pop_back(q); +void foo() +{ + struct dbl_queue *q = empty_dbl_queue(); + push_front(q, 1); + + Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + int one = pop_back(q); free_dbl_queue(q); } \ No newline at end of file From a29f57cb403843b978dec25442e72b2049488400 Mon Sep 17 00:00:00 2001 From: Christopher Pulte Date: Mon, 29 Jul 2024 16:33:10 +0100 Subject: [PATCH 16/20] Revert "recategorise now-working examples". Sorry! This reverts commit 2d93a9bf7162659b9253c1efff31d0674a365cfb. --- .../{working/00134.c => broken/error-proof/00134.err1.c} | 0 .../{working/00135.c => broken/error-proof/00135.err1.c} | 0 .../{working/long_type.c => broken/error-proof/long_type_err_1.c} | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename src/example-archive/c-testsuite/{working/00134.c => broken/error-proof/00134.err1.c} (100%) rename src/example-archive/c-testsuite/{working/00135.c => broken/error-proof/00135.err1.c} (100%) rename src/example-archive/simple-examples/{working/long_type.c => broken/error-proof/long_type_err_1.c} (100%) diff --git a/src/example-archive/c-testsuite/working/00134.c b/src/example-archive/c-testsuite/broken/error-proof/00134.err1.c similarity index 100% rename from src/example-archive/c-testsuite/working/00134.c rename to src/example-archive/c-testsuite/broken/error-proof/00134.err1.c diff --git a/src/example-archive/c-testsuite/working/00135.c b/src/example-archive/c-testsuite/broken/error-proof/00135.err1.c similarity index 100% rename from src/example-archive/c-testsuite/working/00135.c rename to src/example-archive/c-testsuite/broken/error-proof/00135.err1.c diff --git a/src/example-archive/simple-examples/working/long_type.c b/src/example-archive/simple-examples/broken/error-proof/long_type_err_1.c similarity index 100% rename from src/example-archive/simple-examples/working/long_type.c rename to src/example-archive/simple-examples/broken/error-proof/long_type_err_1.c From 21904beb0d110a0abc47991e84a45ba1ef153396 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Mon, 29 Jul 2024 11:53:08 -0400 Subject: [PATCH 17/20] finish examples --- src/examples/Dbl_Queue/main.c | 178 ++++++++-------------------------- 1 file changed, 43 insertions(+), 135 deletions(-) diff --git a/src/examples/Dbl_Queue/main.c b/src/examples/Dbl_Queue/main.c index 98fccec5..c2b0a4a1 100644 --- a/src/examples/Dbl_Queue/main.c +++ b/src/examples/Dbl_Queue/main.c @@ -1,101 +1,5 @@ -// WIP, currently does not pass - -// #include "./predicates.c" #include "./functions.c" #include "./lemmas.c" -int main() -{ - struct dbl_queue *q = empty_dbl_queue(); - /*@ assert(!is_null(q)); @*/ - /*@ split_case(is_null(q->front)); @*/ - /*@ split_case(ptr_eq(q->front, q->back)); @*/ - - - push_front(q, 1); - // /*@ split_case(is_null(q)); @*/ - // /*@ split_case(is_null(q->front)); @*/ - // /*@ split_case(is_null(q->back)); @*/ - // /*@ split_case(ptr_eq(q->front, q->back)); @*/ - // /*@ assert(ptr_eq(q->front, q->back)); @*/ - // /*@ assert(q->front->data == 1i32); @*/ - // /*@ assert(q->back->data == 1i32); @*/ - - - // Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); - // /*@ split_case(is_null(q)); @*/ - // /*@ split_case(is_null(q->front)); @*/ - // /*@ split_case(is_null(q->back)); @*/ - - // /*@ split_case(ptr_eq(q->front, q->back)); @*/ - // /*@ assert(ptr_eq(q->front, q->back)); @*/ - // // /*@ assert(q->front->data == 1i32); @*/ - // // /*@ assert(q->back->data == 1i32); @*/ - - - // push_back(q, 2); - // /*@ split_case(is_null(q->front)); @*/ - // /*@ split_case(ptr_eq(q->front, q->back)); @*/ - // // /*@ assert(q->front->data == 1i32); @*/ - // // /*@ assert(q->back->data == 2i32); @*/ - // /*@ assert(!ptr_eq(q->front, q->back)); @*/ - // /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ - // /*@ assert(ptr_eq(q->back->prev, q->front)); @*/ - // // /*@ assert(q->front->data == 1i32); @*/ - // // /*@ assert(q->back->data == 2i32); @*/ - - // Dbl_Queue_Bwd_At_eq_Fwd_lemma(q); - // push_front(q, 3); - - - // /*@ split_case(is_null(q)); @*/ - // /*@ split_case(is_null(q->front)); @*/ - // /*@ split_case(ptr_eq(q->front, q->back)); @*/ - // /*@ assert(q->front->data == 3i32); @*/ - // // /*@ assert(q->front->next->data == 1i32); @*/ - // /*@ assert(q->back->data == 2i32); @*/ - - // /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ - // /*@ split_case(ptr_eq(q->front->next->next, q->back)); @*/ - // /*@ split_case(ptr_eq(q->back->prev, q->front)); @*/ - - - - - // int three = pop_front(q); - - - // /*@ split_case(is_null(q->front)); @*/ - // /*@ split_case(is_null(q->back)); @*/ - - // /*@ split_case(ptr_eq(q->front, q->back)); @*/ - - // /*@ assert(!is_null(q)); @*/ - // /*@ assert(!is_null(q->front)); @*/ - // /*@ assert(!is_null(q->back)); @*/ - // /*@ assert(q->front->data == 3i32); @*/ - // /*@ assert(q->back->data == 2i32); @*/ - - // Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); - // /*@ split_case(is_null(q)); @*/ - // /*@ split_case(is_null(q->front)); @*/ - // /*@ split_case(is_null(q->back)); @*/ - - // /*@ split_case(ptr_eq(q->front, q->back)); @*/ - - // /*@ unfold rev(Seq_Nil{}); @*/ - // // /*@ assert(!is_null(q->front)); @*/ - - - // int two = pop_back(q); - - - - int one = pop_front(q); - /*@ assert(one == 1i32); @*/ - /*@ split_case(is_null(q->front)); @*/ - /*@ split_case(ptr_eq(q->front, q->back)); @*/ - free_dbl_queue(q); -} void ex_front() { @@ -128,48 +32,14 @@ void ex_back() free_dbl_queue(q); } -// void ex_switch() -// { -// struct dbl_queue *q = empty_dbl_queue(); -// push_front(q, 1); -// /*@ split_case(is_null(q->front)); @*/ -// /*@ split_case(is_null(q->back)); @*/ -// /*@ split_case(ptr_eq(q->front, q->back)); @*/ -// /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ -// /*@ split_case(is_null(q)); @*/ -// /*@ unfold rev(Seq_Nil{}); @*/ -// /*@ assert(q->front->data == 1i32); @*/ -// /*@ assert(!is_null(q->front)); @*/ -// /*@ assert(!is_null(q->back)); @*/ - -// Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); -// /*@ assert(!is_null(q->front)); @*/ -// /*@ assert(!is_null(q->back)); @*/ - -// /*@ assert(q->back->data == 1i32); @*/ - -// /*@ unfold rev(Seq_Cons{head: 1i32, tail: Seq_Nil{}}); @*/ -// /*@ unfold rev(Seq_Nil{}); @*/ -// /*@ split_case(is_null(q)); @*/ -// /*@ split_case(is_null(q->front)); @*/ -// /*@ split_case(is_null(q->back)); @*/ -// // /*@ split_case(ptr_eq(q->front, q->back->prev)); @*/ - - -// /*@ split_case(ptr_eq(q->front, q->back)); @*/ -// int one = pop_back(q); -// /*@ assert(one == 1i32); @*/ - -// /*@ split_case(is_null(q->front)); @*/ -// /*@ split_case(ptr_eq(q->front, q->back)); @*/ -// free_dbl_queue(q); -// } - -void ex_switch() +void ex_switch1() { struct dbl_queue *q = empty_dbl_queue(); push_front(q, 1); Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + /*@ unfold rev(Seq_Cons{ head: 1i32, tail: Seq_Nil{} }); @*/ + /*@ unfold rev(Seq_Nil{}); @*/ + /*@ unfold snoc(Seq_Nil{}, 1i32); @*/ push_back(q, 2); int two = pop_back(q); int one = pop_back(q); @@ -182,13 +52,51 @@ void ex_switch() } -void foo() +void ex_switch2() { struct dbl_queue *q = empty_dbl_queue(); push_front(q, 1); Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + /*@ unfold rev(Seq_Cons{ head: 1i32, tail: Seq_Nil{} }); @*/ + /*@ unfold rev(Seq_Nil{}); @*/ + /*@ unfold snoc(Seq_Nil{}, 1i32); @*/ + int one = pop_back(q); + /*@ assert(one == 1i32); @*/ + + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + free_dbl_queue(q); +} + +void ex_switch3() +{ + struct dbl_queue *q = empty_dbl_queue(); + push_front(q, 1); + Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + /*@ unfold rev(Seq_Cons{ head: 1i32, tail: Seq_Nil{} }); @*/ + /*@ unfold rev(Seq_Nil{}); @*/ + /*@ unfold snoc(Seq_Nil{}, 1i32); @*/ + + push_back(q, 2); + Dbl_Queue_Bwd_At_eq_Fwd_lemma(q); //rev(2,1) == (1,2) + /*@ unfold rev(Seq_Cons{ head: 2i32, tail: Seq_Cons{head: 1i32, tail: Seq_Nil{}}}); @*/ + /*@ unfold snoc(Seq_Nil{}, 2i32); @*/ + /*@ unfold snoc(Seq_Cons{head: 1i32, tail: Seq_Nil{}}, 2i32); @*/ + + int one = pop_front(q); + + Dbl_Queue_Fwd_At_eq_Bwd_lemma(q); + /*@ unfold rev(Seq_Cons{ head: 2i32, tail: Seq_Nil{} }); @*/ + + int two = pop_back(q); + + /*@ assert(one == 1i32); @*/ + /*@ assert(two == 2i32); @*/ + + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ free_dbl_queue(q); } \ No newline at end of file From a0f866aa298249ed135e3c225e5145917d6f4bb0 Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Tue, 30 Jul 2024 14:33:42 -0400 Subject: [PATCH 18/20] add double ended queues to tutorial --- src/examples/Dbl_Queue/append_lemmas.h | 57 ++++++ src/examples/Dbl_Queue/c_types.h | 10 ++ src/examples/Dbl_Queue/empty.c | 16 ++ .../Dbl_Queue/{functions.c => functions.h} | 27 --- src/examples/Dbl_Queue/fwds_append_lemma.h | 30 ++++ src/examples/Dbl_Queue/headers.h | 9 + .../Dbl_Queue/inner_fwd_eq_bwd_lemma.h | 62 +++++++ src/examples/Dbl_Queue/{lemmas.c => lemmas.h} | 0 src/examples/Dbl_Queue/main.broken.c | 12 ++ src/examples/Dbl_Queue/malloc_free.h | 25 +++ .../Dbl_Queue/own_FB_fwds_eq_bwds_lemma.h | 36 ++++ src/examples/Dbl_Queue/pop_back.c | 38 ++++ src/examples/Dbl_Queue/pop_front.c | 33 ++++ .../Dbl_Queue/pop_front_orig.broken.c | 21 +++ src/examples/Dbl_Queue/predicates.c | 160 ----------------- src/examples/Dbl_Queue/preds_bwd.h | 53 ++++++ src/examples/Dbl_Queue/preds_fwd.h | 54 ++++++ src/examples/Dbl_Queue/push_back.c | 35 ++++ src/examples/Dbl_Queue/push_front.c | 28 +++ .../Dbl_Queue/push_front_orig.broken.c | 19 ++ .../Dbl_Queue/{main.c => verified_examples.c} | 5 +- src/tutorial.adoc | 168 ++++++++++++++++++ 22 files changed, 709 insertions(+), 189 deletions(-) create mode 100644 src/examples/Dbl_Queue/append_lemmas.h create mode 100644 src/examples/Dbl_Queue/c_types.h create mode 100644 src/examples/Dbl_Queue/empty.c rename src/examples/Dbl_Queue/{functions.c => functions.h} (84%) create mode 100644 src/examples/Dbl_Queue/fwds_append_lemma.h create mode 100644 src/examples/Dbl_Queue/headers.h create mode 100644 src/examples/Dbl_Queue/inner_fwd_eq_bwd_lemma.h rename src/examples/Dbl_Queue/{lemmas.c => lemmas.h} (100%) create mode 100644 src/examples/Dbl_Queue/main.broken.c create mode 100644 src/examples/Dbl_Queue/malloc_free.h create mode 100644 src/examples/Dbl_Queue/own_FB_fwds_eq_bwds_lemma.h create mode 100644 src/examples/Dbl_Queue/pop_back.c create mode 100644 src/examples/Dbl_Queue/pop_front.c create mode 100644 src/examples/Dbl_Queue/pop_front_orig.broken.c delete mode 100644 src/examples/Dbl_Queue/predicates.c create mode 100644 src/examples/Dbl_Queue/preds_bwd.h create mode 100644 src/examples/Dbl_Queue/preds_fwd.h create mode 100644 src/examples/Dbl_Queue/push_back.c create mode 100644 src/examples/Dbl_Queue/push_front.c create mode 100644 src/examples/Dbl_Queue/push_front_orig.broken.c rename src/examples/Dbl_Queue/{main.c => verified_examples.c} (97%) diff --git a/src/examples/Dbl_Queue/append_lemmas.h b/src/examples/Dbl_Queue/append_lemmas.h new file mode 100644 index 00000000..a1e63b38 --- /dev/null +++ b/src/examples/Dbl_Queue/append_lemmas.h @@ -0,0 +1,57 @@ +void Own_Inner_fwds_append_lemma(struct node *front, struct node *second_last, struct node *last) +/*@ + requires + take F = Owned(front); + take Second_last = Owned(second_last); + take Fwd = Own_Inner_Fwds(F.next, front, F, second_last, Second_last); + ptr_eq(Second_last.next, last); + take Last = Owned(last); + ptr_eq(Last.prev, second_last); + ensures + take F2 = Owned(front); + take Last2 = Owned(last); + take Fwd2 = Own_Inner_Fwds(F.next, front, F, last, Last2); + Fwd2 == snoc(Fwd, Last.data); + Last == Last2; + F2 == F; +@*/ +{ + /*@ unfold snoc(Seq_Nil{}, last->data); @*/ + /*@ unfold snoc(Fwd, last->data); @*/ + + if (front->next == second_last) { + return; + } else { + Own_Inner_fwds_append_lemma(front->next, second_last, last); + return; + } +} + +void Own_Inner_bwds_append_lemma(struct node *front, struct node *second_front, struct node *last) +/*@ + requires + take F = Owned(front); + take Second_front = Owned(second_front); + take Last = Owned(last); + take Bwd = Own_Inner_Bwds(Last.prev, last, Last, second_front, Second_front); + ptr_eq(Second_front.prev, front); + ptr_eq(F.next, second_front); + ensures + take F2 = Owned(front); + take Last2 = Owned(last); + take Bwd2 = Own_Inner_Bwds(Last.prev, last, Last, front, F2); + Bwd2 == snoc(Bwd, F.data); + Last == Last2; + F2 == F; +@*/ +{ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + /*@ unfold snoc(Bwd, front->data); @*/ + + if (last->prev == second_front) { + return; + } else { + Own_Inner_bwds_append_lemma(front, second_front, last->prev); + return; + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/c_types.h b/src/examples/Dbl_Queue/c_types.h new file mode 100644 index 00000000..7f8dbf92 --- /dev/null +++ b/src/examples/Dbl_Queue/c_types.h @@ -0,0 +1,10 @@ +struct dbl_queue { + struct node* front; + struct node* back; +}; + +struct node { + int data; + struct node* prev; + struct node* next; +}; \ No newline at end of file diff --git a/src/examples/Dbl_Queue/empty.c b/src/examples/Dbl_Queue/empty.c new file mode 100644 index 00000000..c6f72e44 --- /dev/null +++ b/src/examples/Dbl_Queue/empty.c @@ -0,0 +1,16 @@ +#include "./headers.h" + +struct dbl_queue *empty_dbl_queue() +/* --BEGIN-- */ +/*@ ensures + !is_null(return); + take ret = Dbl_Queue_Fwd_At(return); + ret == Seq_Nil{}; +@*/ +/* --END-- */ +{ + struct dbl_queue *q = malloc_dbl_queue(); + q->front = 0; + q->back = 0; + return q; +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/functions.c b/src/examples/Dbl_Queue/functions.h similarity index 84% rename from src/examples/Dbl_Queue/functions.c rename to src/examples/Dbl_Queue/functions.h index b7741126..aa02d5e4 100644 --- a/src/examples/Dbl_Queue/functions.c +++ b/src/examples/Dbl_Queue/functions.h @@ -1,30 +1,3 @@ -#include "./predicates.c" -extern struct dbl_queue *malloc_dbl_queue(); -/*@ spec malloc_dbl_queue(); - requires true; - ensures take u = Block(return); - !ptr_eq(return,NULL); -@*/ - -extern void free_dbl_queue (struct dbl_queue *p); -/*@ spec free_dbl_queue(pointer p); - requires take u = Block(p); - ensures true; -@*/ - -extern struct node *malloc_node(); -/*@ spec malloc_node(); - requires true; - ensures take u = Block(return); - !is_null(return); -@*/ - -extern void free_node (struct node *p); -/*@ spec free_node(pointer p); - requires take u = Block(p); - ensures true; -@*/ - struct dbl_queue *empty_dbl_queue() /*@ ensures !is_null(return); diff --git a/src/examples/Dbl_Queue/fwds_append_lemma.h b/src/examples/Dbl_Queue/fwds_append_lemma.h new file mode 100644 index 00000000..ae763689 --- /dev/null +++ b/src/examples/Dbl_Queue/fwds_append_lemma.h @@ -0,0 +1,30 @@ +// #include "./headers.h" + +void Own_Inner_fwds_append_lemma(struct node *front, struct node *second_last, struct node *last) +/*@ + requires + take F = Owned(front); + take Second_last = Owned(second_last); + take Fwd = Own_Inner_Fwds(F.next, front, F, second_last, Second_last); + ptr_eq(Second_last.next, last); + take Last = Owned(last); + ptr_eq(Last.prev, second_last); + ensures + take F2 = Owned(front); + take Last2 = Owned(last); + take Fwd2 = Own_Inner_Fwds(F.next, front, F, last, Last2); + Fwd2 == snoc(Fwd, Last.data); + Last == Last2; + F2 == F; +@*/ +{ + /*@ unfold snoc(Seq_Nil{}, last->data); @*/ + /*@ unfold snoc(Fwd, last->data); @*/ + + if (front->next == second_last) { + return; + } else { + Own_Inner_fwds_append_lemma(front->next, second_last, last); + return; + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/headers.h b/src/examples/Dbl_Queue/headers.h new file mode 100644 index 00000000..3d107ba5 --- /dev/null +++ b/src/examples/Dbl_Queue/headers.h @@ -0,0 +1,9 @@ +#include "../list_c_types.h" +#include "../list_cn_types.h" +#include "../list_hdtl.h" +#include "../list_rev.h" + +#include "./c_types.h" +#include "./preds_bwd.h" +#include "./preds_fwd.h" +#include "./malloc_free.h" \ No newline at end of file diff --git a/src/examples/Dbl_Queue/inner_fwd_eq_bwd_lemma.h b/src/examples/Dbl_Queue/inner_fwd_eq_bwd_lemma.h new file mode 100644 index 00000000..77ef4909 --- /dev/null +++ b/src/examples/Dbl_Queue/inner_fwd_eq_bwd_lemma.h @@ -0,0 +1,62 @@ +#include "./headers.h" +#include "./append_lemmas.h" + +void Own_Inner_fwds_eq_bwd_lemma(struct node *front, struct node *back) +/*@ requires + !ptr_eq(front, back); + + take B = Owned(back); + is_null(B.next); + !is_null(B.prev); + + take F = Owned(front); + !is_null(F.next); + + take Fwd = Own_Inner_Fwds(F.next, front, F, back, B); + ensures + take B2 = Owned(back); + B == B2; + take F2 = Owned(front); + F == F2; + take Bwd = Own_Inner_Bwds(B.prev, back, B, front, F); + rev(Seq_Cons{head: F.data, tail: Fwd}) == Seq_Cons{head: B.data, tail: Bwd}; +@*/ +{ + if (front == 0) { + return; + } else { + if (front == back) { + return; + } else { + if (front->next == 0) { + return; + } else { + if (front->next == back) { + /*@ unfold rev(Seq_Nil{}); @*/ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + + /*@ unfold rev(Seq_Cons{head: back->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ + + /*@ unfold rev(Seq_Cons{head: front->data, tail: Seq_Cons{head: back->data, tail: Seq_Nil{}}}); @*/ + + /*@ unfold snoc(Seq_Cons{head: back->data, tail: Seq_Nil{}}, front->data); @*/ + + return; + } else { + + Own_Inner_fwds_eq_bwd_lemma(front->next, back); + + Own_Inner_bwds_append_lemma(front, front->next, back); + + + /*@ unfold rev(Seq_Cons{ head: front->data, tail: Fwd}); @*/ + /*@ unfold snoc(rev(Fwd), front->data); @*/ + + + return; + } + } + } + } +} diff --git a/src/examples/Dbl_Queue/lemmas.c b/src/examples/Dbl_Queue/lemmas.h similarity index 100% rename from src/examples/Dbl_Queue/lemmas.c rename to src/examples/Dbl_Queue/lemmas.h diff --git a/src/examples/Dbl_Queue/main.broken.c b/src/examples/Dbl_Queue/main.broken.c new file mode 100644 index 00000000..6b583db6 --- /dev/null +++ b/src/examples/Dbl_Queue/main.broken.c @@ -0,0 +1,12 @@ +#include "./headers.h" +#include "./functions.h" + +int main() +{ + struct dbl_queue *q = empty_dbl_queue(); + push_front(q, 1); + pop_back(q); + free_dbl_queue(q); + + return 0; +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/malloc_free.h b/src/examples/Dbl_Queue/malloc_free.h new file mode 100644 index 00000000..5153466c --- /dev/null +++ b/src/examples/Dbl_Queue/malloc_free.h @@ -0,0 +1,25 @@ +extern struct dbl_queue *malloc_dbl_queue(); +/*@ spec malloc_dbl_queue(); + requires true; + ensures take u = Block(return); + !ptr_eq(return,NULL); +@*/ + +extern void free_dbl_queue (struct dbl_queue *p); +/*@ spec free_dbl_queue(pointer p); + requires take u = Block(p); + ensures true; +@*/ + +extern struct node *malloc_node(); +/*@ spec malloc_node(); + requires true; + ensures take u = Block(return); + !is_null(return); +@*/ + +extern void free_node (struct node *p); +/*@ spec free_node(pointer p); + requires take u = Block(p); + ensures true; +@*/ \ No newline at end of file diff --git a/src/examples/Dbl_Queue/own_FB_fwds_eq_bwds_lemma.h b/src/examples/Dbl_Queue/own_FB_fwds_eq_bwds_lemma.h new file mode 100644 index 00000000..8ed80064 --- /dev/null +++ b/src/examples/Dbl_Queue/own_FB_fwds_eq_bwds_lemma.h @@ -0,0 +1,36 @@ + +void Own_Front_Back_fwds_eq_bwds_lemma(struct node *front, struct node *back) +/*@ requires + (is_null(front) && is_null(back)) || (!is_null(front) && !is_null(back)); + take Q_Fwd = Own_Front_Back_Fwds(front, back); + ensures + take Q_Bwd = Own_Front_Back_Bwds(front, back); + rev(Q_Fwd) == Q_Bwd; +@*/ +{ + /*@ unfold rev(Seq_Nil{}); @*/ + if (front == 0) { + return; + } else { + if (front == back) { + /*@ unfold rev(Seq_Cons{head: back->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ + return; + } else { + if (front->next == back) + { + /*@ unfold rev(Seq_Cons{head: back->data, tail: Seq_Nil{}}); @*/ + /*@ unfold snoc(Seq_Nil{}, back->data); @*/ + /*@ unfold rev(Q_Fwd); @*/ + /*@ unfold snoc(Seq_Nil{}, front->data); @*/ + /*@ unfold snoc(Seq_Cons{head: back->data, tail: Seq_Nil{}}, front->data); @*/ + + return; + } + else { + Own_Inner_fwds_eq_bwd_lemma(front, back); + return; + } + } + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/pop_back.c b/src/examples/Dbl_Queue/pop_back.c new file mode 100644 index 00000000..f71ffe26 --- /dev/null +++ b/src/examples/Dbl_Queue/pop_back.c @@ -0,0 +1,38 @@ +#include "./headers.h" +int pop_back (struct dbl_queue* q) +/* --BEGIN-- */ +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Bwd_At(q); + Before != Seq_Nil{}; + ensures take After = Dbl_Queue_Bwd_At(q); + After == tl(Before); + hd(Before) == return; +@*/ +/* --END-- */ +{ + /* --BEGIN-- */ + /*@ split_case(is_null(q->back)); @*/ + /*@ assert(!is_null(q->front)); @*/ + /* --END-- */ + if (q->front == q->back) { // singleton list case + int data = q->back->data; + free_node(q->back); + q->front = 0; + q->back = 0; + return data; + + } else { + /* --BEGIN-- */ + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + /* --END-- */ + struct node *back = q->back; + int data = back->data; + back->prev->next = 0; + q->back = back->prev; + free_node(back); + /* --BEGIN-- */ + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + /* --END-- */ + return data; + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/pop_front.c b/src/examples/Dbl_Queue/pop_front.c new file mode 100644 index 00000000..162086e8 --- /dev/null +++ b/src/examples/Dbl_Queue/pop_front.c @@ -0,0 +1,33 @@ +#include "./headers.h" + +int pop_front (struct dbl_queue* q) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Fwd_At(q); + Before != Seq_Nil{}; + ensures take After = Dbl_Queue_Fwd_At(q); + After == tl(Before); + hd(Before) == return; +@*/ +{ + /*@ split_case(is_null(q->front)); @*/ + + if (q->front == q->back) { // singleton list case + int data = q->front->data; + free_node(q->front); + q->front = 0; + q->back = 0; + return data; + + } else { + /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ + + struct node *front = q->front; + int data = front->data; + front->next->prev = 0; + q->front = front->next; + free_node(front); + + /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ + return data; + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/pop_front_orig.broken.c b/src/examples/Dbl_Queue/pop_front_orig.broken.c new file mode 100644 index 00000000..9768fe8b --- /dev/null +++ b/src/examples/Dbl_Queue/pop_front_orig.broken.c @@ -0,0 +1,21 @@ +#include "./headers.h" + +int pop_front (struct dbl_queue* q) +{ + if (q->front == q->back) { // singleton list case + int data = q->front->data; + free_node(q->front); + q->front = 0; + q->back = 0; + + return data; + } else { + struct node *front = q->front; + int data = front->data; + front->next->prev = 0; + q->front = front->next; + free_node(front); + + return data; + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/predicates.c b/src/examples/Dbl_Queue/predicates.c deleted file mode 100644 index 9bff56ae..00000000 --- a/src/examples/Dbl_Queue/predicates.c +++ /dev/null @@ -1,160 +0,0 @@ -#include "../list_c_types.h" -#include "../list_cn_types.h" -#include "../list_hdtl.h" -#include "../list_rev.h" - -struct dbl_queue { - struct node* front; - struct node* back; -}; - -struct node { - int data; - struct node* prev; - struct node* next; -}; - -/*@ - -// This predicate owns the outer queue structure and -// asserts that the front and back pointers are either -// both null or both point to a node. It then takes -// ownership of the nodes in the list in the forwards -// direction through a call to Own_Front_Back_Fwds. It returns -// a sequence of integers representing the data in the queue. -predicate (datatype seq) Dbl_Queue_Fwd_At (pointer l) { - if (is_null(l)) { - return Seq_Nil{}; - } - else { - take L = Owned(l); - assert ( (is_null(L.front) && is_null(L.back)) - || (!is_null(L.front) && !is_null(L.back))); - take inner = Own_Front_Back_Fwds(L.front, L.back); - return inner; - } -} - - -// This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Inner_Fwds to take ownership of the rest of the nodes -// in the queue. It asserts that the front node has a null prev pointer -// and that the back node has a null next pointer. It then returns a -// sequence of integers representing the data in the queue. -predicate (datatype seq) Own_Front_Back_Fwds (pointer front, pointer back) { - if (is_null(front)) { - return Seq_Nil{}; - } else { - if (ptr_eq(front, back)) { - // Only one node in the list, so only one node to own - take F = Owned(front); - assert (is_null(F.next)); - assert (is_null(F.prev)); - return Seq_Cons {head: F.data, tail: Seq_Nil{}}; - } else { - take B = Owned(back); - assert (is_null(B.next)); - take F = Owned(front); - assert(is_null(F.prev)); - assert(!is_null(F.next)); - assert(!is_null(B.prev)); - take Rest = Own_Inner_Fwds(F.next, front, F, back, B); - return Seq_Cons{ head: F.data, tail: Rest}; - } - } -} - -// This recursive predicate takes ownership of a node in the queue, -// and includes checks that the queue is properly doubly linked. It -// also asserts that any node owned in this predicate is not the front -// or the back node. It calls itself recursively, walking forwards until -// it reaches the last node in the list, which was already owned in the -// `Own_Front_Back_Fwds` predicate. The base case puts the back node into the sequence, -// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -predicate (datatype seq) Own_Inner_Fwds(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { - if (ptr_eq(p,b)) { - assert(ptr_eq(Back.prev, prev_pointer)); - assert(ptr_eq(prev_node.next, p)); - return Seq_Cons{head: Back.data, tail: Seq_Nil{}}; - } else { - take n = Owned(p); - assert (ptr_eq(n.prev, prev_pointer)); - assert(ptr_eq(prev_node.next, p)); - assert(!is_null(n.next)); - assert(!is_null(n.prev)); - take Rest = Own_Inner_Fwds(n.next, p, n, b, Back); - return Seq_Cons{head: n.data, tail: Rest}; - } -} - -// This predicate owns the outer queue structure and -// asserts that the front and back pointers are either -// both null or both point to a node. It then takes -// ownership of the nodes in the list in the backwards -// direction through a call to Own_Front_Back_Bwds. It returns -// a sequence of integers representing the data in the queue -// BACKWARDS. It returns the reverse of a call to Dbl_Queue_Fwd_At. -predicate (datatype seq) Dbl_Queue_Bwd_At (pointer l) { - if (is_null(l)) { - return Seq_Nil{}; - } - else { - take L = Owned(l); - assert ( (is_null(L.front) && is_null(L.back)) - || (!is_null(L.front) && !is_null(L.back))); - take inner = Own_Front_Back_Bwds(L.front, L.back); - return inner; - } -} - -// This predicate owns the front and back nodes in the queue, and then -// takes calls Own_Inner_Bwds to take ownership of the rest of the nodes -// in the queue. It asserts that the front node has a null prev pointer -// and that the back node has a null next pointer. It then returns a -// sequence of integers representing the data in the queue BACKWARDS. -predicate (datatype seq) Own_Front_Back_Bwds (pointer front, pointer back) { - if (is_null(front)) { - return Seq_Nil{}; - } else { - if (ptr_eq(front, back)) { - take B = Owned(back); - assert (is_null(B.next)); - assert (is_null(B.prev)); - return Seq_Cons {head: B.data, tail: Seq_Nil{}}; - } else { - take B = Owned(back); - assert (is_null(B.next)); - take F = Owned(front); - assert(is_null(F.prev)); - assert(!is_null(F.next)); - assert(!is_null(B.prev)); - take Rest = Own_Inner_Bwds(B.prev, back, B, front, F); - return Seq_Cons{ head: B.data, tail: Rest}; - } - } -} - -// This recursive predicate takes ownership of a node in the queue, -// and includes checks that the queue is properly doubly linked. It -// also asserts that any node owned in this predicate is not the front -// or the back node. It calls itself recursively, walking backwards until -// it reaches the first node in the list, which was already owned in the -// `Own_Front_Back_Bwds` predicate. The base case puts the front node into the sequence, -// in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`. -// Note that the front is put in the back because this sequence is backwards. -predicate (datatype seq) Own_Inner_Bwds(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { - if (ptr_eq(p,f)) { - assert(ptr_eq(Front.next, next_pointer)); - assert(ptr_eq(next_node.prev, p)); - return Seq_Cons{head: Front.data, tail: Seq_Nil{}}; - } else { - take n = Owned(p); - assert (ptr_eq(n.next, next_pointer)); - assert(ptr_eq(next_node.prev, p)); - assert(!is_null(n.next)); - assert(!is_null(n.prev)); - take Rest = Own_Inner_Bwds(n.prev, p, n, f, Front); - return Seq_Cons{head: n.data, tail: Rest}; - } -} -@*/ \ No newline at end of file diff --git a/src/examples/Dbl_Queue/preds_bwd.h b/src/examples/Dbl_Queue/preds_bwd.h new file mode 100644 index 00000000..47dcd511 --- /dev/null +++ b/src/examples/Dbl_Queue/preds_bwd.h @@ -0,0 +1,53 @@ +/*@ + +predicate (datatype seq) Dbl_Queue_Bwd_At (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = Own_Front_Back_Bwds(L.front, L.back); + return inner; + } +} + +predicate (datatype seq) Own_Front_Back_Bwds (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + take B = Owned(back); + assert (is_null(B.next)); + assert (is_null(B.prev)); + return Seq_Cons {head: B.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + assert(!is_null(F.next)); + assert(!is_null(B.prev)); + take Rest = Own_Inner_Bwds(B.prev, back, B, front, F); + return Seq_Cons{ head: B.data, tail: Rest}; + } + } +} + +predicate (datatype seq) Own_Inner_Bwds(pointer p, pointer next_pointer, struct node next_node, pointer f, struct node Front) { + if (ptr_eq(p,f)) { + assert(ptr_eq(Front.next, next_pointer)); + assert(ptr_eq(next_node.prev, p)); + return Seq_Cons{head: Front.data, tail: Seq_Nil{}}; + } else { + take n = Owned(p); + assert (ptr_eq(n.next, next_pointer)); + assert(ptr_eq(next_node.prev, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Inner_Bwds(n.prev, p, n, f, Front); + return Seq_Cons{head: n.data, tail: Rest}; + } +} +@*/ \ No newline at end of file diff --git a/src/examples/Dbl_Queue/preds_fwd.h b/src/examples/Dbl_Queue/preds_fwd.h new file mode 100644 index 00000000..aaf5325b --- /dev/null +++ b/src/examples/Dbl_Queue/preds_fwd.h @@ -0,0 +1,54 @@ +/*@ + +predicate (datatype seq) Dbl_Queue_Fwd_At (pointer l) { + if (is_null(l)) { + return Seq_Nil{}; + } + else { + take L = Owned(l); + assert ( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = Own_Front_Back_Fwds(L.front, L.back); + return inner; + } +} + +predicate (datatype seq) Own_Front_Back_Fwds (pointer front, pointer back) { + if (is_null(front)) { + return Seq_Nil{}; + } else { + if (ptr_eq(front, back)) { + // Only one node in the list, so only one node to own + take F = Owned(front); + assert (is_null(F.next)); + assert (is_null(F.prev)); + return Seq_Cons {head: F.data, tail: Seq_Nil{}}; + } else { + take B = Owned(back); + assert (is_null(B.next)); + take F = Owned(front); + assert(is_null(F.prev)); + assert(!is_null(F.next)); + assert(!is_null(B.prev)); + take Rest = Own_Inner_Fwds(F.next, front, F, back, B); + return Seq_Cons{ head: F.data, tail: Rest}; + } + } +} + +predicate (datatype seq) Own_Inner_Fwds(pointer p, pointer prev_pointer, struct node prev_node, pointer b, struct node Back) { + if (ptr_eq(p,b)) { + assert(ptr_eq(Back.prev, prev_pointer)); + assert(ptr_eq(prev_node.next, p)); + return Seq_Cons{head: Back.data, tail: Seq_Nil{}}; + } else { + take n = Owned(p); + assert (ptr_eq(n.prev, prev_pointer)); + assert(ptr_eq(prev_node.next, p)); + assert(!is_null(n.next)); + assert(!is_null(n.prev)); + take Rest = Own_Inner_Fwds(n.next, p, n, b, Back); + return Seq_Cons{head: n.data, tail: Rest}; + } +} +@*/ \ No newline at end of file diff --git a/src/examples/Dbl_Queue/push_back.c b/src/examples/Dbl_Queue/push_back.c new file mode 100644 index 00000000..72122bc4 --- /dev/null +++ b/src/examples/Dbl_Queue/push_back.c @@ -0,0 +1,35 @@ +#include "./headers.h" + +// Given a dbl queue pointer, inserts a new node +// to the back of the list +void push_back (struct dbl_queue* q, int element) +/* --BEGIN-- */ +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Bwd_At(q); + ensures take After = Dbl_Queue_Bwd_At(q); + After == Seq_Cons{head: element, tail: Before}; +@*/ +/* --END-- */ +{ + struct node *new_node = malloc_node(); + new_node->data = element; + new_node->next = 0; + new_node->prev = q->back; + /* --BEGIN-- */ + /*@ split_case(ptr_eq((*q).front, (*q).back)); @*/ + /* --END-- */ + if (q->back != 0) { + /* --BEGIN-- */ + /*@ split_case(ptr_eq((*(*q).back).prev, (*q).front)); @*/ + /* --END-- */ + q->back->next = new_node; + q->back = new_node; + return; + + } else { + // in this case, the queue is empty + q->back = new_node; + q->front = new_node; + return; + } +} \ No newline at end of file diff --git a/src/examples/Dbl_Queue/push_front.c b/src/examples/Dbl_Queue/push_front.c new file mode 100644 index 00000000..3edde120 --- /dev/null +++ b/src/examples/Dbl_Queue/push_front.c @@ -0,0 +1,28 @@ +#include "./headers.h" + +// Given a dbl queue pointer, inserts a new node +// to the front of the list +void push_front (struct dbl_queue* q, int element) +/*@ requires (!is_null(q)); + take Before = Dbl_Queue_Fwd_At(q); + ensures take After = Dbl_Queue_Fwd_At(q); + After == Seq_Cons{head: element, tail: Before}; +@*/ +{ + struct node *new_node = malloc_node(); + new_node->data = element; + new_node->next = q->front; + new_node->prev = 0; + + if (q->front == 0) { + // in this case, the queue is empty + q->back = new_node; + q->front = new_node; + } else { + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + /*@ split_case(ptr_eq(q->front->next, q->back)); @*/ + q->front->prev = new_node; + q->front = new_node; + } +} + diff --git a/src/examples/Dbl_Queue/push_front_orig.broken.c b/src/examples/Dbl_Queue/push_front_orig.broken.c new file mode 100644 index 00000000..04f528e5 --- /dev/null +++ b/src/examples/Dbl_Queue/push_front_orig.broken.c @@ -0,0 +1,19 @@ +// Given a dbl queue pointer, inserts a new node +// to the front of the list +void push_front (struct dbl_queue* q, int element) +{ + struct node *new_node = malloc_node(); + new_node->data = element; + new_node->next = q->front; + new_node->prev = 0; + + if (q->front == 0) { + // in this case, the queue is empty + q->back = new_node; + q->front = new_node; + } else { + q->front->prev = new_node; + q->front = new_node; + } +} + diff --git a/src/examples/Dbl_Queue/main.c b/src/examples/Dbl_Queue/verified_examples.c similarity index 97% rename from src/examples/Dbl_Queue/main.c rename to src/examples/Dbl_Queue/verified_examples.c index c2b0a4a1..3c476d23 100644 --- a/src/examples/Dbl_Queue/main.c +++ b/src/examples/Dbl_Queue/verified_examples.c @@ -1,5 +1,6 @@ -#include "./functions.c" -#include "./lemmas.c" +#include "headers.h" +#include "./functions.h" +#include "./lemmas.h" void ex_front() { diff --git a/src/tutorial.adoc b/src/tutorial.adoc index e4d78dc0..a2539301 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -1354,6 +1354,174 @@ Now, let's look at the annotations in the function body. These are similar to in *Exercise*: There are many other functions that one might want to implement for a doubly linked list. For example, one might want to implement a function that appends one list to another, or a function that reverses a list. Try implementing these functions and writing their specifications. +// ====================================================================== + +=== Double Ended Queues + +We have already seen an implementation of a single ended and a doubly linked list in CN. Now we can combine those ideas into a double ended queue. This is a list that allows for O(1) operations for adding or removing elements from either end of the list. Here is the C type definition: + +include_example(exercises/Dbl_Queue/c_types.h) + +Notice that here we have the same exact `node` type as in the doubly linked list example, paired with an outer `dbl_queue` wrapper similar to the `int_queue` wrapper in the imperative queues example. Just as in the imperative queue example, we will just use `seq` as our representation of the data in the list. + +The predicates for this data structure are also a mix of the doubly linked list and imperative queue predicates. We will have a three-tiered predicate structure in the forwards and backwards direction. First, let's look at the forwards direction. + +include_example(exercises/Dbl_Queue/preds_fwd.h) + +The `Dbl_Queue_Fwd_At` predicate owns the outer queue structure and +asserts that the front and back pointers are either both null or both +point to a node. It then takes ownership of the nodes in the list in the +forwards direction through a call to `Own_Front_Back_Fwds`. It returns +a sequence of integers representing the data in the queue. + +The `Own_Front_Back_Fwds` predicate owns the front and back nodes in the +queue, and then calls `Own_Inner_Fwds` to take ownership of the rest of +the nodes in the queue. It asserts that the front node has a null `prev` +pointer and that the back node has a null `next` pointer. It then returns a sequence of integers representing the data in the queue. + +`Own_Inner_Fwds` is a recursive predicate that takes ownership of a +node in the queue, and includes checks that the queue is properly doubly +linked. It also asserts that any node owned in this predicate is not the +front or the back node. It calls itself recursively, walking forwards until +it reaches the last node in the list, which was already owned in the +`Own_Front_Back_Fwds` predicate. The base case puts the back node into the sequence, in order to avoid a call to `snoc`. This helps avoid future calls to `unfold`, although this strategy can cause issues in other cases. + +Now let's look at the backwards direction. + +include_example(exercises/Dbl_Queue/preds_bwd.h) + +You may notice that the backwards predicates are almost completely identical, except that they walk backwards through the list. This means that the `seq` +representation is also backwards. Note that `Own_Front_Back_Fwds` and `Own_Front_Back_Bwds` are exactly the same, and `Own_Front_Back_Fwds` is the same as `Own_Front_Back_Bwds`. The only difference is that they call the forwards or backwards recursive predicate. +The forwards and backwards predicates being identical to the second layer will help us prove that they are equivalent later on. + +The reason for having predicates for the forwards and backwards directions is to solve the issue that every node has multiple pointers to it. By choosing a forwards or backwards direction, we are choosing which pointer to a node can read or write to the node. We will see why this is important later. + +As always, we need some boiler plate for allocation and deallocation. + +include_example(exercises/Dbl_Queue/malloc_free.h) + +// ====================================================================== + +*Exercise*: Look at the initialization function for an empty queue, and add +the necessary annotations. Make sure to include postconditions for ownership as well as correctness of the sequence representation. + +include_example(exercises/Dbl_Queue/empty.c) + +// ====================================================================== + +Now, let's look at a `push` function for the front of the queue. Here is the un-annotated version: + +include_example(exercises/Dbl_Queue/push_front_orig.broken.c) + +*Exercise*: Before reading on, see if you can figure out what specifications are needed. + +Now, here is the fully annotated version of the `push_front` operation: + +include_example(exercises/Dbl_Queue/push_front.c) + +Here, we require that the input queue is non null, because we cannot add +nodes to a queue that does not exist. Note that this is different from saying that the queue is empty. We take ownership of the queue forwards so that we can easily manipulate the `next` pointers in the queue. In this way, we are saying that the `next` pointers are the primary pointers in the list, and the `prev` pointers are just auxiliary. We also ensure that the sequence representation of the queue is correct. + +The two `split_case` annotations open up the `Own_Front_Back_Fwds` and `Own_Inner_Fwds` predicates, respectively. CN needs these annotations to see that we haven't lost ownership of the rest of the list. + +*Exercise*: Add the necessary annotations to the `push_back` function for the double ended queue. + +*Hint*: Remember that the `seq` representation of a queue that we owned backwards is reversed. + +include_example(exercises/Dbl_Queue/push_back.c) + +// ====================================================================== + +Now, let's look at the `pop_front` function. Here is the un-annotated version: + +include_example(exercises/Dbl_Queue/pop_front_orig.broken.c) + +*Exercise*: Before reading on, see if you can figure out what specifications are needed. + +Now, here is the fully annotated version of the `pop_front` operation: + +include_example(exercises/Dbl_Queue/pop_front.c) + +Like before, we require that the input queue is non null, because we cannot remove nodes from a queue that does not exist. We take ownership of the queue forwards so that we can easily manipulate the `next` pointers in the queue. We also require that the queue is not empty. For the postconditions, we ensure that +the integers in the queue are the same as before, except for the first one, which is removed. We also ensure that the returned integer was previously the head of the list that we removed. + +The first `split_case` annotation helps CN reason that the front of the list cannot be null, as this is the only way the `seq` would be Nil. The second `split_case` annotation helps CN reason that we do have reading and writing access to `front->next->prev`. The last `split_case` annotation helps CN reason that we have the correct resources to return (in other words, that we still have ownership over the rest of the queue). + +*Exercise*: Add the necessary annotations to the `pop_back` function for the double ended queue. + +include_example(exercises/Dbl_Queue/pop_back.c) + +// ====================================================================== + +Now, consider the following attempt to write a `main` function that uses these functions. + +include_example(exercises/Dbl_Queue/main.broken.c) + +Note that if you attempt to verify this, you get the following error message: + +.... +src/examples/Dbl_Queue/main.broken.c:8:5: error: Missing resource for calling function pop_back + pop_back(q); + ^~~~~~~~~~~ +Resource needed: Dbl_Queue_Bwd_At(call_empty_dbl_queue0 + .return) + src/examples/Dbl_Queue/./functions.c:106:19: (arg Before) + which requires: Own_Front_Back_Bwds(unpack_Dbl_Queue_Fwd_At3 + .L + .front + , unpack_Dbl_Queue_Fwd_At3.L.back) + src/examples/Dbl_Queue/./preds_bwd.h:11:14: (arg inner) +State file: file:///var/folders/yl/n1rm8_rj7wn0zxwvpr78c2zw0000gn/T/state_fa6abd.html +.... + +This is because the postcondition of `push_front` says that we have ownership over the queue in the forwards direction, but the precondition of `pop_back` requires that we have ownership of the queue in the backwards direction. Logically, we know that these are the same thing, but CN does not. So we must prove that `Dbl_Queue_Fwd_At` and `Dbl_Queue_Bwd_At` are equivalent. + +We can prove these by writing lemmas in CN itself. The general idea is that we want to use induction to prove that 'Own_Inner_Fwds' and 'Own_Inner_Bwds' are equivalent, since they are recursive. Remember that the other predicates are completely the same except for which recursive predicate they call, so if we can prove the recusrive predicates are equivalent, it is trivial to prove the rest equivalent. Additionally, in order to make the inductive step, we will need a lemma that says that if we own a queue forwards to its second to last element, and we own the last element, then we own the queue forwards to its last element (and equivalent for backwards). + +First, we need to write a lemma that says that if we own a queue forwards to its second to last element, and we own the last element, then we own the queue forwards to its last element. This lemma will be helpful for the induction step later on. + +include_example(exercises/Dbl_Queue/fwds_append_lemma.h) + +Note that here we are using the `Own_Inner_Fwds` predicate for this lemma, and include any assertions we would get in `Own_Front_Back_Fwds` as a precondition. This helps give necessary context to CN. + +*Exercise*: Write an equivalent lemma for the backwards direction. + +Now, we can write the lemma that 'Own_Inner_Fwds' and 'Own_Inner_Bwds' are equivalent. + +*Exercise*: Before reading on, try writing these lemmas yourself. + +include_example(exercises/Dbl_Queue/inner_fwd_eq_bwd_lemma.h) + +Notice here that once again, the preconditions include information we get in `Own_front_back_Fwds`. This is also why we own the front and the back in the pre and post condition -- this step is done in the predicate that calls 'Own_Inner_Fwds'. + +We own the inner nodes forwards in the precondition and backwards in the postcondition. Since the queue is not changed in this function, we are showing that the two directions are equivalent. Additionally, we make the claim that the sequence representations are reverses of each other. + +We spell out all of the base cases in the function body explicitly to make it easier to reason about. In the case where `front->next == back`, there are two elements in the list, and we need to include some unfolds to help CN reason that the reverse of [front, back] is [back, front]. The induction step is only necessary when the queue has at least three elements, because this is when `Own_Inner_Fwds` and `Own_Inner_Bwds` actually own parts of the list. + +When we call `Own_Inner_fwds_eq_bwd_lemma(front->next, back)`, we get the information that everything forwards from the second element to the back is equivalent to everything backwards from the back to the second element. So now we own everything backwards to the second element, and we own the first element. This allows us to call `Own_Inner_bwds_append_lemma(front, front->next, back)` for the inductive step. Now, we own everything in the list backwards. The last thing to do is unfold some recursive function definitions so that CN can verify that the sequence representations are the reverse of each other. + +*Exercise*: Try writing the equivalent lemma for the other way around. + +Now, we can build up the same lemmas for the outer predicates. + +*Exercise*: Before reading on, try writing lemmas yourself that `Own_Front_Back_Fwds` and `Own_Front_Back_Bwds` are equivalent, as well as that `Dbl_Queue_Fwd_At` and `Dbl_Queue_Bwd_At` are equivalent. + +Now, look at the proof that `Own_Front_Back_Fwds` is equivalent to `Own_Front_Back_Bwds`. + +include_example(exercises/Dbl_Queue/own_FB_fwds_eq_Bwds_lemma.h) + +Note that once again, we include any information we usually get from the predicate above. The main difficulty in this lemma is unfolding enough to convince CN that the sequence representations are the reverse of each other. + +*Exercise*: Try writing the equivalent lemma in the other direction. + +*Exercise*: Try writing lemmas that `Dbl_Queue_Fwd_At` and `Dbl_Queue_Bwd_At` are equivalent. + +*Exercise*: Use these lemmas to rewrite the `main` function so that it can be verified. + +*Exercise*: Explore what would happen if we tried to only use the forwards predicates for the backwards operations. Can you get this to work? Why or why not? + +If you get stuck, full verfied solutions can be found in `functions.h`, `lemmas..h`, and `verified_examples.c`. + === The Runway Suppose we have been tasked with writing a program that simulates a runway at an airport. This airport is very small, so it only has one runway that is used for both takeoffs and landings. We want to verify that the runway is always safe by implementing the following specifications into CN: From ac6c298a1cc929b3c88c616f967b9be9d38d8bbc Mon Sep 17 00:00:00 2001 From: Liz Austell Date: Tue, 30 Jul 2024 14:40:25 -0400 Subject: [PATCH 19/20] nits --- src/tutorial.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tutorial.adoc b/src/tutorial.adoc index a2539301..14642e0b 100644 --- a/src/tutorial.adoc +++ b/src/tutorial.adoc @@ -1520,7 +1520,7 @@ Note that once again, we include any information we usually get from the predica *Exercise*: Explore what would happen if we tried to only use the forwards predicates for the backwards operations. Can you get this to work? Why or why not? -If you get stuck, full verfied solutions can be found in `functions.h`, `lemmas..h`, and `verified_examples.c`. +If you get stuck, full verified solutions can be found in `functions.h`, `lemmas.h`, and `verified_examples.c`. === The Runway From 2be37d35f252b2e0926916e0a494111b87573ba0 Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 8 Aug 2024 11:23:37 -0400 Subject: [PATCH 20/20] Best version of push operation --- src/examples/dbl_best_push.c | 93 ++++++++++++++++++++++++++++++++++++ 1 file changed, 93 insertions(+) create mode 100644 src/examples/dbl_best_push.c diff --git a/src/examples/dbl_best_push.c b/src/examples/dbl_best_push.c new file mode 100644 index 00000000..20922f82 --- /dev/null +++ b/src/examples/dbl_best_push.c @@ -0,0 +1,93 @@ +/* A version of doubly linked lists that is essentially from Reynold's + original separation logic paper (https://www.cs.cmu.edu/~jcr/seplogic.pdf). + Page 10 has his definition of doubly-linked lists (dlist). + + They're slightly different from ours in that they're "open": + there's no special treatment of null for the front of the list. + + Technical note for the future: We could eliminate the hacky + assert_not_equal reasoning if we added this lemma: + + lemma assert_not_equal (p, prev, cur, f, b) + requires Own_Fwd(prev, cur, f, b); + Owned(p); + ensures Own_Fwd(prev, cur, f, b); + Owned(p); + !ptr_eq(p,b); + + This more specific lemma is something we could actually + (eventually) prove in Rocq, as an inductive fact derived from the + resource predicate definition. */ + +struct node { + int data; + struct node *prev; + struct node *next; +}; + +struct dbl_queue { + struct node *front; + struct node *back; +}; + +/*@ +datatype seq { + Seq_Nil {}, + Seq_Cons {i32 head, datatype seq tail} +} + +predicate (datatype seq) Dbl_Queue_Fwd_At (pointer l) { + take L = Owned(l); + assert( (is_null(L.front) && is_null(L.back)) + || (!is_null(L.front) && !is_null(L.back))); + take inner = Own_Fwd (L.front, NULL, L.back); + return inner; +} + +predicate (datatype seq) Own_Fwd + (pointer curr, pointer prev, pointer b) { + if (is_null(curr)) { + return Seq_Nil{}; + } else { + take Curr = Owned(curr); + assert(ptr_eq(Curr.prev, prev)); + assert(ptr_eq(curr,b) implies is_null(Curr.next)); + take Rest = Own_Fwd(Curr.next, curr, b); + return Seq_Cons{head: Curr.data, tail: Rest}; + } +} + +lemma assert_not_equal (pointer x, pointer y) + requires true; + ensures !ptr_eq(x,y); +@*/ + +extern struct node *malloc_node(); +/*@ spec malloc_node(); + requires true; + ensures take u = Block(return); +@*/ + +void push_front (struct dbl_queue* q, int element) +/*@ requires take Before = Dbl_Queue_Fwd_At(q); + ensures take After = Dbl_Queue_Fwd_At(q); + After == Seq_Cons{head: element, tail: Before}; +@*/ +{ + struct node *new_node = malloc_node(); + /*@ apply assert_not_equal(new_node, q->front); @*/ + /*@ apply assert_not_equal(new_node, q->back); @*/ + new_node->data = element; + new_node->next = q->front; + new_node->prev = 0; + + if (q->front == 0) { + q->back = new_node; + q->front = new_node; + return; + } else { + q->front->prev = new_node; + q->front = new_node; + return; + } +}