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 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.h b/src/examples/Dbl_Queue/functions.h new file mode 100644 index 00000000..aa02d5e4 --- /dev/null +++ b/src/examples/Dbl_Queue/functions.h @@ -0,0 +1,134 @@ +struct dbl_queue *empty_dbl_queue() +/*@ ensures + !is_null(return); + take ret = Dbl_Queue_Fwd_At(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_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; + /*@ 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_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->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(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_Bwd_At(q); + ensures take After = Dbl_Queue_Bwd_At(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_Bwd_At(q); + Before != Seq_Nil{}; + ensures take After = Dbl_Queue_Bwd_At(q); + After == tl(Before); + hd(Before) == return; +@*/ +{ + /*@ 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 { + /*@ 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/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.h b/src/examples/Dbl_Queue/lemmas.h new file mode 100644 index 00000000..b38e7af7 --- /dev/null +++ b/src/examples/Dbl_Queue/lemmas.h @@ -0,0 +1,279 @@ +// #include "./predicates.c" + +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; + } +} + +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; + } + } + } + } +} + +void Own_Inner_bwds_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_Inner_Bwds(B.prev, back, B, front, F); + ensures + take B2 = Owned(back); + B == B2; + take F2 = Owned(front); + F == F2; + 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}; +@*/ +{ + 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); @*/ + + /*@ 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_Inner_bwds_eq_fwd_lemma(front, back->prev); + + Own_Inner_fwds_append_lemma(front, back->prev, back); + + + /*@ unfold rev(Seq_Cons{ head: back->data, tail: Bwd}); @*/ + /*@ unfold snoc(rev(Bwd), back->data); @*/ + return; + } + } + } + } +} + +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; + } + } + } +} + +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 = Own_Front_Back_Bwds(front, back); + ensures + take Q_Fwd = Own_Front_Back_Fwds(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_Inner_bwds_eq_fwd_lemma(front, back); + return; + } + } + } +} + +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 { + Own_Front_Back_fwds_eq_bwds_lemma(q->front, q->back); + } +} + +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 { + Own_Front_Back_bwds_eq_fwds_lemma(q->front, q->back); + } +} \ No newline at end of file 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/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/verified_examples.c b/src/examples/Dbl_Queue/verified_examples.c new file mode 100644 index 00000000..3c476d23 --- /dev/null +++ b/src/examples/Dbl_Queue/verified_examples.c @@ -0,0 +1,103 @@ +#include "headers.h" +#include "./functions.h" +#include "./lemmas.h" + +void ex_front() +{ + struct dbl_queue *q = empty_dbl_queue(); + push_front(q, 1); + + 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_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_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); + /*@ assert(one == 1i32); @*/ + /*@ assert(two == 2i32); @*/ + + /*@ split_case(is_null(q->front)); @*/ + /*@ split_case(ptr_eq(q->front, q->back)); @*/ + free_dbl_queue(q); +} + + +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 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; + } +} diff --git a/src/tutorial.adoc b/src/tutorial.adoc index e4d78dc0..14642e0b 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 verified 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: