From 57d62186efa929c0623a69453c8e4196ac9803a4 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Mon, 5 Jan 2015 20:35:32 -0800
Subject: Added lemmas that make verification go through faster and more
 reliably

---
 Test/VSI-Benchmarks/b3.dfy        | 41 +++++++++++++++++++++++++++++++++------
 Test/VSI-Benchmarks/b3.dfy.expect |  2 +-
 2 files changed, 36 insertions(+), 7 deletions(-)

(limited to 'Test/VSI-Benchmarks')

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 5a2b6e13..f59b0c3e 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -53,7 +53,7 @@ class Benchmark3 {
     ensures multiset(r.contents) == multiset(old(q.contents));
   {
     r := new Queue<int>.Init();
-    while (|q.contents| != 0)
+    while |q.contents| != 0
       invariant |r.contents| + |q.contents| == |old(q.contents)|;
       invariant forall i, j :: 0 <= i < j < |r.contents| ==> r.contents[i] <= r.contents[j];
       invariant forall i, j ::
@@ -83,29 +83,58 @@ class Benchmark3 {
     k := 0;
     m := q.Head(); 
     var j := 0;
-   
-    while (j < n)
+    while j < n
       invariant j <= n;
       invariant 0 <= k < n && old(q.contents)[k] == m;
       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; //i.e. rotated
       invariant forall i :: 0 <= i < j ==> m <= old(q.contents)[i]; //m is min so far
     {
+      ghost var qc0 := q.contents;
       var x := q.Dequeue();
       q.Enqueue(x);
-      if (x < m) { k := j; m := x; }
+      RotationLemma(old(q.contents), j, qc0, q.contents);
+      if x < m { k := j; m := x; }
       j := j+1;
     }
     
     j := 0;
-    while (j < k)
+    while j < k
       invariant j <= k;
       invariant q.contents == old(q.contents)[j..] + old(q.contents)[..j]; 
     {
+      ghost var qc0 := q.contents;
       var x := q.Dequeue();
       q.Enqueue(x);
+      RotationLemma(old(q.contents), j, qc0, q.contents);
       j := j+1;
     }
-
+  
+    assert j == k;  
+    assert q.contents == old(q.contents)[k..] + old(q.contents)[..k];
     m := q.Dequeue();
   }
+
+  lemma RotationLemma(O: seq, j: nat, A: seq, C: seq)
+    requires j < |O|;
+    requires A == O[j..] + O[..j];
+    requires C == A[1..] + [O[j]];
+    ensures C == O[j+1..] + O[..j+1];
+  {
+    calc {
+      A;
+      O[j..] + O[..j];
+      O[j..j+1] + O[j+1..] + O[..j];
+      O[j..j+1] + (O[j+1..] + O[..j]);
+    }
+    calc {
+      C;
+      A[1..] + [A[0]];
+      { assert A[0] == O[j] && A[1..] == O[j+1..] + O[..j]; }
+      O[j+1..] + O[..j] + [O[j]];
+      { assert [O[j]] == O[j..j+1]; }
+      O[j+1..] + O[..j] + O[j..j+1];
+      O[j+1..] + (O[..j] + O[j..j+1]);
+      O[j+1..] + O[..j+1];
+    }
+  }
 }
diff --git a/Test/VSI-Benchmarks/b3.dfy.expect b/Test/VSI-Benchmarks/b3.dfy.expect
index c87e2af2..b9a9bc89 100644
--- a/Test/VSI-Benchmarks/b3.dfy.expect
+++ b/Test/VSI-Benchmarks/b3.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 10 verified, 0 errors
+Dafny program verifier finished with 12 verified, 0 errors
-- 
cgit v1.2.3