Completed problems from the VerifyThis 2015 program verification competition

6 files changed, 685 insertions, 0 deletions

diff --git a/Test/VerifyThis2015/Problem1.dfy b/Test/VerifyThis2015/Problem1.dfy
new file mode 100644
index 00000000..2e8a5243
--- /dev/null
+++ b/Test/VerifyThis2015/Problem1.dfy
@@ -0,0 +1,188 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// Rustan Leino

+// 12 April 2015

+// VerifyThis 2015

+// Problem 1 -- Relaxed Prefix

+

+// The property IsRelaxedPrefix is defined in terms of an auxiliary function.  The

+// auxiliary function allows a given number (here, 1) of elements to be dropped from

+// the pattern.

+predicate IsRelaxedPrefix<T>(pat: seq<T>, a: seq<T>)

+{

+  IsRelaxedPrefixAux(pat, a, 1)

+}

+

+// This predicate returns whether or not "pat", dropping up to "slack" elements, is

+// a prefix of "a".

+predicate IsRelaxedPrefixAux<T>(pat: seq<T>, a: seq<T>, slack: nat)

+{

+  // if "pat" is the empty sequence, the property holds trivially, regardless of the slack

+  if pat == [] then true

+  // if both "pat" and "a" are nonempty and they agree on their first element, then the property

+  // holds iff it holds of their drop-1 suffixes

+  else if a != [] && pat[0] == a[0] then IsRelaxedPrefixAux(pat[1..], a[1..], slack)

+  // if either "a" is empty or "pat" and "a" disagree on their first element, then the property

+  // holds iff there's any slack left and the property holds after spending 1 slack unit and dropping

+  // the first element of the pattern

+  else slack > 0 && IsRelaxedPrefixAux(pat[1..], a, slack-1)

+}

+

+// Here is the corrected reference implementation.  The specification says to return true iff

+// "pat" is a relaxed prefix of "a".

+method ComputeIsRelaxedPrefix<T(==)>(pat: seq<T>, a: seq<T>) returns (b: bool)

+  ensures b == IsRelaxedPrefix(pat, a)

+{

+  // This implementation is the given reference implementation but with two corrections.  One

+  // correction is the out-of-bounds error in the indexing of "a".  This is corrected here by

+  // strengthening the guard of the while loop.  The other correction is that after the loop, the

+  // property still holds if "a" has been exhausted but the number of elements left to inspect in

+  // the pattern does not exceed the number of elements we are still allowed to drop.  (There are

+  // other ways the given reference implementation could have been fixed as well.)

+  ghost var B := IsRelaxedPrefixAux(pat, a, 1);  // the answer we want

+  var shift, i := 0, 0;

+  while i < |pat| && i-shift < |a|

+    invariant 0 <= i <= |pat| && i-shift <= |a|

+    invariant 0 <= shift <= i

+    invariant IsRelaxedPrefixAux(pat[i..], a[i-shift..], 1-shift) == B

+  {

+    if pat[i] != a[i-shift] {

+      if shift == 0 {

+        shift := 1;

+      } else {

+        return false;

+      }

+    }

+    i := i + 1;

+  }

+  return i - shift <= |pat| <= i - shift + 1;

+}

+

+method Main()

+{

+  var a := [1,3,2,3];

+  var b := ComputeIsRelaxedPrefix([1,3], a);

+  print b, "\n";

+  b := ComputeIsRelaxedPrefix([1,2,3], a);

+  print b, "\n";

+  b := ComputeIsRelaxedPrefix([1,2,4], a);

+  print b, "\n";

+}

+

+// Here is an alternative definition of IsRelaxedPrefix.  Perhaps this definition more obviously

+// follows the English description of "relaxed prefix" given in the problem statement.

+predicate IRP_Alt<T>(pat: seq<T>, a: seq<T>)

+{

+  // "pat" is a relaxed prefix of "a"

+  // if "pat" is an actual prefix of "a"

+  pat <= a ||

+  // or if after dropping one element from "pat", namely the one at an index "k", then the result

+  // is a prefix of "a"

+  exists k :: 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a

+}

