Changes to the VerifyThis2015 test programs

4 files changed, 45 insertions, 18 deletions

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...