Merge pull request #46 from rems-project/austell_Linkedlist

Add Doubly Linked List example to tutorial

src/examples/Dbl_Linked_List/add.c

@@ -0,0 +1,35 @@
+#include "./headers.h"
+
+// Adds after the given node and returns a pointer to the new node
+struct node *add(int element, struct node *n)
+/*@ requires take Before = Dll_at(n);
+    ensures  take After = Dll_at(return);
+
+             is_null(n) ? After == Dll { left: Seq_Nil{}, curr: Node(After), right: Seq_Nil{}}
+                        : After == Dll { left: Seq_Cons{head: Node(Before).data, tail: Left(Before)}, curr: Node(After), right: Right(Before)};
+@*/
+{
+    struct node *new_node = malloc_node();
+    new_node->data = element;
+    new_node->prev = 0;
+    new_node->next = 0;
+
+    if (n == 0) //empty list case
+    {
+        new_node->prev = 0;
+        new_node->next = 0;
+        return new_node;
+    } else { 
+        /*@ split_case(is_null((*n).prev)); @*/
+        new_node->next = n->next;
+        new_node->prev = n;
+
+        if (n->next !=0) {
+            /*@ split_case(is_null((*(*n).next).next)); @*/
+            n->next->prev = new_node;
+        }
+
+        n->next = new_node;
+        return new_node;
+    }
+}

src/examples/Dbl_Linked_List/add_orig.broken.c

@@ -0,0 +1,27 @@
+#include "./headers.h"
+
+// Adds after the given node and returns a pointer to the new node
+struct node *add(int element, struct node *n)
+{
+    struct node *new_node = malloc_node();
+    new_node->data = element;
+    new_node->prev = 0;
+    new_node->next = 0;
+
+    if (n == 0) //empty list case
+    {
+        new_node->prev = 0;
+        new_node->next = 0;
+        return new_node;
+    } else { 
+        new_node->next = n->next;
+        new_node->prev = n;
+
+        if (n->next !=0) {
+            n->next->prev = new_node;
+        }
+
+        n->next = new_node;
+        return new_node;
+    }
+}

src/examples/Dbl_Linked_List/c_types.h

@@ -0,0 +1,5 @@
+struct node {
+  int data;  
+  struct node* prev;
+  struct node* next;
+};

src/examples/Dbl_Linked_List/cn_types.h

@@ -0,0 +1,6 @@
+/*@
+datatype Dll {
+    Empty_Dll {},
+    Dll {datatype seq left, struct node curr, datatype seq right}
+}
+@*/

src/examples/Dbl_Linked_List/getters.h

@@ -0,0 +1,22 @@
+/*@
+function (datatype seq) Right (datatype Dll L) {
+    match L {
+        Empty_Dll {} => { Seq_Nil{} }
+        Dll {left: _, curr: _, right: r} => { r }
+    }
+}
+
+function (datatype seq) Left (datatype Dll L) {
+    match L {
+        Empty_Dll {} => { Seq_Nil {} }
+        Dll {left: l, curr: _, right: _} => { l }
+    }
+}
+
+function (struct node) Node (datatype Dll L) {
+    match L {
+        Empty_Dll {} => {  default<struct node> }
+        Dll {left: _, curr: n, right: _} => { n }
+    }
+}
+@*/

src/examples/Dbl_Linked_List/headers.h

@@ -0,0 +1,10 @@
+#include "../list.h"
+#include "../list_append.h"
+#include "../list_rev.h"
+
+#include "./c_types.h"
+#include "./cn_types.h"
+#include "./converters.h"
+#include "./getters.h"
+#include "./malloc_free.h"
+#include "./predicates.h"

src/examples/Dbl_Linked_List/malloc_free.h

@@ -0,0 +1,12 @@
+extern struct node *malloc_node();
+/*@ spec malloc_node();
+    requires true;
+    ensures take u = Block<struct node>(return);
+            !ptr_eq(return,NULL);
+@*/ 
+
+extern void free_node (struct node *p);
+/*@ spec free_node(pointer p);
+    requires take u = Block<struct node>(p);
+    ensures true;
+@*/

src/examples/Dbl_Linked_List/node_and_int.h