+

+// We prove that the alternate definition is the same as the one given above.

+lemma AreTheSame_Theorem<T>(pat: seq<T>, a: seq<T>)

+  ensures IsRelaxedPrefix(pat, a) == IRP_Alt(pat, a)

+{

+  // Prove <==

+  if IRP_Alt(pat, a) {

+    if pat <= a {

+      Same0(pat, a);

+    } else if exists k :: 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a {

+      var k :| 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a;

+      Same1(pat, a, k);

+    }

+    assert IsRelaxedPrefix(pat, a);

+  }

+  // Prove ==>

+  if IsRelaxedPrefix(pat, a) {

+    Same2(pat, a);

+    assert IRP_Alt(pat, a);

+  }

+}

+lemma Same0<T>(pat: seq<T>, a: seq<T>)

+  requires pat <= a

+  ensures IsRelaxedPrefixAux(pat, a, 1)

+{

+}

+lemma Same1<T>(pat: seq<T>, a: seq<T>, k: nat)

+  requires 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a

+  ensures IsRelaxedPrefixAux(pat, a, 1)

+{

+  // "k" gives one splitting point, but we want to last splitting point

+  var d := k;

+  while d+1 < |pat| && pat[d] == pat[d+1] 

+    invariant 0 <= d < |pat| && pat[..d] + pat[d+1..] <= a

+  {

+    d := d + 1;

+  }

+  Same1_Aux(pat, a, d);

+}

+lemma Same1_Aux<T>(pat: seq<T>, a: seq<T>, k: nat)

+  requires 0 <= k < |pat| && pat[..k] + pat[k+1..] <= a && (k+1 == |pat| || pat[k] != pat[k+1])

+  ensures IsRelaxedPrefixAux(pat, a, 1)

+{

+  if k+1 == |pat| {

+    assert pat[..k] + pat[k+1..] == pat[..k] <= a;

+    if k == 0 {

+    } else {

+      assert IsRelaxedPrefixAux(pat, a, 1) == IsRelaxedPrefixAux(pat[1..], a[1..], 1);

+      Same1_Aux(pat[1..], a[1..], k-1);

+    }

+  } else if k == 0 {

+    assert pat[..0] + pat[1..] == pat[1..];

+    assert pat[1] == a[0];

+    assert pat[0] != pat[1];

+    assert IsRelaxedPrefixAux(pat, a, 1) == IsRelaxedPrefixAux(pat[1..], a, 0);

+    Prefix(pat[1..], a);

+  } else {

+    calc ==> {

+      true;

+      pat[..k] + pat[k+1..] <= a;

+      (pat[..k] + pat[k+1..])[1..] <= a[1..];

+      pat[..k][1..] + pat[k+1..] <= a[1..];

+      { assert pat[..k][1..] == pat[1..][..k-1]; }

+      pat[1..][..k-1] + pat[k+1..] <= a[1..];

+      { assert pat[k+1..] == pat[1..][k..]; }

+      pat[1..][..k-1] + pat[1..][k..] <= a[1..];

+    }

+    Same1_Aux(pat[1..], a[1..], k-1);

+  }

+}

+lemma Prefix<T>(pat: seq<T>, a: seq<T>)

+  requires pat <= a

+  ensures IsRelaxedPrefixAux(pat, a, 0)

+{

+}

+lemma Same2<T>(pat: seq<T>, a: seq<T>)

+  requires IsRelaxedPrefixAux(pat, a, 1)

+  ensures IRP_Alt(pat, a)

+{

+  if pat == [] {

+    assert pat <= a;

+  } else if a != [] && pat[0] == a[0] {

+    assert IsRelaxedPrefixAux(pat[1..], a[1..], 1);

+    Same2(pat[1..], a[1..]);

+    if pat[1..] <= a[1..] {

+      assert pat <= a;

+    } else {

+      var k :| 0 <= k < |pat[1..]| && pat[1..][..k] + pat[1..][k+1..] <= a[1..];

+      assert 0 <= k+1 < |pat| && pat[..k+1] + pat[k+2..] <= a;

+    }

+  } else {

+    assert IsRelaxedPrefixAux(pat[1..], a, 0);

+    Same2_Prefix(pat[1..], a);

+    assert pat[1..] <= a;

+    assert 0 <= 0 < |pat| && pat[..0] + pat[0+1..] <= a;

+  }

+}

