From 90c68ad369e3f9318d4f31ed4f9e628cb7f2738d Mon Sep 17 00:00:00 2001 From: leino Date: Tue, 14 Apr 2015 04:34:34 -0700 Subject: Completed problems from the VerifyThis 2015 program verification competition --- Test/VerifyThis2015/Problem1.dfy | 188 +++++++++++++++++ Test/VerifyThis2015/Problem1.dfy.expect | 8 + Test/VerifyThis2015/Problem2.dfy | 357 ++++++++++++++++++++++++++++++++ Test/VerifyThis2015/Problem2.dfy.expect | 2 + Test/VerifyThis2015/Problem3.dfy | 125 +++++++++++ Test/VerifyThis2015/Problem3.dfy.expect | 5 + 6 files changed, 685 insertions(+) create mode 100644 Test/VerifyThis2015/Problem1.dfy create mode 100644 Test/VerifyThis2015/Problem1.dfy.expect create mode 100644 Test/VerifyThis2015/Problem2.dfy create mode 100644 Test/VerifyThis2015/Problem2.dfy.expect create mode 100644 Test/VerifyThis2015/Problem3.dfy create mode 100644 Test/VerifyThis2015/Problem3.dfy.expect (limited to 'Test/VerifyThis2015') 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(pat: seq, a: seq) +{ + IsRelaxedPrefixAux(pat, a, 1) +} + +// This predicate returns whether or not "pat", dropping up to "slack" elements, is +// a prefix of "a". +predicate IsRelaxedPrefixAux(pat: seq, a: seq, 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(pat: seq, a: seq) 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(pat: seq, a: seq) +{ + // "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(pat: seq, a: seq) + 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(pat: seq, a: seq) + requires pat <= a + ensures IsRelaxedPrefixAux(pat, a, 1) +{ +} +lemma Same1(pat: seq, a: seq, 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(pat: seq, a: seq, 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(pat: seq, a: seq) + requires pat <= a + ensures IsRelaxedPrefixAux(pat, a, 0) +{ +} +lemma Same2(pat: seq, a: seq) + 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(pat: seq, a: seq) + 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) + 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 // 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) + 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... + -- cgit v1.2.3