From e0273594a4d96673fd24192a48d7b4fa86c4d16d Mon Sep 17 00:00:00 2001 From: Benjamin Pierce Date: Thu, 13 Jun 2024 22:12:08 -0400 Subject: [PATCH] Remove temp files --- src/examples/temp-queue-common.h | 48 ----------- src/examples/temp-queue1.broken.c | 103 ---------------------- src/examples/temp-queue1a.broken.c | 99 --------------------- src/examples/temp-queue1b.broken.c | 101 ---------------------- src/examples/temp-queue1c.broken.c | 114 ------------------------- src/examples/temp-queue2.broken.c | 89 ------------------- src/examples/temp-queue3.broken.c | 133 ----------------------------- 7 files changed, 687 deletions(-) delete mode 100644 src/examples/temp-queue-common.h delete mode 100644 src/examples/temp-queue1.broken.c delete mode 100644 src/examples/temp-queue1a.broken.c delete mode 100644 src/examples/temp-queue1b.broken.c delete mode 100644 src/examples/temp-queue1c.broken.c delete mode 100644 src/examples/temp-queue2.broken.c delete mode 100644 src/examples/temp-queue3.broken.c diff --git a/src/examples/temp-queue-common.h b/src/examples/temp-queue-common.h deleted file mode 100644 index 6253aa5b..00000000 --- a/src/examples/temp-queue-common.h +++ /dev/null @@ -1,48 +0,0 @@ -#include "list.h" -#include "list_snoc_cn.h" - -struct int_queue { - struct int_queueCell* head; - struct int_queueCell* tail; -}; - -struct int_queueCell { - int first; - struct int_queueCell* next; -}; - -extern struct int_queue *mallocIntQueue(); -/*@ spec mallocIntQueue(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern void freeIntQueue (struct int_queue *p); -/*@ spec freeIntQueue(pointer p); - requires take u = Block(p); - ensures true; -@*/ - -extern struct int_queueCell *mallocIntQueueCell(); -/*@ spec mallocIntQueueCell(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern void freeIntQueueCell (struct int_queueCell *p); -/*@ spec freeIntQueueCell(pointer p); - requires take u = Block(p); - ensures true; -@*/ - -/*@ -function [rec] (datatype seq) push (datatype seq xs, i32 y) { - snoc (xs, y) -} - -function [rec] (i32) pop (datatype seq xs, i32 y) { - hd (xs) -} -@*/ diff --git a/src/examples/temp-queue1.broken.c b/src/examples/temp-queue1.broken.c deleted file mode 100644 index b6fb4203..00000000 --- a/src/examples/temp-queue1.broken.c +++ /dev/null @@ -1,103 +0,0 @@ -#include "list.h" - - -/*@ function (datatype seq) rev(datatype seq xs) @*/ - - -// N.b.: This is wrong! -/*@ -function [rec] (datatype seq) snoc(datatype seq xs, i32 y) { - match xs { - Seq_Nil {} => { - Seq_Nil {} - } - Seq_Cons {head : h, tail : zs} => { - snoc (rev(zs), h) - } - } -} -@*/ - -struct int_queue { - struct int_queueCell* head; - struct int_queueCell* tail; -}; - -struct int_queueCell { - int first; - struct int_queueCell* next; -}; - -extern struct int_queue *mallocIntQueue(); -/*@ spec mallocIntQueue(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern struct int_queueCell *mallocIntQueueCell(); -/*@ spec mallocIntQueueCell(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -/*@ -predicate (datatype seq) IntQueue(pointer q) { - take H = Owned(q); - take Q = IntQueue1(q,H); - return Q; -} - -predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) { - if (is_null(H.head)) { - assert (is_null(H.tail)); - return (Seq_Nil{}); - } else { - assert (!is_null(H.tail)); - take Q = IntQueueAux (H.head, H.tail); - return Q; - } -} - -predicate (datatype seq) IntQueueAux(pointer h, pointer t) { - take C = Owned(h); - take L = IntQueueAux1(h, C, t); - return L; -} - -predicate (datatype seq) IntQueueAux1 - (pointer h, struct int_queueCell C, pointer t) { - if (is_null(C.next)) { - assert (h == t); - return (Seq_Cons{head: C.first, tail: Seq_Nil{}}); - } else { - take TL = IntQueueAux(C.next, t); - return (Seq_Cons { head: C.first, tail: TL }); - } -} -@*/ - -/*@ -lemma snac_nil (i32 foo) - requires true; - ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}}; -@*/ - -void IntQueue_push (int x, struct int_queue *q) -/*@ requires take l = IntQueue(q); - ensures take ret = IntQueue(q); - ret == snoc (l, x); -@*/ -{ - struct int_queueCell *c = mallocIntQueueCell(); - c->first = x; - c->next = 0; - if (q->tail == 0) { - q->head = c; - q->tail = c; - } else { - q->tail->next = c; - q->tail = c; - } -} diff --git a/src/examples/temp-queue1a.broken.c b/src/examples/temp-queue1a.broken.c deleted file mode 100644 index ffccf7ab..00000000 --- a/src/examples/temp-queue1a.broken.c +++ /dev/null @@ -1,99 +0,0 @@ -#include "list.h" - -// Fixed version -/*@ -function [rec] (datatype seq) snoc(datatype seq xs, i32 y) { - match xs { - Seq_Nil {} => { - Seq_Cons {head: y, tail: Seq_Nil{}} - } - Seq_Cons {head: x, tail: zs} => { - Seq_Cons{head: x, tail: snoc (zs, y)} - } - } -} -@*/ - -struct int_queue { - struct int_queueCell* head; - struct int_queueCell* tail; -}; - -struct int_queueCell { - int first; - struct int_queueCell* next; -}; - -extern struct int_queue *mallocIntQueue(); -/*@ spec mallocIntQueue(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern struct int_queueCell *mallocIntQueueCell(); -/*@ spec mallocIntQueueCell(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -/*@ -predicate (datatype seq) IntQueue(pointer q) { - take H = Owned(q); - take Q = IntQueue1(q,H); - return Q; -} - -predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) { - if (is_null(H.head)) { - assert (is_null(H.tail)); - return (Seq_Nil{}); - } else { - assert (!is_null(H.tail)); - take Q = IntQueueAux (H.head, H.tail); - return Q; - } -} - -predicate (datatype seq) IntQueueAux(pointer h, pointer t) { - take C = Owned(h); - take L = IntQueueAux1(h, C, t); - return L; -} - -predicate (datatype seq) IntQueueAux1 - (pointer h, struct int_queueCell C, pointer t) { - if (is_null(C.next)) { - assert (h == t); - return (Seq_Cons{head: C.first, tail: Seq_Nil{}}); - } else { - take TL = IntQueueAux(C.next, t); - return (Seq_Cons { head: C.first, tail: TL }); - } -} -@*/ - -/*@ -lemma snac_nil (i32 foo) - requires true; - ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}}; -@*/ - -void IntQueue_push (int x, struct int_queue *q) -/*@ requires take l = IntQueue(q); - ensures take ret = IntQueue(q); - ret == snoc (l, x); -@*/ -{ - struct int_queueCell *c = mallocIntQueueCell(); - c->first = x; - c->next = 0; - if (q->tail == 0) { - q->head = c; - q->tail = c; - } else { - q->tail->next = c; - q->tail = c; - } -} diff --git a/src/examples/temp-queue1b.broken.c b/src/examples/temp-queue1b.broken.c deleted file mode 100644 index 6c49e1de..00000000 --- a/src/examples/temp-queue1b.broken.c +++ /dev/null @@ -1,101 +0,0 @@ -#include "list.h" - -// Fixed version -/*@ -function [rec] (datatype seq) snoc(datatype seq xs, i32 y) { - match xs { - Seq_Nil {} => { - Seq_Cons {head: y, tail: Seq_Nil{}} - } - Seq_Cons {head: x, tail: zs} => { - Seq_Cons{head: x, tail: snoc (zs, y)} - } - } -} -@*/ - -struct int_queue { - struct int_queueCell* head; - struct int_queueCell* tail; -}; - -struct int_queueCell { - int first; - struct int_queueCell* next; -}; - -extern struct int_queue *mallocIntQueue(); -/*@ spec mallocIntQueue(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern struct int_queueCell *mallocIntQueueCell(); -/*@ spec mallocIntQueueCell(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -/*@ -predicate (datatype seq) IntQueue(pointer q) { - take H = Owned(q); - take Q = IntQueue1(q,H); - return Q; -} - -predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) { - if (is_null(H.head)) { - assert (is_null(H.tail)); - return (Seq_Nil{}); - } else { - assert (!is_null(H.tail)); - take Q = IntQueueAux (H.head, H.tail); - return Q; - } -} - -predicate (datatype seq) IntQueueAux(pointer h, pointer t) { - take C = Owned(h); - take L = IntQueueAux1(h, C, t); - return L; -} - -predicate (datatype seq) IntQueueAux1 - (pointer h, struct int_queueCell C, pointer t) { - if (is_null(C.next)) { - assert (h == t); - return (Seq_Cons{head: C.first, tail: Seq_Nil{}}); - } else { - take TL = IntQueueAux(C.next, t); - return (Seq_Cons { head: C.first, tail: TL }); - } -} -@*/ - -/*@ -lemma snac_nil (i32 foo) - requires true; - ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}}; -@*/ - -void IntQueue_push (int x, struct int_queue *q) -/*@ requires take l = IntQueue(q); - ensures take ret = IntQueue(q); - ret == snoc (l, x); -@*/ -{ - struct int_queueCell *c = mallocIntQueueCell(); - c->first = x; - c->next = 0; - if (q->tail == 0) { - q->head = c; - q->tail = c; - return; - } else { - q->tail->next = c; - q->tail = c; - return; - } -} diff --git a/src/examples/temp-queue1c.broken.c b/src/examples/temp-queue1c.broken.c deleted file mode 100644 index b358ee98..00000000 --- a/src/examples/temp-queue1c.broken.c +++ /dev/null @@ -1,114 +0,0 @@ -#include "list.h" - -// Broken snoc -/*@ -function [rec] (datatype seq) rev(datatype seq xs) { - match xs { - Seq_Nil {} => { - Seq_Nil {} - } - Seq_Cons {head : h, tail : zs} => { - snoc (rev(zs), h) - } - } -} - -function [rec] (datatype seq) snoc(datatype seq xs, i32 y) { - match xs { - Seq_Nil {} => { - Seq_Nil {} - } - Seq_Cons {head : h, tail : zs} => { - snoc (rev(zs), h) - } - } -} -@*/ - -struct int_queue { - struct int_queueCell* head; - struct int_queueCell* tail; -}; - -struct int_queueCell { - int first; - struct int_queueCell* next; -}; - -extern struct int_queue *mallocIntQueue(); -/*@ spec mallocIntQueue(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern struct int_queueCell *mallocIntQueueCell(); -/*@ spec mallocIntQueueCell(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -/*@ -predicate (datatype seq) IntQueue(pointer q) { - take H = Owned(q); - assert ((is_null(H.head) && is_null(H.tail)) || (!is_null(H.head) && !is_null(H.tail))); - take Q = IntQueue1(q,H); - return Q; -} - -predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) { - if (is_null(H.head)) { - assert (is_null(H.tail)); - return (Seq_Nil{}); - } else { - assert (!is_null(H.tail)); - take Q = IntQueueAux (H.head, H.tail); - return Q; - } -} - -predicate (datatype seq) IntQueueAux(pointer h, pointer t) { - take C = Owned(h); - take L = IntQueueAux1(h, C, t); - return L; -} - -predicate (datatype seq) IntQueueAux1 - (pointer h, struct int_queueCell C, pointer t) { - if (is_null(C.next)) { - assert (h == t); - return (Seq_Cons{head: C.first, tail: Seq_Nil{}}); - } else { - take TL = IntQueueAux(C.next, t); - return (Seq_Cons { head: C.first, tail: TL }); - } -} -@*/ - -/*@ -lemma snac_nil (i32 foo) - requires true; - ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}}; -@*/ - -void IntQueue_push (int x, struct int_queue *q) -/*@ requires take l = IntQueue(q); - ensures take ret = IntQueue(q); - ret == snoc (l, x); -@*/ -{ - struct int_queueCell *c = mallocIntQueueCell(); - c->first = x; - c->next = 0; - if (q->tail == 0) { - q->head = c; - q->tail = c; - /*@ unfold snoc(l,x); @*/ - return; - } else { - q->tail->next = c; - q->tail = c; - return; - } -} diff --git a/src/examples/temp-queue2.broken.c b/src/examples/temp-queue2.broken.c deleted file mode 100644 index 755869ea..00000000 --- a/src/examples/temp-queue2.broken.c +++ /dev/null @@ -1,89 +0,0 @@ -#include "list.h" -#include "list_snoc_cn.h" - -/*@ -lemma snac_nil (i32 foo) - requires true; - ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}}; -@*/ - -struct int_queue { - struct int_queueCell* head; - struct int_queueCell* tail; -}; - -struct int_queueCell { - int first; - struct int_queueCell* next; -}; - -extern struct int_queue *mallocIntQueue(); -/*@ spec mallocIntQueue(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern struct int_queueCell *mallocIntQueueCell(); -/*@ spec mallocIntQueueCell(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -/*@ -predicate (datatype seq) IntQueue(pointer q) { - take H = Owned(q); - take Q = IntQueue1(q,H); - return Q; -} - -predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) { - if (is_null(H.head)) { - assert (is_null(H.tail)); - return (Seq_Nil{}); - } else { - assert (!is_null(H.tail)); - take Q = IntQueueAux (H.head, H.tail); - return Q; - } -} - -predicate (datatype seq) IntQueueAux(pointer h, pointer t) { - take C = Owned(h); - take L = IntQueueAux1(h, C, t); - return L; -} - -predicate (datatype seq) IntQueueAux1 - (pointer h, struct int_queueCell C, pointer t) { - if (is_null(C.next)) { - assert (h == t); - return (Seq_Cons{head: C.first, tail: Seq_Nil{}}); - } else { - take TL = IntQueueAux(C.next, t); - return (Seq_Cons { head: C.first, tail: TL }); - } -} - -@*/ - -void IntQueue_push (int x, struct int_queue *q) -/*@ requires take l = IntQueue(q); - ensures take ret = IntQueue(q); - ret == snoc (l, x); -@*/ -{ - struct int_queueCell *c = mallocIntQueueCell(); - c->first = x; - c->next = 0; - if (q->tail == 0) { - /*@ split_case (*q).head == NULL; @*/ - /*@ apply snac_nil(x); @*/ - q->head = c; - q->tail = c; - } else { - q->tail->next = c; - q->tail = c; - } -} diff --git a/src/examples/temp-queue3.broken.c b/src/examples/temp-queue3.broken.c deleted file mode 100644 index 9147f4de..00000000 --- a/src/examples/temp-queue3.broken.c +++ /dev/null @@ -1,133 +0,0 @@ -/* queue.c */ - -#include "list.h" -#include "list_snoc_cn.h" - -/*@ -lemma snoc_nil (i32 foo) - requires true; - ensures snoc (Seq_Nil{}, foo) == Seq_Cons {head: foo, tail: Seq_Nil{}}; -@*/ - -struct int_queue { - struct int_queueCell* head; - struct int_queueCell* tail; -}; - -struct int_queueCell { - int first; - struct int_queueCell* next; -}; - -/*@ -predicate (datatype seq) IntQueue (pointer q) { - take H = Owned(q); - take Q = IntQueue1(q,H); - return Q; -} - -predicate (datatype seq) IntQueue1 (pointer dummy, struct int_queue H) { - if (is_null(H.head) || is_null(H.tail)) { - assert (is_null(H.head) && is_null(H.tail)); - return (Seq_Nil{}); - } else { - assert (!is_null(H.head) && !is_null(H.tail)); - take T = Owned(H.tail); - assert (is_null(T.next)); - take Q = IntQueueAux (H.head, H.tail, T.first); - return Q; - } -} - -predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) { - if (h == t) { - return (Seq_Cons{head: lastVal, tail: Seq_Nil{}}); - } else { - take C = Owned(h); - take TL = IntQueueAux(C.next, t, lastVal); - return (Seq_Cons { head: C.first, tail: TL }); - } -} - -@*/ - -// --------------------------------------------------------------------- - -extern struct int_queue *mallocIntQueue(); -/*@ spec mallocIntQueue(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern void freeIntQueue (struct int_queue *p); -/*@ spec freeIntQueue(pointer p); - requires take u = Block(p); - ensures true; -@*/ - -extern struct int_queueCell *mallocIntQueueCell(); -/*@ spec mallocIntQueueCell(); - requires true; - ensures take u = Block(return); - return != NULL; -@*/ // 'return != NULL' should not be needed - -extern void freeIntQueueCell (struct int_queueCell *p); -/*@ spec freeIntQueueCell(pointer p); - requires take u = Block(p); - ensures true; -@*/ - -// ----------------------------------------------------------------- - -struct int_queue* IntQueue_empty () -/*@ ensures take ret = IntQueue(return); - ret == Seq_Nil{}; -@*/ -{ - struct int_queue *p = mallocIntQueue(); - p->head = 0; - p->tail = 0; - return p; -} - -int IntQueue_pop (struct int_queue *q) -/*@ requires take before = IntQueue(q); - before != Seq_Nil{}; - ensures take after = IntQueue(q); - after == tl(before); - return == hd(before); -@*/ -{ - /*@ split_case (*q).head == NULL; @*/ - /*@ split_case (*q).tail == NULL; @*/ - // This is needed to unfold IntQueueAux, I guess? - /*@ split_case (*q).head == (*q).tail; @*/ - struct int_queueCell* h = q->head; - /*@ split_case (*h).next == NULL; @*/ - int x = h->first; - if (h->next == 0) { - // This line was missing originally -- good pedagogy to fix in stages?? - freeIntQueueCell(h); - q->head = 0; - q->tail = 0; - return x; - } else { - // Needs to deallocate here too! - q->head = h->next; - return x; - } - // The return was originally here -- make sure to comment on why it got moved! -} - -// Notes: -// - When I tried /*@ unfold IntQueueAux (H.head, H.tail, T.first); @*/ -// I was confused by "the specification function `IntQueueAux' is not declared". -// I guess this is, again, the distinction between functions and predicates...? -// - Seq_Cons is awkward for several reasons: -// - long / verbose (nothing to do about that, I guess) -// - Seq is capitalized, but it means seq -// - most important part is buried in the middle -// - What are the established C conventions here?? -// - lastVal can be eliminated, I think