summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-04-28 19:48:33 -0700
committerGravatar leino <unknown>2015-04-28 19:48:33 -0700
commit8af694583e86b36d8fcc81485ea2f02c9961d96c (patch)
tree81c8c439236c5cf744fc5d5327586e328a64335d
parent84b3df3615af4f83df753b042b276b994a97b18b (diff)
Changes to the VerifyThis2015 test programs
-rw-r--r--Test/VerifyThis2015/Problem2.dfy39
-rw-r--r--Test/VerifyThis2015/Problem2.dfy.expect2
-rw-r--r--Test/VerifyThis2015/Problem3.dfy20
-rw-r--r--Test/VerifyThis2015/Problem3.dfy.expect2
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...