@@ -0,0 +1,17 @@
+struct node_and_int {
+  struct node* node;
+  int data;
+};
+
+extern struct node_and_int *malloc_node_and_int();
+/*@ spec malloc_node_and_int();
+    requires true;
+    ensures take u = Block<struct node_and_int>(return);
+            !ptr_eq(return,NULL);
+@*/ 
+
+extern void free_node_and_int (struct node_and_int *p);
+/*@ spec free_node_and_int(pointer p);
+    requires take u = Block<struct node_and_int>(p);
+    ensures true;
+@*/

src/examples/Dbl_Linked_List/predicates.h

@@ -0,0 +1,36 @@
+/*@
+predicate (datatype Dll) Dll_at (pointer p) {
+    if (is_null(p)) {
+        return Empty_Dll{};
+    } else {
+        take n = Owned<struct node>(p);
+        take Left = Own_Backwards(n.prev, p, n);
+        take Right = Own_Forwards(n.next, p, n);
+        return Dll{left: Left, curr: n, right: Right};
+    }
+}
+
+predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) {
+    if (is_null(p)) {
+        return Seq_Nil{};
+    } else {
+        take n = Owned<struct node>(p);
+        assert (ptr_eq(n.prev, prev_pointer));
+        assert(ptr_eq(prev_node.next, p));
+        take Right = Own_Forwards(n.next, p, n);
+        return Seq_Cons{head: n.data, tail: Right};
+    }
+}
+
+predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) {
+    if (is_null(p)) {
+        return Seq_Nil{};
+    } else {
+        take n = Owned<struct node>(p);
+        assert (ptr_eq(n.next, next_pointer));
+        assert(ptr_eq(next_node.prev, p));
+        take Left = Own_Backwards(n.prev, p, n);
+        return Seq_Cons{head: n.data, tail: Left};
+    }
+}
+@*/

src/examples/Dbl_Linked_List/remove.c

@@ -0,0 +1,36 @@
+#include "./headers.h"
+#include "./node_and_int.h"
+
+// removes the given node from the list and returns another pointer 
+// to somewhere in the list, or a null pointer if the list is empty.
+struct node_and_int *remove(struct node *n)
+/*@ requires !is_null(n);
+             take Before = Dll_at(n);
+             let del = Node(Before);
+    ensures  take ret = Owned<struct node_and_int>(return);
+             take After = Dll_at(ret.node);
+             ret.data == del.data;
+             (is_null(del.prev) && is_null(del.next)) ? After == Empty_Dll{}
+                 : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: tl(Right(Before))}
+                     : After == Dll{left: tl(Left(Before)), curr: Node(After), right: Right(Before)});
+@*/
+{
+    struct node *temp = 0;
+    if (n->prev != 0) {
+        /*@ split_case(is_null((*(*n).prev).prev)); @*/
+        n->prev->next = n->next;
+        temp = n->prev;
+    }
+    if (n->next != 0) {
+        /*@ split_case(is_null((*(*n).next).next)); @*/
+        n->next->prev = n->prev;
+        temp = n->next;
+    }
+
+    struct node_and_int *pair = malloc_node_and_int();
+    pair->node = temp;
+    pair->data = n->data;
+
+    free_node(n);       
+    return pair;
+}

src/examples/Dbl_Linked_List/remove_orig.broken.c

@@ -0,0 +1,24 @@
+#include "./headers.h"
+#include "./node_and_int.h"
+
+// removes the given node from the list and returns another pointer 
+// to somewhere in the list, or a null pointer if the list is empty.
+struct node_and_int *remove(struct node *n)
+{
+    struct node *temp = 0;
+    if (n->prev != 0) {
+        n->prev->next = n->next;
+        temp = n->prev;
+    }
+    if (n->next != 0) {
+        n->next->prev = n->prev;
+        temp = n->next;
+    }
+
+    struct node_and_int *pair = malloc_node_and_int();
+    pair->node = temp;
+    pair->data = n->data;
+
+    free_node(n);       
+    return pair;
+}

src/examples/Dbl_Linked_List/singleton.c

@@ -0,0 +1,13 @@
+#include "./headers.h"
+
+struct node *singleton(int element)
+/*@ ensures take Ret = Dll_at(return);
+        Ret == Dll{left: Seq_Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Seq_Nil{}};
+@*/
+{
+   struct node *n = malloc_node();
+   n->data = element;
+   n->prev = 0;
+   n->next = 0;
+   return n;
+}