From 8af694583e86b36d8fcc81485ea2f02c9961d96c Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Tue, 28 Apr 2015 19:48:33 -0700
Subject: Changes to the VerifyThis2015 test programs

---
 Test/VerifyThis2015/Problem2.dfy        | 39 +++++++++++++++++++--------------
 Test/VerifyThis2015/Problem2.dfy.expect |  2 +-
 Test/VerifyThis2015/Problem3.dfy        | 20 +++++++++++++++++
 Test/VerifyThis2015/Problem3.dfy.expect |  2 +-
 4 files changed, 45 insertions(+), 18 deletions(-)

(limited to 'Test/VerifyThis2015')

diff --git a/Test/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy
index 84fa924d..1c7deffd 100644
--- a/Test/VerifyThis2015/Problem2.dfy
+++ b/Test/VerifyThis2015/Problem2.dfy
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"
 
 // Rustan Leino
-// 13 April 2015
+// 13 April 2015, and many subsequent enhancements and revisions
 // VerifyThis 2015
 // Problem 2 -- Parallel GCD
 
@@ -109,7 +109,6 @@ method ParallelGcd_WithoutTermination(A: int, B: int) returns (gcd: int)
 method ParallelGcd(A: int, B: int) returns (gcd: int)
   requires A > 0 && B > 0
   ensures gcd == Gcd(A, B)
-  decreases *
 {
   var a, b := A, B;
   var pc0, pc1 := 0, 0;  // program counter for the two processes
@@ -127,12 +126,13 @@ method ParallelGcd(A: int, B: int) returns (gcd: int)
     invariant pc0 == 2 ==> b <= b0 && (b0 <= a0 ==> b0 == b)
     invariant pc1 == 2 ==> a <= a1 && (a1 <= b1 ==> a1 == a)
     invariant (pc0 == 3 ==> a == b) && (pc1 == 3 ==> a == b)
-    invariant 0 <= budget0 && 0 <= budget1 && 1 <= budget0 + budget1
+    invariant 0 <= budget0 && 0 <= budget1 && (pc0 == 3 || pc1 == 3 || 1 <= budget0 + budget1)
     // With the budgets, the program is guaranteed to terminate, as is proved by the following termination
-    // metric (which is a lexicographic triple):
-    decreases *, a + b,
-//              if a == b then 0 else if a < b then budget0 else budget1,
-              (if a0 < b0 then budget0 else 0) + (if b1 < a1 then budget1 else 0),
+    // metric (which is a lexicographic tuple):
+    decreases a + b,
+              FinalStretch(pc0, pc1, a0, b0, b) + FinalStretch(pc1, pc0, b1, a1, a),
+              (if pc0 == 2 && a0 < b0 && !(a < b) then 1 else 0) + (if pc1 == 2 && b1 < a1 && !(b < a) then 1 else 0),
+              (if a < b then budget0 else 0) + (if b < a then budget1 else 0),
               8 - pc0 - pc1
   {
     if {
@@ -166,15 +166,26 @@ method ParallelGcd(A: int, B: int) returns (gcd: int)
   gcd := a;
 }
 
+function FinalStretch(pcThis: int, pcThat: int, a0: int, b0: int, b: int): int
+{
+  if pcThat != 3 then 10  // we're not yet in the final stretch
+  else if pcThis == 3 then 0
+  else if pcThis == 2 && a0 == b0 then 1
+  else if pcThis == 1 && a0 == b then 2
+  else if pcThis == 0 then 3
+  else if pcThis == 2 && a0 < b0 then 4
+  else 5
+}
+
 method BudgetUpdate(inThis: int, inThat: int, pcThat: int) returns (outThis: int, outThat: int)
   requires pcThat == 3 || 0 < inThis
-  ensures pcThat == 3 ==> outThis == inThis && outThat == inThat
-  ensures pcThat != 3 ==> outThis == inThis - 1 && outThat > 0
+  ensures outThis == if 0 < inThis then inThis - 1 else inThis
+  ensures if pcThat == 3 then outThat == inThat else outThat > 0
 {
+  outThis := if 0 < inThis then inThis - 1 else inThis;
   if pcThat == 3 {
-    outThis, outThat := inThis, inThat;
+    outThat := inThat;
   } else {
-    outThis := inThis - 1;
     outThat :| outThat > 0;
   }
 }
@@ -295,11 +306,7 @@ lemma Symmetry(a: int, b: int)
   assert DividesBoth(k, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= k;
   assert DividesBoth(l, b, a) && forall m :: DividesBoth(m, b, a) ==> m <= l;
   assert DividesBoth(l, a, b);
-  forall m | DividesBoth(m, b, a)
-    ensures m <= l && DividesBoth(m, a, b)
-  {
-  }
-  assert forall m :: DividesBoth(m, a, b) ==> m <= l;
+  assert forall m :: DividesBoth(m, b, a) ==> m <= l && DividesBoth(m, a, b);
   assert k == l;
 }
 
diff --git a/Test/VerifyThis2015/Problem2.dfy.expect b/Test/VerifyThis2015/Problem2.dfy.expect
index ad540132..f5e3b3dc 100644
--- a/Test/VerifyThis2015/Problem2.dfy.expect
+++ b/Test/VerifyThis2015/Problem2.dfy.expect
@@ -1,2 +1,2 @@
 
-Dafny program verifier finished with 35 verified, 0 errors
+Dafny program verifier finished with 36 verified, 0 errors
diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
index fb95637d..4205035d 100644
--- a/Test/VerifyThis2015/Problem3.dfy
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -123,3 +123,23 @@ class DoublyLinkedList {
     Nodes := Nodes[..k] + [x] + Nodes[k..];
   }
 }
+
+// --------------------------------------------------------
+// If it were not required to build a data structure (like the class above) that supports the
+// Remove and PutBack operations, the operations can easily be verified to compose into the
+// identity transformation.  The following method shows that the two operations, under a suitable
+// precondition, have no net effect on any .L or .R field.
+
+method Alt(x: Node)
+  requires x != null && x.L != null && x.R != null
+  requires x.L.R == x && x.R.L == x  // links are mirrored
+  modifies x, x.L, x.R
+  ensures forall y: Node :: y != null ==> y.L == old(y.L) && y.R == old(y.R)
+{
+  // remove
+  x.R.L := x.L;
+  x.L.R := x.R;
+  // put back
+  x.R.L := x;
+  x.L.R := x;
+}
diff --git a/Test/VerifyThis2015/Problem3.dfy.expect b/Test/VerifyThis2015/Problem3.dfy.expect
index 9559b9a6..4035605c 100644
--- a/Test/VerifyThis2015/Problem3.dfy.expect
+++ b/Test/VerifyThis2015/Problem3.dfy.expect
@@ -1,5 +1,5 @@
 
-Dafny program verifier finished with 13 verified, 0 errors
+Dafny program verifier finished with 15 verified, 0 errors
 Program compiled successfully
 Running...
 
-- 
cgit v1.2.3