Add Double Ended Queue example to tutorial

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<struct node>(front);
+      take Second_last = Owned<struct node>(second_last);
+      take Fwd = Own_Inner_Fwds(F.next, front, F, second_last, Second_last);
+      ptr_eq(Second_last.next, last);
+      take Last = Owned<struct node>(last);
+      ptr_eq(Last.prev, second_last);
+  ensures
+      take F2 = Owned<struct node>(front);
+      take Last2 = Owned<struct node>(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<struct node>(front);
+      take Second_front = Owned<struct node>(second_front);
+      take Last = Owned<struct node>(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<struct node>(front);
+      take Last2 = Owned<struct node>(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;
+    }
+}

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;
+};

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;
+}

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;
+    }
+}

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<struct node>(front);
+      take Second_last = Owned<struct node>(second_last);
+      take Fwd = Own_Inner_Fwds(F.next, front, F, second_last, Second_last);
+      ptr_eq(Second_last.next, last);
+      take Last = Owned<struct node>(last);
+      ptr_eq(Last.prev, second_last);
+  ensures
+      take F2 = Owned<struct node>(front);
+      take Last2 = Owned<struct node>(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;
+    }
+}

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"

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<struct node>(back);
+        is_null(B.next);
+        !is_null(B.prev);
+
+        take F = Owned<struct node>(front);
+        !is_null(F.next);
+
+        take Fwd = Own_Inner_Fwds(F.next, front, F, back, B);
+    ensures
+        take B2 = Owned<struct node>(back);
+        B == B2;
+        take F2 = Owned<struct node>(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;
+                }
+            }
+        }
+    }
+}