+lemma Same2_Prefix<T>(pat: seq<T>, a: seq<T>)

+  requires IsRelaxedPrefixAux(pat, a, 0)

+  ensures pat <= a

+{

+  if pat != [] {

+    Same2_Prefix(pat[1..], a[1..]);

+  }

+}

diff --git a/Test/VerifyThis2015/Problem1.dfy.expect b/Test/VerifyThis2015/Problem1.dfy.expect
new file mode 100644
index 00000000..3d021945
--- /dev/null
+++ b/Test/VerifyThis2015/Problem1.dfy.expect
@@ -0,0 +1,8 @@
+

+Dafny program verifier finished with 21 verified, 0 errors

+Program compiled successfully

+Running...

+

+True
+True
+False
diff --git a/Test/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy
new file mode 100644
index 00000000..84fa924d
--- /dev/null
+++ b/Test/VerifyThis2015/Problem2.dfy
@@ -0,0 +1,357 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// Rustan Leino

+// 13 April 2015

+// VerifyThis 2015

+// Problem 2 -- Parallel GCD

+

+method SequentialGcd(A: int, B: int) returns (gcd: int)

+  requires A > 0 && B > 0

+  ensures gcd == Gcd(A, B)

+{

+  var a, b := A, B;

+  while

+    invariant 0 < a && 0 < b

+    invariant Gcd(A, B) == Gcd(a, b)

+    decreases a + b

+  {

+    case a > b =>

+      GcdDecrease(a, b);

+      a := a - b;

+    case b > a =>

+      calc {

+        Gcd(a, b);

+        { Symmetry(a, b); }

+        Gcd(b, a);

+        { GcdDecrease(b, a); }

+        Gcd(b - a, a);

+        { Symmetry(b - a, a); }

+        Gcd(a, b - a);

+      }

+      b := b - a;

+  }

+  GcdEqual(a);

+  return a;

+}

+

+method ParallelGcd_ReadAB_WithoutTermination(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

+  var a0, b0, a1, b1;  // local variables for the two processes

+  while !(pc0 == 2 && pc1 == 2)

+    invariant 0 < a && 0 < b

+    invariant Gcd(A, B) == Gcd(a, b)

+    invariant 0 <= pc0 < 3 && 0 <= pc1 < 3

+    invariant pc0 == 1 && b0 <= a0 ==> a0 == a && b0 == b

+    invariant pc1 == 1 && a1 <= b1 ==> a1 == a && b1 == b

+    invariant (pc0 == 2 ==> a == b) && (pc1 == 2 ==> a == b)

+    decreases *

+  {

+    if {

+      case pc0 == 0              => a0, b0, pc0 := a, b, 1;

+      case pc0 == 1 && b0 < a0   => GcdDecrease(a, b);

+                                    a, pc0 := a0 - b0, 0;

+      case pc0 == 1 && b0 > a0  => pc0 := 0;

+      case pc0 == 1 && b0 == a0 => pc0 := 2;  // move into a halting state

+      case pc1 == 0             => a1, b1, pc1 := a, b, 1;

+      case pc1 == 1 && a1 < b1  => Symmetry(a, b); GcdDecrease(b, a); Symmetry(b - a, a);

+                                   b, pc1 := b1 - a1, 0;

+      case pc1 == 1 && a1 > b1  => pc1 := 0;

+      case pc1 == 1 && a1 == b1 => pc1 := 2;  // move into a halting state

+    }

+  }

+  GcdEqual(a);

+  gcd := a;

+}

+

+method ParallelGcd_WithoutTermination(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

+  var a0, b0, a1, b1;  // local variables for the two processes

+  while !(pc0 == 3 && pc1 == 3)

+    invariant 0 < a && 0 < b

+    invariant Gcd(A, B) == Gcd(a, b)

+    invariant 0 <= pc0 < 4 && 0 <= pc1 < 4

+    invariant (pc0 == 0 || a0 == a) && (pc1 == 0 || b1 == b)

+    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)

