diff options
| author |  Jason Koenig <unknown> | 2012-06-28 16:38:27 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-06-28 16:38:27 -0700 |
| commit | 94b721bde2ce1f1702c9b9f4fef1554e11f9d313 (patch) | |
| tree | 1cb72f5b91398c1d127734d01cf74114bcd753bd | |
| parent | cd498c42f796d5e1cd7d5afd57da1310232e4c4c (diff) | |
Dafny: fixed some test cases
| -rw-r--r-- | Test/dafny0/Answer | 101 | ||||
| -rw-r--r-- | Test/dafny0/EqualityTypes.dfy | 89 | ||||
| -rw-r--r-- | Test/dafny0/LiberalEquality.dfy | 2 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 74 | ||||
| -rw-r--r-- | Test/dafny0/Modules1.dfy | 25 | ||||
| -rw-r--r-- | Test/dafny0/ModulesCycle.dfy | 35 | ||||
| -rw-r--r-- | Test/dafny0/Predicates.dfy | 10 | ||||
| -rw-r--r-- | Test/dafny0/Refinement.dfy | 5 | ||||
| -rw-r--r-- | Test/dafny1/ListContents.dfy | 13 | ||||
| -rw-r--r-- | Test/dafny1/SchorrWaite-stages.dfy | 267 | ||||
| -rw-r--r-- | Test/dafny1/runtest.bat | 2 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 4 |
12 files changed, 470 insertions, 157 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 7510363a..85958099 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -703,8 +703,8 @@ Execution trace: Dafny program verifier finished with 7 verified, 1 error
-------------------- ModulesCycle.dfy --------------------
-ModulesCycle.dfy(12,7): Error: module T named among imports does not exist
-ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G
+ModulesCycle.dfy(3,9): Error: module T does not exist
+ModulesCycle.dfy(6,7): Error: module definition contains a cycle (note: parent modules implicitly depend on submodules): A -> D -> C -> B
2 resolution/type errors detected in ModulesCycle.dfy
-------------------- Modules0.dfy --------------------
@@ -714,55 +714,47 @@ Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB
Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB
-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(52,19): Error: The name T ambiguously refers to a type in one of the modules N, M (try qualifying the type name with the module name)
-Modules0.dfy(52,12): Error: new can be applied only to reference types (got T)
-Modules0.dfy(57,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)
-Modules0.dfy(73,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
-Modules0.dfy(74,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(84,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
-Modules0.dfy(108,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
-Modules0.dfy(247,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
-Modules0.dfy(256,13): Error: unresolved identifier: X
-Modules0.dfy(257,15): Error: member DoesNotExist does not exist in class X
-Modules0.dfy(299,16): Error: member R does not exist in class B
-Modules0.dfy(299,6): Error: expected method call, found expression
-Modules0.dfy(322,18): Error: second argument to "in" must be a set or sequence with elements of type Q_Imp.Node, or a map with domain Q_Imp.Node (instead got set<Node>)
-Modules0.dfy(326,13): Error: arguments must have the same type (got Q_Imp.Node and Node)
-Modules0.dfy(327,11): Error: Undeclared module name: LongLostModule (did you forget a module import?)
-Modules0.dfy(328,11): Error: Undeclared module name: Wazzup (did you forget a module import?)
-Modules0.dfy(329,17): Error: Undeclared class name Edon in module Q_Imp
-Modules0.dfy(331,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
-Modules0.dfy(332,30): Error: member Create does not exist in class Klassy
-Modules0.dfy(143,11): Error: ghost variables are allowed only in specification contexts
-Modules0.dfy(157,11): Error: old expressions are allowed only in specification and ghost contexts
-Modules0.dfy(158,11): Error: fresh expressions are allowed only in specification and ghost contexts
-Modules0.dfy(159,11): Error: allocated expressions are allowed only in specification and ghost contexts
-Modules0.dfy(175,10): Error: match source expression 'tree' has already been used as a match source expression in this context
-Modules0.dfy(214,12): Error: match source expression 'l' has already been used as a match source expression in this context
-36 resolution/type errors detected in Modules0.dfy
+Modules0.dfy(53,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(54,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(65,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)
+Modules0.dfy(72,20): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)
+Modules0.dfy(72,34): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)
+Modules0.dfy(75,23): Error: Undeclared top-level type or type parameter: MyClass0 (did you forget a module import?)
+Modules0.dfy(80,24): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)
+Modules0.dfy(89,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)
+Modules0.dfy(221,15): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)
+Modules0.dfy(221,8): Error: new can be applied only to reference types (got X)
+Modules0.dfy(230,13): Error: The name does not exist in the given module
+Modules0.dfy(240,13): Error: unresolved identifier: X
+Modules0.dfy(241,15): Error: member DoesNotExist does not exist in class X
+Modules0.dfy(280,19): Error: Undeclared top-level type or type parameter: D (did you forget a module import?)
+Modules0.dfy(280,12): Error: new can be applied only to reference types (got D)
+Modules0.dfy(283,25): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(284,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(284,6): Error: expected method call, found expression
+Modules0.dfy(285,16): Error: type of the receiver is not fully determined at this program point
+Modules0.dfy(285,6): Error: expected method call, found expression
+Modules0.dfy(307,24): Error: Undeclared module name: Q_Imp (did you forget a module import?)
+Modules0.dfy(97,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget a module import?)
+28 resolution/type errors detected in Modules0.dfy
-------------------- Modules1.dfy --------------------
-Modules1.dfy(74,16): Error: assertion violation
+Modules1.dfy(75,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(86,16): Error: assertion violation
+Modules1.dfy(88,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Modules1.dfy(88,14): Error: assertion violation
+Modules1.dfy(90,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-Modules1.dfy(52,3): Error: decreases expression must be bounded below by 0
+Modules1.dfy(53,3): Error: decreases expression must be bounded below by 0
Execution trace:
(0,0): anon0
-Modules1.dfy(58,3): Error: failure to decrease termination measure
+Modules1.dfy(59,3): Error: failure to decrease termination measure
Execution trace:
(0,0): anon0
@@ -1441,19 +1433,19 @@ Refinement.dfy(93,3): Error BP5003: A postcondition might not hold on this retur Refinement.dfy(74,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Refinement.dfy(179,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(180,5): Error BP5003: A postcondition might not hold on this return path.
Refinement.dfy(112,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(176,9): Related location: Related location
+Refinement.dfy(177,9): Related location: Related location
Execution trace:
(0,0): anon0
-Refinement.dfy(183,5): Error BP5003: A postcondition might not hold on this return path.
+Refinement.dfy(184,5): Error BP5003: A postcondition might not hold on this return path.
Refinement.dfy(120,15): Related location: This is the postcondition that might not hold.
-Refinement.dfy(176,9): Related location: Related location
+Refinement.dfy(177,9): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Refinement.dfy(189,7): Error: assertion violation
+Refinement.dfy(190,7): Error: assertion violation
Refinement.dfy[IncorrectConcrete](128,24): Related location: Related location
Execution trace:
(0,0): anon0
@@ -1535,24 +1527,24 @@ Predicates.dfy[B](17,15): Related location: This is the postcondition that might Predicates.dfy(28,9): Related location: Related location
Execution trace:
(0,0): anon0
-Predicates.dfy(84,16): Error: assertion violation
+Predicates.dfy(85,16): Error: assertion violation
Execution trace:
(0,0): anon0
-Predicates.dfy(88,14): Error: assertion violation
+Predicates.dfy(89,14): Error: assertion violation
Execution trace:
(0,0): anon0
-Predicates.dfy[Tricky_Full](121,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Tricky_Full](120,15): Related location: This is the postcondition that might not hold.
-Predicates.dfy(131,7): Related location: Related location
-Predicates.dfy[Tricky_Full](111,9): Related location: Related location
+Predicates.dfy[Tricky_Full](123,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Tricky_Full](122,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(133,7): Related location: Related location
+Predicates.dfy[Tricky_Full](113,9): Related location: Related location
Execution trace:
(0,0): anon0
-Predicates.dfy(159,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy(158,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy(161,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy(160,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
-Predicates.dfy[Q1](149,5): Error BP5003: A postcondition might not hold on this return path.
-Predicates.dfy[Q1](148,15): Related location: This is the postcondition that might not hold.
+Predicates.dfy[Q1](151,5): Error BP5003: A postcondition might not hold on this return path.
+Predicates.dfy[Q1](150,15): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
@@ -1583,9 +1575,10 @@ Execution trace: Dafny program verifier finished with 30 verified, 2 errors
-------------------- LiberalEquality.dfy --------------------
+LiberalEquality.dfy(18,14): Error: arguments must have the same type (got T and U)
LiberalEquality.dfy(37,14): Error: arguments must have the same type (got Weird<T,int,V> and Weird<T,bool,V>)
LiberalEquality.dfy(52,14): Error: arguments must have the same type (got array<int> and array<bool>)
-2 resolution/type errors detected in LiberalEquality.dfy
+3 resolution/type errors detected in LiberalEquality.dfy
-------------------- SmallTests.dfy --------------------
SmallTests.dfy(30,11): Error: index out of range
diff --git a/Test/dafny0/EqualityTypes.dfy b/Test/dafny0/EqualityTypes.dfy new file mode 100644 index 00000000..251b2e2f --- /dev/null +++ b/Test/dafny0/EqualityTypes.dfy @@ -0,0 +1,89 @@ +module A {
+ datatype Explicit<T(==)> = Nil | Cons(set<T>, Explicit<T>);
+ datatype Inferred<T> = Nil | Cons(set<T>, Inferred<T>);
+
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T>(x: Inferred<T>)
+ }
+}
+
+module B refines A {
+ class C {
+ method M<T>(x: Explicit<T>)
+ method N<T(==)>(x: Inferred<T>)
+ }
+}
+
+// ----------------------------
+
+module C {
+ type X(==);
+ type Y(==);
+}
+
+module D refines C {
+ class X { }
+ datatype Y = Red | Green | Blue;
+}
+
+module E refines C {
+ codatatype X = Next(int, X); // error: X requires equality and codatatypes don't got it
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green(X) | Blue;
+}
+
+module F refines C {
+ datatype X<T> = Nil | Cons(T, X<T>); // error: not allowed to add a type parameter to type X
+ class Y<T> { } // error: not allowed to add a type parameter to type Y
+}
+
+module G refines C {
+ datatype X = Nil | Next(Z, X); // error: X does not support equality
+ datatype Y = Nil | Something(Z) | More(Y, Y); // error: Y does not support equality
+ codatatype Z = Red | Green | Blue;
+}
+
+// ----------------------------
+
+module H {
+ datatype Dt<T> = Nil | Cons(T, Dt);
+
+ datatype BulkyList<T> = Nothing | Wrapper(T, BulkyListAux);
+ datatype BulkyListAux<T> = Kons(set<T>, BulkyListAuxAux);
+ datatype BulkyListAuxAux<T> = GoBack(BulkyList);
+
+ codatatype Stream<T> = Next(head: T, tail: Stream<T>);
+
+ method M<T(==)>(x: T)
+ { }
+ function method F<T>(x: BulkyList<T>, y: BulkyList<T>): int
+ { if x == y then 5 else 7 } // this equality is allowed
+ function method G<T>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // error: the equality is not allowed, because Dt<T> may not support equality
+ function method G'<T(==)>(x: Dt<T>, y: Dt<T>): int
+ { if x == y then 5 else 7 } // fine
+
+ method Caller0(b: BulkyList, y: int) {
+ match (b) {
+ case Nothing =>
+ case Wrapper(t, bla) =>
+ var u;
+ if (y < 100) { u := t; }
+ // The following call is allowed, because it will be inferred that
+ // 'u' is of a type that supports equality
+ M(u);
+ }
+ }
+ method Caller1(d: Dt) {
+ match (d) {
+ case Nil =>
+ case Cons(t, rest) =>
+ M(t); // error: t may be of a type that does not support equality
+ }
+ }
+ method Caller2(co: Stream) {
+ var d := Cons(co, Nil);
+ Caller1(d); // case in point for the error in Caller1
+ }
+}
diff --git a/Test/dafny0/LiberalEquality.dfy b/Test/dafny0/LiberalEquality.dfy index 3dc52c80..b9b4629b 100644 --- a/Test/dafny0/LiberalEquality.dfy +++ b/Test/dafny0/LiberalEquality.dfy @@ -15,7 +15,7 @@ class Test<T> { }
method m1<T, U>(t: T, u: U)
- requires t != u;
+ requires t != u; // Cannot compare type parameters (can only compare reference types that could be the same)
{
}
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index 80ac7eef..273c88de 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -23,46 +23,26 @@ module N { class T { }
}
-module U imports N { // fine, despite the fact that a class is called U,
- // since module names are in their own name space
+module U {
+ module NN = N;
}
-module UU imports N, U, N, N { // duplicates are allowed
-}
-
-module N_left imports N { }
-module N_right imports N { }
-module Diamond imports N_left, N_right { // this imports N.T twice, but that's okay
-}
-module A imports N, M { // Note, this has the effect of importing two different T's,
- // but that's okay as long as the module doesn't try to access
- // one of them
+module A { // Note, this has the effect of importing two different T's,
+ // but that's okay as long as the module doesn't try to access
+ // one of them
+ module MM = M;
+ module NN = N;
class X {
- var t: T; // error: use of the ambiguous name T
- function F(x: T): // error: use of the ambiguous name T
- T // error: use of the ambiguous name T
+ var t: MM.T; // error: use of the ambiguous name T
+ function F(x: MM.T): // error: use of the ambiguous name T
+ MM.T // error: use of the ambiguous name T
{ x }
- method M(x: T) // error: use of the ambiguous name T
- returns (y: T) // error: use of the ambiguous name T
+ method M(x: NN.T) // error: use of the ambiguous name T
+ returns (y: NN.T) // error: use of the ambiguous name T
}
}
-module A' imports N, M {
- method M()
- { var g := new T; } // error: use of the ambiguous name T
-}
-module B0 imports A {
- class BadUse {
- var b0: T; // error: T is not directly accessible
- }
-}
-
-module B1 imports A, N {
- class GoodUse {
- var b1: T; // fine
- }
-}
// --------------- calls
@@ -76,9 +56,10 @@ module X0 { }
}
-module X1 imports X0 {
+module X1 {
+ module X0' = X0;
class MyClass1 {
- method Down(x0: MyClass0) {
+ method Down(x0: X0'.MyClass0) {
x0.Down();
}
method Up(x2: MyClass2) { // error: class MyClass2 is not in scope
@@ -86,7 +67,7 @@ module X1 imports X0 { }
}
-module X2 imports X0, X1, YY {
+module X2 {
class MyClass2 {
method Down(x1: MyClass1, x0: MyClass0) {
x1.Down(x0);
@@ -231,9 +212,10 @@ module ATr { }
}
-module BTr imports ATr {
+module BTr {
+ module A = ATr;
class Y {
- method N() returns (x: X)
+ method N() returns (x: A.X)
ensures x != null;
{
x := new X;
@@ -241,15 +223,17 @@ module BTr imports ATr { }
}
-module CTr imports BTr {
+module CTr {
+ module B = BTr;
class Z {
- var b: Y; // fine
- var a: X; // error: imports don't reach name X explicitly
+ var b: B.Y; // fine
+ var a: B.X; // error: imports don't reach name X explicitly
}
}
-module CTs imports BTr {
+module CTs {
+ module B = BTr;
method P() {
- var y := new Y;
+ var y := new B.Y;
var x := y.N(); // this is allowed and will correctly infer the type of x to
// be X, but X could not have been mentioned explicitly
var q := x.M();
@@ -285,7 +269,9 @@ module NonLocalB { }
}
-module Local imports NonLocalA, NonLocalB {
+module Local {
+ module AA = NonLocalA;
+ module BB = NonLocalB;
class MyClass {
method MyMethod()
{
@@ -317,7 +303,7 @@ module Q_Imp { }
}
-module Q_M imports Q_Imp {
+module Q_M {
method MyMethod(root: Q_Imp.Node, S: set<Node>)
requires root in S; // error: the element type of S does not agree with the type of root
{
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index e8a88749..6fd8560e 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -1,6 +1,7 @@ -module A imports B {
+module A {
+ module B = Babble;
class X {
- function Fx(z: Z): int
+ function Fx(z: B.Z): int
requires z != null;
decreases 5, 4, 3;
{ z.G() } // fine; this goes to a different module
@@ -17,7 +18,7 @@ method MyMethod() { } var MyField: int;
-module B {
+module Babble {
class Z {
method K() { }
function G(): int
@@ -78,14 +79,15 @@ module A_Visibility { }
}
-module B_Visibility imports A_Visibility {
+module B_Visibility {
+ module A = A_Visibility;
method Main() {
var y;
- if (C.P(y)) {
+ if (A.C.P(y)) {
assert 0 <= y; // this much is known of C.P
assert 2 <= y; // error
} else {
- assert C.P(8); // error: C.P cannot be established outside the declaring module
+ assert A.C.P(8); // error: C.P cannot be established outside the declaring module
}
}
}
@@ -99,13 +101,14 @@ module Q_Imp { }
}
-module Q_M imports Q_Imp {
- method MyMethod(root: Q_Imp.Node, S: set<Q_Imp.Node>)
+module Q_M {
+ module Q = Q_Imp;
+ method MyMethod(root: Q.Node, S: set<Q.Node>)
requires root in S;
{
- var i := new Q_Imp.Node;
- var j := new Node;
+ var i := new Q.Node;
+ var j := new Q.Node;
assert i != j; // fine
- var q := new Q_Imp.Klassy.Init();
+ var q := new Q.Klassy.Init();
}
}
diff --git a/Test/dafny0/ModulesCycle.dfy b/Test/dafny0/ModulesCycle.dfy index a7f1caa2..15cad8e8 100644 --- a/Test/dafny0/ModulesCycle.dfy +++ b/Test/dafny0/ModulesCycle.dfy @@ -1,33 +1,12 @@ -module M {
- class T { }
- class U { }
-}
-
-module N {
-}
-
-module U imports N {
-}
-
-module V imports T { // error: T is not a module
-}
-module A imports B, M {
- class Y { }
+module V {
+ module t = T; // error: T is not visible (and isn't even a module)
}
-module B imports N, M {
- class X { }
+module A {
+ module B = C;
}
-module G imports A, M, A, H, B { // error: cycle in import graph
-}
-
-module H imports A, N, I {
-}
-
-module I imports J {
-}
-
-module J imports G, M {
-}
+module C {
+ module D = A;
+}
\ No newline at end of file diff --git a/Test/dafny0/Predicates.dfy b/Test/dafny0/Predicates.dfy index 146129b5..8857482f 100644 --- a/Test/dafny0/Predicates.dfy +++ b/Test/dafny0/Predicates.dfy @@ -78,9 +78,10 @@ module Tight refines Loose { }
}
-module UnawareClient imports Loose {
+module UnawareClient {
+ module L = Loose;
method Main0() {
- var n := new MyNumber.Init();
+ var n := new L.MyNumber.Init();
assert n.N == 0; // error: this is not known
n.Inc();
n.Inc();
@@ -89,9 +90,10 @@ module UnawareClient imports Loose { }
}
-module AwareClient imports Tight {
+module AwareClient {
+ module T = Tight;
method Main1() {
- var n := new MyNumber.Init();
+ var n := new T.MyNumber.Init();
assert n.N == 0;
n.Inc();
n.Inc();
diff --git a/Test/dafny0/Refinement.dfy b/Test/dafny0/Refinement.dfy index da7f0ac2..2c2fc52b 100644 --- a/Test/dafny0/Refinement.dfy +++ b/Test/dafny0/Refinement.dfy @@ -155,10 +155,11 @@ module Concrete refines Abstract { } } -module Client imports Concrete { +module Client { + module C = Concrete; class TheClient { method Main() { - var n := new MyNumber.Init(); + var n := new C.MyNumber.Init(); n.Inc(); n.Inc(); var k := n.Get(); diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy index 594be748..a8b4861d 100644 --- a/Test/dafny1/ListContents.dfy +++ b/Test/dafny1/ListContents.dfy @@ -62,7 +62,7 @@ class Node<T> { reverse.next := null;
reverse.footprint := {reverse};
reverse.list := [data];
-
+
while (current != null)
invariant reverse != null && reverse.Valid();
invariant reverse.footprint <= old(footprint);
@@ -71,8 +71,8 @@ class Node<T> { current.Valid() &&
current in old(footprint) && current.footprint <= old(footprint) &&
current.footprint !! reverse.footprint &&
- |old(list)| == |reverse.list| + |current.list| &&
- (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
+ |old(list)| == |reverse.list| + |current.list|;
+ invariant current != null ==> current.list == old(list)[|reverse.list|..];
invariant
(forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
decreases if current != null then |current.list| else -1;
@@ -86,13 +86,6 @@ class Node<T> { reverse := current;
current := nx;
- // This makes the verification go faster.
- assert current != null ==>
- current.Valid() &&
- current in old(footprint) && current.footprint <= old(footprint) &&
- current.footprint !! reverse.footprint &&
- |old(list)| == |reverse.list| + |current.list| &&
- (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
}
}
}
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy new file mode 100644 index 00000000..5a4da8ce --- /dev/null +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -0,0 +1,267 @@ +// Schorr-Waite algorithms, written and verified in Dafny.
+// Rustan Leino
+// Original version: 7 November 2008
+// Version with proof divided into stages: June 2012.
+// Copyright (c) 2008-2012 Microsoft.
+
+ghost module M0 {
+ // In this module, we declare the Node class, the definition of Reachability, and the specification
+ // and implementation of the Schorr-Waite algorithm.
+
+ class Node {
+ var children: seq<Node>;
+ var marked: bool;
+ var childrenVisited: nat;
+ }
+
+ datatype Path = Empty | Extend(Path, Node);
+
+ function Reachable(source: Node, sink: Node, S: set<Node>): bool
+ requires null !in S;
+ reads S;
+ {
+ exists via: Path :: ReachableVia(source, via, sink, S)
+ }
+
+ function ReachableVia(source: Node, p: Path, sink: Node, S: set<Node>): bool
+ requires null !in S;
+ reads S;
+ decreases p;
+ {
+ match p
+ case Empty => source == sink
+ case Extend(prefix, n) => n in S && sink in n.children && ReachableVia(source, prefix, n, S)
+ }
+
+ method SchorrWaite(root: Node, ghost S: set<Node>)
+ requires root in S;
+ // S is closed under 'children':
+ requires forall n :: n in S ==> n != null &&
+ forall ch :: ch in n.children ==> ch == null || ch in S;
+ // the graph starts off with nothing marked and nothing being indicated as currently being visited:
+ requires forall n :: n in S ==> !n.marked && n.childrenVisited == 0;
+ modifies S;
+ // nodes reachable from 'root' are marked:
+ ensures root.marked;
+ ensures forall n :: n in S && n.marked ==>
+ forall ch :: ch in n.children && ch != null ==> ch.marked;
+ // every marked node was reachable from 'root' in the pre-state:
+ ensures forall n :: n in S && n.marked ==> old(Reachable(root, n, S));
+ // the structure of the graph has not changed:
+ ensures forall n :: n in S ==>
+ n.childrenVisited == old(n.childrenVisited) &&
+ n.children == old(n.children);
+ {
+ root.marked := true;
+ var t, p := root, null;
+ ghost var stackNodes := [];
+ while (true)
+ // stackNodes is a sequence of nodes from S:
+ invariant forall n :: n in stackNodes ==> n in S;
+
+ // The current node, t, is not included in stackNodes. Rather, t is just above the top of stackNodes.
+ // We say that the stack stackNodes+[t] are the "active" nodes.
+ invariant t in S && t !in stackNodes;
+
+ // p points to the parent of the current node, that is, the node through which t was encountered in the
+ // depth-first traversal. This amounts to being the top of stackNodes, or null if stackNodes is empty.
+ // Note, it may seem like the variable p is redundant, since it holds a value that can be computed
+ // from stackNodes. But note that stackNodes is a ghost variable and won't be present at run
+ // time, where p is a physical variable that will be present at run time.
+ invariant p == if |stackNodes| == 0 then null else stackNodes[|stackNodes|-1];
+
+ // The .childrenVisited field is the extra information that the Schorr-Waite algorithm needs. It
+ // is used only for the active nodes, where it keeps track of how many of a node's children have been
+ // processed. For the nodes on stackNodes, .childrenVisited is less than the number of children, so
+ // it is an index of a child. For t, .childrenVisited may be as large as all of the children, which
+ // indicates that the node is ready to be popped off the stack of active nodes. For all other nodes,
+ // .childrenVisited is the original value, which is 0.
+ invariant forall n :: n in stackNodes ==> n.childrenVisited < |n.children|;
+ invariant t.childrenVisited <= |t.children|;
+ invariant forall n :: n in S && n !in stackNodes && n != t ==> n.childrenVisited == 0;
+
+ // To represent the stackNodes, the algorithm reverses children pointers. It never changes the number
+ // of children a node has. The only nodes with children pointers different than the original values are
+ // the nodes on stackNodes; moreover, only the index of the currently active child of a node is different.
+ invariant forall n :: n in stackNodes ==>
+ |n.children| == old(|n.children|) &&
+ forall j :: 0 <= j < |n.children| ==> j == n.childrenVisited || n.children[j] == old(n.children[j]);
+ invariant forall n :: n in S && n !in stackNodes ==> n.children == old(n.children);
+
+ // The children pointers that have been changed form a stack. That is, the active child of stackNodes[k]
+ // points to stackNodes[k-1], with the end case pointing to null.
+ invariant 0 < |stackNodes| ==>
+ stackNodes[0].children[stackNodes[0].childrenVisited] == null;
+ invariant forall k :: 0 < k < |stackNodes| ==>
+ stackNodes[k].children[stackNodes[k].childrenVisited] == stackNodes[k-1];
+ // We also need to keep track of what the original values of the children pointers had been. Here, we
+ // have that the active child of stackNodes[k] used to be stackNodes[k+1], with the end case pointing
+ // to t.
+ invariant forall k :: 0 <= k < |stackNodes|-1 ==>
+ old(stackNodes[k].children)[stackNodes[k].childrenVisited] == stackNodes[k+1];
+ invariant 0 < |stackNodes| ==>
+ old(stackNodes[|stackNodes|-1].children)[stackNodes[|stackNodes|-1].childrenVisited] == t;
+
+ decreases *; // leave termination checking for a later refinement
+ {
+ if (t.childrenVisited == |t.children|) {
+ // pop
+ t.childrenVisited := 0;
+ if (p == null) { break; }
+
+ t, p, p.children := p, p.children[p.childrenVisited], p.children[p.childrenVisited := t];
+ stackNodes := stackNodes[..|stackNodes| - 1];
+ t.childrenVisited := t.childrenVisited + 1;
+
+ } else if (t.children[t.childrenVisited] == null || t.children[t.childrenVisited].marked) {
+ // just advance to next child
+ t.childrenVisited := t.childrenVisited + 1;
+
+ } else {
+ // push
+ stackNodes := stackNodes + [t];
+ t, p, t.children := t.children[t.childrenVisited], t, t.children[t.childrenVisited := p];
+ t.marked := true;
+
+ // To prove that this "if" branch maintains the invariant "t !in stackNodes" will require
+ // some more properties about the loop. Therefore, we just assume the property here and
+ // prove it in a separate refinement.
+ assume t !in stackNodes;
+ }
+ }
+ // From the loop invariant, it now follows that all children pointers have been restored,
+ // and so have all .childrenVisited fields. Thus, the last postcondition (the one that says
+ // the structure of the graph has not been changed) has been established.
+ // Eventually, we also need to prove that exactly the right nodes have been marked,
+ // but let's just assume those properties for now and prove them in later refinements:
+ assume root.marked && forall n :: n in S && n.marked ==>
+ forall ch :: ch in n.children && ch != null ==> ch.marked;
+ assume forall n :: n in S && n.marked ==> old(Reachable(root, n, S));
+ }
+}
+
+ghost module M1 refines M0 {
+ // In this superposition, we start reasoning about the marks. In particular, we prove that the method
+ // marks all reachable nodes.
+ method SchorrWaite...
+ {
+ ...;
+ while ...
+ // The loop keeps marking nodes: The root is always marked. All children of any marked non-active
+ // node are marked. Active nodes are marked, and the first .childrenVisited of every active node
+ // are marked.
+ invariant root.marked;
+ invariant forall n :: n in S && n.marked && n !in stackNodes && n != t ==>
+ forall ch :: ch in n.children && ch != null ==> ch.marked;
+ invariant forall n :: n in stackNodes || n == t ==>
+ n.marked &&
+ forall j :: 0 <= j < n.childrenVisited ==> n.children[j] == null || n.children[j].marked;
+
+ decreases *; // keep postponing termination checking
+ {
+ if ... { // pop
+ } else if ... { // next child
+ } else { // push
+ ...;
+ // With the new loop invariants, we know that all active nodes are marked. Since the new value
+ // of "t" was not marked at the beginning of this iteration, we can now prove that the invariant
+ // "t !in stackNodes" is maintained, so we'll refine the assume from above with an assert.
+ assert ...;
+ }
+ }
+ // The new loop invariants give us a lower bound on which nodes are marked. Hence, we can now
+ // discharge the "everything reachable is marked" postcondition, whose proof we postponed above
+ // by supplying an assume statement. Here, we refine that assume statement into an assert.
+ assert ...;
+ }
+}
+
+ghost module M2 refines M1 {
+ // In this superposition, we prove that only reachable nodes are marked. Essentially, we want
+ // to add a loop invariant that says t is reachable from root, because then the loop invariant
+ // that marked nodes are reachable follows. More precisely, we need to say that the node
+ // referenced by t is *in the initial state* reachable from root--because as we change
+ // children pointers during the course of the algorithm, what is reachable at some point in
+ // time may be different from what was reachable initially.
+
+ // To do our proof, which involves establishing reachability between various nodes, we need
+ // some additional bookkeeping. In particular, we keep track of the path from root to t,
+ // and we associate with every marked node the path to it from root. The former is easily
+ // maintained in a local ghost variable; the latter is most easily represented as a ghost
+ // field in each node (an alternative would be to have a local variable that is a map from
+ // nodes to paths). So, we add a field declaration to the Node class:
+ class Node {
+ ghost var pathFromRoot: Path;
+ }
+
+ method SchorrWaite...
+ {
+ ghost var path := Path.Empty;
+ root.pathFromRoot := path;
+ ...;
+ while ...
+ // There's a subtle complication when we speak of old(ReachableVia(... P ...)) for a path
+ // P. The expression old(...) says to evaluate the expression "..." in the pre-state of
+ // the method. So, old(ReachableVia(...)) says to evaluate ReachableVia(...) in the pre-
+ // state of the method. But in order for the "old(...)" expression to be well-formed,
+ // the subexpressions of the "..." must only refer to values that existed in the pre-state
+ // of the method. This incurs the proof obligation that any objects referenced by the
+ // parameters of ReachableVia(...) must have been allocated in the pre-state of the
+ // method. The proof obligation is easy to establish for root, t, and S (since root and
+ // S were given as in-parameters to the method, and we have "t in S"). But what about
+ // the path argument to ReachableVia? Since datatype values of type Path contain object
+ // references, we need to make sure we can deal with the proof obligation for the path
+ // argument. For this reason, we add invariants that say that "path" and the .pathFromRoot
+ // field of all marked nodes contain values that make sense in the pre-state.
+ invariant old(allocated(path)) && old(ReachableVia(root, path, t, S));
+ invariant forall n :: n in S && n.marked ==> var pth := n.pathFromRoot;
+ old(allocated(pth)) && old(ReachableVia(root, pth, n, S));
+ invariant forall n :: n in S && n.marked ==> old(Reachable(root, n, S));
+
+ decreases *; // keep postponing termination checking
+ {
+ if ... {
+ // pop
+ ...;
+ path := t.pathFromRoot;
+ } else if ... {
+ // advance to next child
+ } else {
+ // push
+ path := Path.Extend(path, t);
+ ...;
+ t.pathFromRoot := path;
+ }
+ }
+ // In M0 above, we placed two assume statements here. In M1, we refined the first of these
+ // into an assert. We repeat that assert here:
+ assert ...;
+ // And now we we refine the second assume into an assert, proving that only reachable nodes
+ // have been marked.
+ assert ...;
+ }
+}
+
+module M3 refines M2 {
+ // In this final superposition, we prove termination of the loop.
+ method SchorrWaite...
+ {
+ // The loop variant is a lexicographic triple, consisting of (0) the set of unmarked
+ // nodes, (1) the (length of the) stackNodes sequence, and (2) the number children of
+ // the current node that are still to be investigated. We introduce a ghost variable
+ // to keep track of the set of unmarked nodes.
+ ghost var unmarkedNodes := S - {root};
+ ...;
+ while ...
+ invariant forall n :: n in S && !n.marked ==> n in unmarkedNodes;
+ decreases unmarkedNodes, stackNodes, |t.children| - t.childrenVisited;
+ {
+ if ... { // pop
+ } else if ... { // next child
+ } else { // push
+ ...;
+ unmarkedNodes := unmarkedNodes - {t};
+ }
+ }
+ }
+}
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index fa7f7c70..22bef761 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -5,7 +5,7 @@ set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
for %%f in (Queue.dfy PriorityQueue.dfy
- ExtensibleArray.dfy ExtensibleArrayAuto.dfy
+ ExtensibleArray.dfy
BinaryTree.dfy
UnboundedStack.dfy
SeparationLogicList.dfy
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index b68ba251..19b116d2 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -4,7 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
-REM soon again: SnapshotableTrees.dfy
+REM soon again: SnapshotableTrees.dfy StoreAndRetrieve.dfy
for %%f in (
Classics.dfy
TreeBarrier.dfy
@@ -14,7 +14,7 @@ for %%f in ( COST-verif-comp-2011-3-TwoDuplicates.dfy
COST-verif-comp-2011-4-FloydCycleDetect.dfy
Intervals.dfy TreeFill.dfy TuringFactorial.dfy
- StoreAndRetrieve.dfy MajorityVote.dfy SegmentSum.dfy
+ MajorityVote.dfy SegmentSum.dfy
) do (
echo.
echo -------------------- %%f --------------------
|