summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-04-14 04:34:34 -0700
committerGravatar leino <unknown>2015-04-14 04:34:34 -0700
commit90c68ad369e3f9318d4f31ed4f9e628cb7f2738d (patch)
treeedaa342fbe38f798050ca92568c31f7d62ea49c7
parent4c70e323d1af8be2e7386ea25ecb7fe77ec09a49 (diff)
Completed problems from the VerifyThis 2015 program verification competition
-rw-r--r--Test/VerifyThis2015/Problem1.dfy188
-rw-r--r--Test/VerifyThis2015/Problem1.dfy.expect8
-rw-r--r--Test/VerifyThis2015/Problem2.dfy357
-rw-r--r--Test/VerifyThis2015/Problem2.dfy.expect2
-rw-r--r--Test/VerifyThis2015/Problem3.dfy125
-rw-r--r--Test/VerifyThis2015/Problem3.dfy.expect5
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...
+