+    decreases *

+  {

+    if {

+      case pc0 == 0             => a0, pc0 := a, 1;

+      case pc0 == 1             => b0, pc0 := b, 2;

+      case pc0 == 2 && a0 > b0  => GcdDecrease(a, b);

+                                   a, pc0 := a0 - b0, 0;

+      case pc0 == 2 && a0 < b0  => pc0 := 0;

+      case pc0 == 2 && a0 == b0 => pc0 := 3;

+      case pc1 == 0             => b1, pc1 := b, 1;

+      case pc1 == 1             => a1, pc1 := a, 2;

+      case pc1 == 2 && b1 > a1  => Symmetry(a, b); GcdDecrease(b, a); Symmetry(b - a, a);

+                                   b, pc1 := b1 - a1, 0;

+      case pc1 == 2 && b1 < a1  => pc1 := 0;

+      case pc1 == 2 && b1 == a1 => pc1 := 3;

+    }

+  }

+  GcdEqual(a);

+  gcd := a;

+}

+

+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

+  var a0, b0, a1, b1;  // local variables for the two processes

+  // To model fairness of scheduling, these "budget" variable give a bound on the number of times the

+  // scheduler will repeatedly schedule on process to execute its "compare a and b" test.  When a

+  // process executes its comparison, its budget is decreased and the budget for the other process

+  // is set to some arbitrary positive amount.

+  var budget0, budget1 :| budget0 > 0 && budget1 > 0;

+  while !(pc0 == 3 && pc1 == 3)

+    invariant 0 < a && 0 < b

+    invariant Gcd(A, B) == Gcd(a, b)

+    invariant 0 <= pc0 < 4 && 0 <= pc1 < 4

+    invariant (pc0 == 0 || a0 == a) && (pc1 == 0 || b1 == b)

+    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

+    // 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),

+              8 - pc0 - pc1

+  {

+    if {

+      case pc0 == 0                            => a0, pc0 := a, 1;

+      case pc0 == 1                            => b0, pc0 := b, 2;

+      case pc0 == 2 && (budget0 > 0 || pc1 == 3) && a0 > b0  =>

+                                                  GcdDecrease(a, b);

+                                                  a, pc0 := a0 - b0, 0;

+                                                  budget0, budget1 := BudgetUpdate(budget0, budget1, pc1);

+      case pc0 == 2 && (budget0 > 0 || pc1 == 3) && a0 < b0  =>

+                                                  pc0 := 0;

+                                                  budget0, budget1 := BudgetUpdate(budget0, budget1, pc1);

+      case pc0 == 2 && (budget0 > 0 || pc1 == 3) && a0 == b0 =>

+                                                  pc0 := 3;

+                                                  budget0, budget1 := BudgetUpdate(budget0, budget1, pc1);

+      case pc1 == 0                            => b1, pc1 := b, 1;

+      case pc1 == 1                            => a1, pc1 := a, 2;

+      case pc1 == 2 && (budget1 > 0 || pc0 == 3) && b1 > a1  =>

+                                                  Symmetry(a, b); GcdDecrease(b, a); Symmetry(b - a, a);

+                                                  b, pc1 := b1 - a1, 0;

+                                                  budget1, budget0 := BudgetUpdate(budget1, budget0, pc0);

+      case pc1 == 2 && (budget1 > 0 || pc0 == 3) && b1 < a1  =>

+                                                  pc1 := 0;

+                                                  budget1, budget0 := BudgetUpdate(budget1, budget0, pc0);

+      case pc1 == 2 && (budget1 > 0 || pc0 == 3) && b1 == a1 =>

+                                                  pc1 := 3;

+                                                  budget1, budget0 := BudgetUpdate(budget1, budget0, pc0);

+    }

+  }

+  GcdEqual(a);

+  gcd := a;

+}

+

+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

