Merge pull request #50 from JudySun233/new_gvc0_examples

add verified gvc0 codes for minimum priority queue and stack

src/test/resources/quant-study/new-examples/minprique.c0

@@ -0,0 +1,224 @@
+#use <conio>
+#use <stress>
+struct Node {
+    int val;
+    struct Node *next;
+    bool deleted;
+};
+typedef struct Node Node;
+
+struct MinPriorityQueue {
+    Node *head;
+    int size;
+};
+typedef struct MinPriorityQueue MinPriorityQueue;
+
+/*@
+predicate orderedListSegWithPrev(struct Node *start, struct Node *end, int prev, int endVal) =
+  (start == end) ?
+    ( (end == NULL) ? true : endVal >= prev )
+    :
+    (
+      acc(start->val) && acc(start->next) && acc(start->deleted) &&
+      start->val >= prev && orderedListSegWithPrev(start->next, end, start->val, endVal)
+    ) ;
+@*/
+
+/*@
+predicate orderedListSeg(struct Node *start, struct Node *end, int endVal) =
+  (start == end) ?
+    ( true )
+    :
+    (
+      acc(start->val) && acc(start->next) && acc(start->deleted) &&
+      orderedListSegWithPrev(start->next, end, start->val, endVal)
+    ) ;
+@*/
+
+/*@
+predicate isMinPQ(Node *start) =
+  orderedListSeg(start, NULL, -1);
+@*/
+
+//-------------------------------------------------------------------lemmas
+// Lemma:
+void appendLemmaLoopBody(struct Node *a, struct Node *b, struct Node *c, int aPrev, int cPrev, int bVal, int cVal, bool bDeleted)
+  /*@
+    requires orderedListSegWithPrev(a, b, aPrev, bVal) &&
+        ( (b == c) ? bVal == cVal : true ) &&
+        ( (c == NULL) ?
+            ( true )
+            :
+            ( acc(c->val) && acc(c->next) && acc(c->deleted) && c->val == cVal &&
+              c->val >= cPrev && orderedListSegWithPrev(c->next, NULL, c->val, -1)
+            )
+        ) &&
+        ( (b == c) ?
+            ( true )
+            :
+            (
+              acc(b->val) && acc(b->next) && acc(b->deleted) && b->val == bVal &&
+              orderedListSegWithPrev(b->next, c, b->val, cVal)
+            )
+        ) ;
+  @*/
+  /*@
+    ensures orderedListSegWithPrev(a, c, aPrev, cVal) &&
+        ( (c == NULL) ?
+            ( true )
+            :
+            ( acc(c->val) && acc(c->next) && acc(c->deleted) && c->val == cVal &&
+              c->val >= cPrev && orderedListSegWithPrev(c->next, NULL, c->val, -1)
+            )
+        ) ;
+  @*/
+{
+  if (b == c) {
+  } else if (a == b) {
+    //@ unfold orderedListSegWithPrev(a, b, aPrev, bVal);
+    //@ fold orderedListSegWithPrev(a, c, aPrev, cVal);
+  } else {
+    //@ unfold orderedListSegWithPrev(a, b, aPrev, bVal);
+    appendLemmaLoopBody(a->next, b, c, a->val, cPrev, bVal, cVal, b->deleted);
+    //@ fold orderedListSegWithPrev(a, c, aPrev, cVal);
+  }
+}
+
+void appendLemmaAfterLoopBody(struct Node *a, struct Node *b, struct Node *c, int aPrev, int bVal, int cVal, bool bDeleted)
+  /*@
+    requires orderedListSegWithPrev(a, b, aPrev, bVal) &&
+        ( (b == c) ? bVal == cVal : true ) &&
+        ( (c == NULL) ? true : acc(c->val) && acc(c->next) && acc(c->deleted) && c->val == cVal ) &&
+        ( (b == c) ?
+            ( true )
+            :
+            (
+              acc(b->val) && acc(b->next) && acc(b->deleted) && b->val == bVal &&
+              orderedListSegWithPrev(b->next, c, b->val, cVal)
+            )
+        ) ;
+  @*/
+  /*@
+    ensures orderedListSegWithPrev(a, c, aPrev, cVal) &&
+        ( (c == NULL) ? true : acc(c->val) && acc(c->next) && acc(c->deleted) && c->val == cVal) ;
+  @*/
+{
+  if (b == c) {
+  } else if (a == b) {
+    //@ unfold orderedListSegWithPrev(a, b, aPrev, bVal);
+    //@ fold orderedListSegWithPrev(a, c, aPrev, cVal);
+  } else {
+    //@ unfold orderedListSegWithPrev(a, b, aPrev, bVal);
+    appendLemmaAfterLoopBody(a->next, b, c, a->val, bVal, cVal, b->deleted);
+    //@ fold orderedListSegWithPrev(a, c, aPrev, cVal);
+  }
+}
+
+//-------------------------------------------------------------------verified code starts below
+
+MinPriorityQueue* createMinPriQueue(int value) 
+    //@ requires true;
+    //@ ensures acc((\result)->size) && acc((\result)->head) && isMinPQ((\result)->head);
+{
+    MinPriorityQueue *q = alloc(struct MinPriorityQueue);
+    q->head = alloc(struct Node);
+    q->head->val = value;
+    q->head->next = NULL;
+    q->size = 1;
+    //@ fold orderedListSegWithPrev(q->head->next, NULL, q->head->val, -1);
+    //@ fold orderedListSeg(q->head, NULL, -1);
+    //@ fold isMinPQ(q->head);
+    return q;
+}
+
+void enqueue(MinPriorityQueue *q, int value) 
+    //@ requires acc(q->head) && acc(q->size) && isMinPQ(q->head);
+    //@ ensures acc(q->head) && acc(q->size) && isMinPQ(q->head);
+{
+    //@ unfold isMinPQ(q->head);
+    //@ unfold orderedListSeg(q->head, NULL, -1);
+    if (q->head == NULL || value <= q->head->val) { // insert at head
+        Node *newNode = alloc(struct Node);
+        newNode->val = value;
+        newNode->next = q->head;
+        q->head = newNode;  
+        //@ fold orderedListSegWithPrev(newNode->next, NULL, newNode->val, -1);
+        //@ fold orderedListSeg(q->head, NULL, -1);
+        //@ fold isMinPQ(q->head);
+    } else { // insert after head
+        Node *curr = q->head;
+        //@ unfold orderedListSegWithPrev(curr->next, NULL, curr->val, -1);
+        //@ fold orderedListSeg(q->head, curr, curr->val);
+        while (curr->next != NULL && curr->next->val < value) 
+        //@ loop_invariant acc(curr->val) && acc(curr->next) && acc(curr->deleted);
+        //@ loop_invariant acc(q->head);
+        //@ loop_invariant orderedListSeg(q->head, curr, curr->val) && curr->val <= value;
+        //@ loop_invariant (curr->next == NULL) ? (true) : acc(curr->next->next) && acc(curr->next->val) && acc(curr->next->deleted) && curr->next->val >= curr->val && orderedListSegWithPrev(curr->next->next, NULL, curr->next->val, -1);
+        { 
+            Node *prev = curr;
+            curr = prev->next;
+            //@ unfold orderedListSeg(q->head, prev, prev->val);
+            //@ fold orderedListSegWithPrev(prev->next, curr, prev->val, curr->val);
+
+            if (q->head == prev) {
+            } else {
+              appendLemmaLoopBody(q->head->next, prev, curr, q->head->val, prev->val, prev->val, curr->val, prev->deleted);
+            }
+
+            //@ fold orderedListSeg(q->head, curr, curr->val);
+            //@ unfold orderedListSegWithPrev(curr->next, NULL, curr->val, -1);
+        }
+        struct Node *newNode = alloc(struct Node);
+        newNode->val = value;
+        newNode->next = curr->next;
+        newNode->deleted = false;
+        curr->next = newNode;
+        //@ fold orderedListSegWithPrev(newNode->next, NULL, newNode->val, -1);
+        //@ fold orderedListSegWithPrev(curr->next, NULL, curr->val, -1);
+
+        //@ unfold orderedListSeg(q->head, curr, curr->val);
+        if (q->head == curr) {
+        } else {
+          appendLemmaAfterLoopBody(q->head->next, curr, NULL, q->head->val, curr->val, -1, q->head->deleted);
+        }
+
+        //@ fold orderedListSeg(q->head, NULL, -1);
+        //@ fold isMinPQ(q->head);
+    }
+    q->size++;
+}
+
+void dequeue(MinPriorityQueue *q) 
+    //@ requires acc(q->head) && acc(q->size) && isMinPQ(q->head);
+    //@ ensures acc(q->head) && acc(q->size) && isMinPQ(q->head);
+{
+    //@ unfold isMinPQ(q->head);
+    //@ unfold orderedListSeg(q->head, NULL, -1);
+    if (q->head == NULL) {
+        // Queue is empty, nothing to dequeue
+        //@ fold orderedListSeg(q->head, NULL, -1);
+        //@ fold isMinPQ(q->head);
+        return;
+    } else {
+        //@ unfold orderedListSegWithPrev(q->head->next, NULL, q->head->val, -1);
+        q->head->deleted = true; // Mark node as deleted
+        //@ fold orderedListSegWithPrev(q->head->next, NULL, q->head->val, -1);
+        //@ fold orderedListSeg(q->head, NULL, -1);
+        //@ fold isMinPQ(q->head);
+    }
+    q->size--;
+}
+
+int main () 
+    //@ requires true;
+    //@ ensures true;
+{
+    MinPriorityQueue *q = createMinPriQueue(1);
+    enqueue(q, 10);
+    enqueue(q, 5);
+    enqueue(q, 20);
+    dequeue(q);
+    dequeue(q);
+    dequeue(q);
+    return 0;
+}