+{

+  if pcThat == 3 {

+    outThis, outThat := inThis, inThat;

+  } else {

+    outThis := inThis - 1;

+    outThat :| outThat > 0;

+  }

+}

+

+function Gcd(a: int, b: int): int

+  requires a > 0 && b > 0

+{

+  Exists(a, b);

+  var d :| DividesBoth(d, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= d;

+  d

+}

+

+predicate DividesBoth(d: int, a: int, b: int)

+  requires a > 0 && b > 0

+{

+  d > 0 && Divides(d, a) && Divides(d, b)

+}

+

+predicate {:opaque} Divides(d: int, a: int)

+  requires d > 0 && a > 0

+{

+  exists n :: n > 0 && MulTriple(n, d, a)

+}

+predicate MulTriple(n: int, d: int, a: int)

+  requires n > 0 && d > 0

+{

+  n * d == a

+}

+

+// ----- lemmas and proofs

+

+lemma Exists(a: int, b: int)

+  requires a > 0 && b > 0

+  ensures exists d :: DividesBoth(d, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= d;

+{

+  var d := ShowExists(a, b);

+}

+

+lemma ShowExists(a: int, b: int) returns (d: int)

+  requires a > 0 && b > 0

+  ensures DividesBoth(d, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= d;

+{

+  forall

+    ensures exists d :: DividesBoth(d, a, b)

+  {

+    OneDividesAnything(a);

+    OneDividesAnything(b);

+    assert Divides(1, a);

+    assert Divides(1, b);

+    assert DividesBoth(1, a, b);

+  }

+  d :| DividesBoth(d, a, b);

+  DividesUpperBound(d, a);

+  DividesUpperBound(d, b);

+  while true

+    invariant DividesBoth(d, a, b)

+    invariant d <= a && d <= b

+    decreases a + b - 2*d

+  {

+    if exists k :: DividesBoth(k, a, b) && k > d {

+      var k :| DividesBoth(k, a, b) && k > d;

+      d := k;

+      assert Divides(d, a);

+      DividesUpperBound(d, a);

+      assert d <= a;

+      DividesUpperBound(d, b);

+      assert d <= b;

+    } else {

+      return;

+    }

+  }

+}

+

+lemma OneDividesAnything(a: int)

+  requires a > 0

+  ensures Divides(1, a)

+{

+  reveal_Divides();  // here, we use the definition of Divides

+  assert MulTriple(a, 1, a);

+}

+

+lemma GcdEqual(a: int)

+  requires a > 0

+  ensures Gcd(a, a) == a

+{

+  DividesIdempotent(a);

+  assert Divides(a, a);

+  DividesUpperBound(a, a);

+  assert DividesBoth(a, a, a);

+

+  var k := Gcd(a, a);

+  assert k > 0 && DividesBoth(k, a, a);

+  assert forall m :: m > 0 && DividesBoth(m, a, a) ==> m <= k;

+  assert Divides(k, a);

+  DividesUpperBound(k, a);

+}

+

+lemma DividesIdempotent(a: int)

+  requires a > 0

+  ensures Divides(a, a)

+{

+  reveal_Divides();  // here, we use the body of function Divides

+  assert MulTriple(1, a, a);

+}

+

+lemma DividesUpperBound(d: int, a: int)

+  requires d > 0 && a > 0

+  ensures Divides(d, a) ==> d <= a

+{

+  reveal_Divides();  // here, we use the body of function Divides

+}

+

+lemma Symmetry(a: int, b: int)

+  requires a > 0 && b > 0

+  ensures Gcd(a, b) == Gcd(b, a)

+{

+  var k, l := Gcd(a, b), Gcd(b, a);

+  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 k == l;

+}

+

+lemma GcdDecrease(a: int, b: int)

+  requires a > b > 0

+  ensures Gcd(a, b) == Gcd(a - b, b)

+{

+  var k := Gcd(a - b, b);

+  assert DividesBoth(k, a-b, b) && forall m :: DividesBoth(m, a-b, b) ==> m <= k;

+  var n := DividesProperty(k, a-b);

+  assert n*k == a-b;

+  var p := DividesProperty(k, b);

+  assert p*k == b;

+

+  assert n*k + p*k == a-b + b;

+  assert (n+p)*k == a;

+

+  MultipleDivides(n+p, k, a);

+  assert Divides(k, a);

+  assert DividesBoth(k, a, b);

+

+  var l := Gcd(a, b);

+  assert forall m :: DividesBoth(m, a, b) ==> m <= l;

+  assert k <= l;

+

+  var n' := DividesProperty(l, a);

+  var p' := DividesProperty(l, b);

+  assert n'*l == a;

+  assert p'*l == b;

+  assert n'*l - p'*l == a - b;

+  assert (n' - p')*l == a - b;

+  MultipleDivides(n' - p', l, a - b);

+  assert Divides(l, a - b);

+  assert DividesBoth(l, a - b, b);

+  assert l <= k;

+

+  assert k == l;

+}

+

+lemma MultipleDivides(n: int, d: int, a: int)

+  requires n > 0 && d > 0 && n*d == a

+  ensures Divides(d, a)

+{

+  reveal_Divides();

+  assert MulTriple(n, d, a);

+}

+

+lemma DividesProperty(d: int, a: int) returns (n: int)

+  requires d > 0 && a > 0

+  requires Divides(d, a)

+  ensures n*d == a

+{

+  reveal_Divides();

+  n :| n > 0 && MulTriple(n, d, a);

+}

diff --git a/Test/VerifyThis2015/Problem2.dfy.expect b/Test/VerifyThis2015/Problem2.dfy.expect
new file mode 100644
index 00000000..ad540132
--- /dev/null
+++ b/Test/VerifyThis2015/Problem2.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 35 verified, 0 errors

diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy
new file mode 100644
index 00000000..fb95637d
--- /dev/null
+++ b/Test/VerifyThis2015/Problem3.dfy
@@ -0,0 +1,125 @@
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:5 "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

+// Rustan Leino

+// 12 April 2015

+// VerifyThis 2015

+// Problem 3 -- Dancing Links

+

+// The following method demonstrates that Remove and PutBack (defined below) have the desired properties

+method Test(dd: DoublyLinkedList, x: Node)

+  requires dd != null && dd.Valid()

+  requires x in dd.Nodes && x != dd.Nodes[0] && x != dd.Nodes[|dd.Nodes|-1]

+  modifies dd, dd.Nodes

+  ensures dd.Valid() && dd.Nodes == old(dd.Nodes)

+{

+  ghost var k := dd.Remove(x);

+  dd.PutBack(x, k);

+}

+// It is also possible to remove and put back any number of elements, provided these operations are

+// done in a FOLI order.

+method TestMany(dd: DoublyLinkedList, xs: seq<Node>)

+  requires dd != null && dd.Valid()

+  requires forall x :: x in xs ==> x in dd.Nodes && x != dd.Nodes[0] && x != dd.Nodes[|dd.Nodes|-1]

+  requires forall i,j :: 0 <= i < j < |xs| ==> xs[i] != xs[j]

+  modifies dd, dd.Nodes

+  ensures dd.Valid() && dd.Nodes == old(dd.Nodes)

+{

+  if xs != [] {

+    var x := xs[0];

+    ghost var k := dd.Remove(x);

+    TestMany(dd, xs[1..]);

+    dd.PutBack(x, k);

+  }

+}

+

+// And here's a Main program that shows that doubly linked lists do exist (well, at least there is one :))

+method Main()

+{

+  var a0 := new Node;

+  var a1 := new Node;

+  var a2 := new Node;

+  var a3 := new Node;

+  var a4 := new Node;

+  var a5 := new Node;

+  var dd := new DoublyLinkedList([a0, a1, a2, a3, a4, a5]);

+  Test(dd, a3);

+  TestMany(dd, [a2, a4, a3]);

+}

+

+class Node {

+  var L: Node

+  var R: Node

+}

+

+class DoublyLinkedList {

+  ghost var Nodes: seq<Node>  // sequence of nodes in the linked list

+  // Valid() says that the data structure is a proper doubly linked list

+  predicate Valid()

+    reads this, Nodes

+  {

+    (forall i :: 0 <= i < |Nodes| ==> Nodes[i] != null) &&

+    (|Nodes| > 0 ==>

+      Nodes[0].L == null && (forall i :: 1 <= i < |Nodes| ==> Nodes[i].L == Nodes[i-1]) &&

+      (forall i :: 0 <= i < |Nodes|-1 ==> Nodes[i].R == Nodes[i+1]) && Nodes[|Nodes|-1].R == null

+    ) &&

+    forall i,j :: 0 <= i < j < |Nodes| ==> Nodes[i] != Nodes[j]  // this is actually a consequence of the previous conditions

+  }

+  // This constructor just shows that there is a way to create a doubly linked list.  It accepts

+  // as an argument the sequences of Nodes to construct the doubly linked list from.  The constructor

+  // will change all the .L and .R pointers of the given nodes in order to create a properly

+  // formed list.

+  constructor (nodes: seq<Node>)

+    requires forall i :: 0 <= i < |nodes| ==> nodes[i] != null

+    requires forall i,j :: 0 <= i < j < |nodes| ==> nodes[i] != nodes[j]

+    modifies this, nodes

+    ensures Valid() && Nodes == nodes

+  {

+    if nodes != [] {

+      var prev, n := nodes[0], 1;

+      prev.L, prev.R := null, null;

+      while n < |nodes|

+        invariant 1 <= n <= |nodes|

+        invariant nodes[0].L == null

+        invariant prev == nodes[n-1] && prev.R == null

+        invariant forall i :: 1 <= i < n ==> nodes[i].L == nodes[i-1]

+        invariant forall i :: 0 <= i < n-1 ==> nodes[i].R == nodes[i+1]

+      {

+        nodes[n].L, prev.R, prev := prev, nodes[n], nodes[n];

+        prev.R := null;

+        n := n + 1;

+      }

+    }

+    Nodes := nodes;

+  }

+  method Remove(x: Node) returns (ghost k: int)

+    requires Valid()

+    requires x in Nodes && x != Nodes[0] && x != Nodes[|Nodes|-1]  // not allowed to remove end nodes; you may think of them as a sentinel nodes

+    modifies this, Nodes

+    ensures Valid()

+    ensures 0 <= k < |old(Nodes)| && x == old(Nodes)[k]

+    ensures Nodes == old(Nodes)[..k] + old(Nodes)[k+1..] && x.L == old(x.L) && x.R == old(x.R)

+  {

+    k :| 1 <= k < |Nodes|-1 && Nodes[k] == x;

+    x.R.L := x.L;

+    x.L.R := x.R;

+    Nodes := Nodes[..k] + Nodes[k+1..];

+  }

+  // One might consider have a precondition that says there exists a "k" with the properties given here.

+  // However, we want to be able to refer to "k" in the postcondition as well, so it's convenient to

+  // burden the client with having to pass in "k" as a ghost parameter.  This, however, is really no

+  // extra burden on the client, because if the client would have been able to show the existence of

+  // such a "k", then the client can easily just use an assign-such-that statement to obtain such a

+  // value "k".

+  method PutBack(x: Node, ghost k: int)

+    requires Valid()

+    requires x != null && 1 <= k < |Nodes| && x.L == Nodes[k-1] && x.R == Nodes[k]

+    modifies this, Nodes, x

+    ensures Valid()

+    ensures Nodes == old(Nodes)[..k] + [x] + old(Nodes)[k..]

+  {

+    x.R.L := x;

+    x.L.R := x;

+    Nodes := Nodes[..k] + [x] + Nodes[k..];

+  }

+}

diff --git a/Test/VerifyThis2015/Problem3.dfy.expect b/Test/VerifyThis2015/Problem3.dfy.expect
new file mode 100644
index 00000000..9559b9a6
--- /dev/null
+++ b/Test/VerifyThis2015/Problem3.dfy.expect
@@ -0,0 +1,5 @@
+

+Dafny program verifier finished with 13 verified, 0 errors

+Program compiled successfully

+Running...

+