diff options
Diffstat (limited to 'Test')
40 files changed, 319 insertions, 108 deletions
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy index 396d0a6e..57a593fe 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -174,7 +174,7 @@ module CallGraph { }
module CrashRegression {
- codatatype Stream<T> = Cons(T, Stream)
+ codatatype Stream = Cons(int, Stream)
// The following functions (where A ends up being the representative in the
// SCC and B, which is also in the same SCC, has no body) once crashed the
@@ -188,3 +188,19 @@ module CrashRegression { function S(): Stream
}
+
+module AmbiguousTypeParameters {
+ codatatype Stream<T> = Cons(T, Stream)
+
+ function A(): Stream
+ {
+ B()
+ }
+
+ // Here, the type arguments to A and S cannot be resolved
+ function B(): Stream
+ ensures A() == S();
+
+ function S(): Stream
+}
+
diff --git a/Test/dafny0/CoResolution.dfy.expect b/Test/dafny0/CoResolution.dfy.expect index e9022f41..140aa890 100644 --- a/Test/dafny0/CoResolution.dfy.expect +++ b/Test/dafny0/CoResolution.dfy.expect @@ -19,4 +19,6 @@ CoResolution.dfy(141,17): Error: a recursive call from a copredicate can go only CoResolution.dfy(149,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(151,4): Error: a recursive call from a copredicate can go only to other copredicates
CoResolution.dfy(167,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
-21 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(202,12): Error: type variable '_T0' in the function call to 'A' could not determined
+CoResolution.dfy(202,19): Error: type variable '_T0' in the function call to 'S' could not determined
+23 resolution/type errors detected in CoResolution.dfy
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy index 8050aded..83b2a571 100644 --- a/Test/dafny0/Computations.dfy +++ b/Test/dafny0/Computations.dfy @@ -184,3 +184,26 @@ ghost method test_fib3(k: nat, m: nat) var y := 12;
assert y <= k && k < y + m && m == 1 ==> fib(k)==144;
}
+
+module NeedsAllLiteralsAxiom {
+ // The following test shows that there exist an example that
+ // benefits from the all-literals axiom. (It's not clear how
+ // important such an example is, nor is it clear what the cost
+ // of including the all-literals axiom is.)
+
+ function trick(n: nat, m: nat): nat
+ decreases n; // note that m is not included
+ {
+ if n < m || m==0 then n else trick(n-m, m) + m
+ }
+
+ lemma lemma_trick(n: nat, m: nat)
+ ensures trick(n, m) == n;
+ {
+ }
+
+ lemma calc_trick(n: nat, m: nat)
+ ensures trick(100, 10) == 100;
+ {
+ }
+}
diff --git a/Test/dafny0/Computations.dfy.expect b/Test/dafny0/Computations.dfy.expect index 85c793d4..71fc8a81 100644 --- a/Test/dafny0/Computations.dfy.expect +++ b/Test/dafny0/Computations.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 58 verified, 0 errors
+Dafny program verifier finished with 63 verified, 0 errors
diff --git a/Test/dafny0/FunctionSpecifications.dfy b/Test/dafny0/FunctionSpecifications.dfy index f78f1cc1..caf8a681 100644 --- a/Test/dafny0/FunctionSpecifications.dfy +++ b/Test/dafny0/FunctionSpecifications.dfy @@ -97,7 +97,7 @@ function IncC(i: nat): int /////////////////////////////////////////////////////////////
// Test basic function hiding
-function {:opaque} secret(x:int, y:int) : int
+function {:opaque} secret(x:int, y:int) : int
requires 0 <= x < 5;
requires 0 <= y < 5;
ensures secret(x, y) < 10;
@@ -107,7 +107,7 @@ method test_secret() {
assert secret(2, 3) >= 5; // Should fail because secret's body is hidden
reveal_secret();
- assert secret(2, 3) == 5; // Should pass now that the body is "visible"
+ assert secret(2, 3) == 5; // Should pass now that the body is "visible"
assert secret(4, 1) == 7; // Make sure it catches incorrect applications as well
}
@@ -132,7 +132,7 @@ method test_recursive_f() }
// Check that opaque doesn't interfere with ensures checking
-function {:opaque} bad_ensures(x:int, y:int):int
+function {:opaque} bad_ensures(x:int, y:int):int
requires x >= 0 && y >= 0;
ensures bad_ensures(x, y) > 0;
{
@@ -172,7 +172,7 @@ method n() assert g(0) == g(0) + 1;
}
-// Check that using the reveal_ lemma to prove the well-definedness of a function
+// Check that using the reveal_ lemma to prove the well-definedness of a function
// in a lower SCC does not cause a soundness problem
function A(): int
@@ -188,4 +188,14 @@ function {:opaque} B(): int A()
}
-
+method m_noreveal()
+ ensures false;
+{
+ assert f(0) == f(0) + 1;
+}
+
+method n_noreveal()
+ ensures false;
+{
+ assert g(0) == g(0) + 1;
+}
diff --git a/Test/dafny0/FunctionSpecifications.dfy.expect b/Test/dafny0/FunctionSpecifications.dfy.expect index 545289b8..618372d8 100644 --- a/Test/dafny0/FunctionSpecifications.dfy.expect +++ b/Test/dafny0/FunctionSpecifications.dfy.expect @@ -37,20 +37,20 @@ FunctionSpecifications.dfy(130,27): Error: assertion violation Execution trace:
(0,0): anon0
(0,0): anon3_Else
-FunctionSpecifications.dfy(153,15): Error: assertion violation
+FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
-FunctionSpecifications.dfy(165,3): Error: cannot prove termination; try supplying a decreases clause
+ (0,0): anon3_Else
+FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-FunctionSpecifications.dfy(172,15): Error: assertion violation
+FunctionSpecifications.dfy(194,15): Error: assertion violation
Execution trace:
(0,0): anon0
-FunctionSpecifications.dfy(181,3): Error: cannot prove termination; try supplying a decreases clause
+FunctionSpecifications.dfy(200,15): Error: assertion violation
Execution trace:
(0,0): anon0
- (0,0): anon3_Else
FunctionSpecifications.dfy(135,20): Error BP5003: A postcondition might not hold on this return path.
FunctionSpecifications.dfy(137,29): Related location: This is the postcondition that might not hold.
Execution trace:
@@ -74,4 +74,4 @@ FunctionSpecifications.dfy(185,20): Error: cannot prove termination; try supplyi Execution trace:
(0,0): anon0
-Dafny program verifier finished with 19 verified, 17 errors
+Dafny program verifier finished with 23 verified, 17 errors
diff --git a/Test/dafny0/Modules1.dfy b/Test/dafny0/Modules1.dfy index c4e12780..2f38e39e 100644 --- a/Test/dafny0/Modules1.dfy +++ b/Test/dafny0/Modules1.dfy @@ -122,10 +122,10 @@ module Q_M { abstract module Regression {
module A
{
- predicate p(m: map)
+ predicate p<c,d>(m: map<c,d>)
- lemma m(m: map)
- ensures exists m :: p(m);
+ lemma m<a,b>(m: map<a,b>)
+ ensures exists m :: p(var m : map<a,b> := m; m);
}
abstract module B
diff --git a/Test/dafny0/MultiDimArray.dfy b/Test/dafny0/MultiDimArray.dfy index 4b4809a6..7c8ffa4a 100644 --- a/Test/dafny0/MultiDimArray.dfy +++ b/Test/dafny0/MultiDimArray.dfy @@ -10,7 +10,7 @@ class A { var e: array2 <A>;
var f: array3 <A>;
var g: array300 <A>;
- var h: array3000 <array2<int>>;
+// var h: array3000 <array2<int>>; // too big!
method M0()
requires a != null && b != null;
diff --git a/Test/dafny0/MultiSets.dfy b/Test/dafny0/MultiSets.dfy index 7478719e..3535f857 100644 --- a/Test/dafny0/MultiSets.dfy +++ b/Test/dafny0/MultiSets.dfy @@ -7,7 +7,7 @@ method test1() var ms2: multiset<int> := multiset{3};
assert 1 in ms;
assert forall i :: i != 1 ==> i !in ms; // 1 is the only thing in ms.
-
+
assert ((ms - multiset{1}) - multiset {1}) != multiset{}; // it has more than 2 ones
assert ((ms - multiset{1}) - multiset {1}) - multiset{1} == multiset{}; // and exactly three
@@ -15,7 +15,7 @@ method test1() assert ms - multiset{1} == multiset{1,1};
assert !(multiset{1} !! multiset{1});
assert exists m :: !(m !! multiset{1});
- assert forall m :: m !! multiset{};
+ assert forall m :: (var m : multiset<int> := m; m) !! multiset{};
assert forall s :: (s == set x: int | x in ms :: x) ==> s == {1};
}
@@ -163,7 +163,7 @@ class BoxTests<G> { requires forall x :: x in a ==> x in b;
ensures a <= b; // error: this property does not hold for multisets
{
- }
+ }
}
// ---------- indexing and updates ----------
diff --git a/Test/dafny0/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy index a97d63a3..d658af78 100644 --- a/Test/dafny0/NoTypeArgs.dfy +++ b/Test/dafny0/NoTypeArgs.dfy @@ -73,14 +73,14 @@ ghost method Theorem(xs: List) }
}
-ghost method Lemma(xs: List, ys: List)
+ghost method Lemma<A>(xs: List, ys: List)
ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));
{
match (xs) {
case Nil =>
- assert forall ws :: concat(ws, Nil) == ws;
+ assert forall ws :: concat(ws, Nil) == var ws : List<A> := ws; ws;
case Cons(t, rest) =>
- assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
+ assert forall a, b, c :: concat(a, concat(b, c)) == var ws : List <A> := concat(concat(a, b), c); ws;
}
}
diff --git a/Test/dafny0/OpaqueFunctions.dfy b/Test/dafny0/OpaqueFunctions.dfy index d95a6160..3b591ef2 100644 --- a/Test/dafny0/OpaqueFunctions.dfy +++ b/Test/dafny0/OpaqueFunctions.dfy @@ -157,4 +157,9 @@ module M1 refines M0 { // ---------------------------------- opaque and generics
-function{:opaque} zero<A>():int { 0 }
+function{:opaque} id<A>(x : A):A { x }
+
+datatype Box<A> = Bx(A)
+
+function{:opaque} id_box(x : Box):Box { x }
+
diff --git a/Test/dafny0/OpaqueFunctions.dfy.expect b/Test/dafny0/OpaqueFunctions.dfy.expect index 51e298b4..9d4497dc 100644 --- a/Test/dafny0/OpaqueFunctions.dfy.expect +++ b/Test/dafny0/OpaqueFunctions.dfy.expect @@ -72,4 +72,4 @@ OpaqueFunctions.dfy(138,12): Error: assertion violation Execution trace:
(0,0): anon0
-Dafny program verifier finished with 43 verified, 19 errors
+Dafny program verifier finished with 45 verified, 19 errors
diff --git a/Test/dafny0/OpaqueFunctionsFail.dfy b/Test/dafny0/OpaqueFunctionsFail.dfy new file mode 100644 index 00000000..ae7f81f6 --- /dev/null +++ b/Test/dafny0/OpaqueFunctionsFail.dfy @@ -0,0 +1,10 @@ + +// ---------------------------------- opaque and generics + +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +// This function cannot normally be called, so the +// generated opaquity code contains such a bad call. +function{:opaque} zero<A>():int { 0 } + diff --git a/Test/dafny0/OpaqueFunctionsFail.dfy.expect b/Test/dafny0/OpaqueFunctionsFail.dfy.expect new file mode 100644 index 00000000..8c2638c3 --- /dev/null +++ b/Test/dafny0/OpaqueFunctionsFail.dfy.expect @@ -0,0 +1,4 @@ +OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called. +OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to 'zero' could not determined +OpaqueFunctionsFail.dfy(9,18): Error: type variable 'A' in the function call to '#zero_FULL' could not determined. If you are making an opaque function, make sure that the function can be called. +3 resolution/type errors detected in OpaqueFunctionsFail.dfy diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 5b550339..137aa92c 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -961,3 +961,25 @@ method TypeConversions(m: nat, i: int, r: real) returns (n: nat, j: int, s: real j := int(j); // error: cannot convert int->int
j := int(n); // error: cannot convert nat->int
}
+
+// --- filling in type arguments and checking that there aren't too many ---
+
+module TypeArgumentCount {
+ class C<T> {
+ var f: T;
+ }
+
+ method R0(a: array3, c: C)
+
+ method R1()
+ {
+ var a: array3;
+ var c: C;
+ }
+
+ method R2<T>()
+ {
+ var a: array3<T,int>; // error: too many type arguments
+ var c: C<T,int>; // error: too many type arguments
+ }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index c136bc5b..d768fc3e 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -2,7 +2,8 @@ ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
-ResolutionErrors.dfy(565,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly
+ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not determined
+ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not determined
ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements
@@ -53,6 +54,8 @@ ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements ( ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
+ResolutionErrors.dfy(964,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
+ResolutionErrors.dfy(965,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
ResolutionErrors.dfy(429,2): Error: More than one default constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index a4afecff..4c4d01d8 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -514,7 +514,7 @@ static method TestAttributesVarDecls() {
var {:foo} foo;
var {:bar} bar := 0;
- var {:foo} {:bar} foobar := {};
+ var {:foo} {:bar} foobar : set<int> := {};
var {:baz} baz, {:foobaz} foobaz := true, false;
}
diff --git a/Test/dafny0/Superposition.dfy.expect b/Test/dafny0/Superposition.dfy.expect index b3f2d9ad..2e988bfb 100644 --- a/Test/dafny0/Superposition.dfy.expect +++ b/Test/dafny0/Superposition.dfy.expect @@ -3,13 +3,13 @@ Verifying CheckWellformed$$_0_M0.C.M ... [0 proof obligations] verified
Verifying Impl$$_0_M0.C.M ...
- [4 proof obligations] verified
+ [5 proof obligations] verified
Verifying CheckWellformed$$_0_M0.C.P ...
- [4 proof obligations] verified
+ [6 proof obligations] verified
Verifying CheckWellformed$$_0_M0.C.Q ...
- [3 proof obligations] error
+ [5 proof obligations] error
Superposition.dfy(27,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(28,26): Related location: This is the postcondition that might not hold.
Execution trace:
@@ -17,7 +17,7 @@ Execution trace: (0,0): anon5_Else
Verifying CheckWellformed$$_0_M0.C.R ...
- [3 proof obligations] error
+ [5 proof obligations] error
Superposition.dfy(33,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy(34,26): Related location: This is the postcondition that might not hold.
Execution trace:
@@ -31,7 +31,7 @@ Verifying Impl$$_1_M1.C.M ... [1 proof obligation] verified
Verifying CheckWellformed$$_1_M1.C.P ...
- [1 proof obligation] error
+ [2 proof obligations] error
Superposition.dfy(50,15): Error BP5003: A postcondition might not hold on this return path.
Superposition.dfy[M1](22,26): Related location: This is the postcondition that might not hold.
Execution trace:
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 963916f0..900b6110 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -321,3 +321,35 @@ method IdentityMap(s: set<Pair>) returns (m: map) m, s := m[p.0 := p.1], s - {p};
}
}
+
+// -------------- auto filled-in type arguments for array types ------
+
+module ArrayTypeMagic {
+ method M(a: array2)
+ {
+ }
+
+ method F(b: array) returns (s: seq)
+ requires b != null;
+ {
+ return b[..];
+ }
+
+ datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)
+ datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)
+ datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)
+
+ function G(t: ArrayCubeTree): array3
+ {
+ match t
+ case Leaf(d) => d
+ case Node(l, _) => G(l)
+ }
+
+ datatype Nat = Zero | Succ(Nat)
+
+ datatype List<T> = Nil | Cons(T, List)
+
+ datatype Cell<T> = Mk(T)
+ datatype DList<T,U> = Nil(Cell) | Cons(T, U, DList)
+}
diff --git a/Test/dafny0/TypeParameters.dfy.expect b/Test/dafny0/TypeParameters.dfy.expect index 00efc26f..3d00e89a 100644 --- a/Test/dafny0/TypeParameters.dfy.expect +++ b/Test/dafny0/TypeParameters.dfy.expect @@ -49,4 +49,4 @@ Execution trace: TypeParameters.dfy(177,3): anon21_Else
TypeParameters.dfy(177,3): anon23_Else
-Dafny program verifier finished with 58 verified, 8 errors
+Dafny program verifier finished with 63 verified, 8 errors
diff --git a/Test/dafny0/snapshots/Snapshots0.v1.dfy b/Test/dafny0/snapshots/Snapshots0.v1.dfy index 28f9f283..db9fc01a 100644 --- a/Test/dafny0/snapshots/Snapshots0.v1.dfy +++ b/Test/dafny0/snapshots/Snapshots0.v1.dfy @@ -1,7 +1,7 @@ method foo()
{
bar();
- assert false;
+ assert false; // error
}
method bar()
diff --git a/Test/dafny0/snapshots/Snapshots1.v0.dfy b/Test/dafny0/snapshots/Snapshots1.v0.dfy new file mode 100644 index 00000000..dd1e7deb --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.v0.dfy @@ -0,0 +1,13 @@ +method M()
+{
+ N();
+ assert false;
+}
+
+method N()
+ ensures P;
+
+predicate P
+{
+ false
+}
diff --git a/Test/dafny0/snapshots/Snapshots1.v1.dfy b/Test/dafny0/snapshots/Snapshots1.v1.dfy new file mode 100644 index 00000000..93ad6068 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots1.v1.dfy @@ -0,0 +1,13 @@ +method M()
+{
+ N();
+ assert false; // error
+}
+
+method N()
+ ensures P;
+
+predicate P
+{
+ true
+}
diff --git a/Test/dafny0/snapshots/Snapshots2.v0.dfy b/Test/dafny0/snapshots/Snapshots2.v0.dfy new file mode 100644 index 00000000..37b9982b --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.v0.dfy @@ -0,0 +1,19 @@ +method M()
+{
+ N();
+ assert false;
+}
+
+method N()
+ ensures P;
+
+predicate P
+ ensures P == Q;
+
+predicate Q
+ ensures Q == R;
+
+predicate R
+{
+ false
+}
diff --git a/Test/dafny0/snapshots/Snapshots2.v1.dfy b/Test/dafny0/snapshots/Snapshots2.v1.dfy new file mode 100644 index 00000000..03719744 --- /dev/null +++ b/Test/dafny0/snapshots/Snapshots2.v1.dfy @@ -0,0 +1,19 @@ +method M()
+{
+ N();
+ assert false; // error
+}
+
+method N()
+ ensures P;
+
+predicate P
+ ensures P == Q;
+
+predicate Q
+ ensures Q == R;
+
+predicate R
+{
+ true
+}
diff --git a/Test/dafny0/snapshots/runtest.snapshot b/Test/dafny0/snapshots/runtest.snapshot index 6d2f880f..c3cf6b00 100644 --- a/Test/dafny0/snapshots/runtest.snapshot +++ b/Test/dafny0/snapshots/runtest.snapshot @@ -1,2 +1,2 @@ -// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy > "%t" +// RUN: %dafny /compile:0 /verifySnapshots:2 /verifySeparately Snapshots0.dfy Snapshots1.dfy Snapshots2.dfy > "%t" // RUN: %diff "%s.expect" "%t" diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect index 7906e7a5..87827811 100644 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -1,7 +1,27 @@ +-------------------- Snapshots0.dfy --------------------
+
Dafny program verifier finished with 3 verified, 0 errors
Snapshots0.v1.dfy(4,10): Error: assertion violation
Execution trace:
(0,0): anon0
Dafny program verifier finished with 2 verified, 1 error
+
+-------------------- Snapshots1.dfy --------------------
+
+Dafny program verifier finished with 4 verified, 0 errors
+Snapshots1.v1.dfy(4,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 3 verified, 1 error
+
+-------------------- Snapshots2.dfy --------------------
+
+Dafny program verifier finished with 6 verified, 0 errors
+Snapshots2.v1.dfy(4,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 5 verified, 1 error
diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy index 7e5ab205..360c5aba 100644 --- a/Test/dafny1/Celebrity.dfy +++ b/Test/dafny1/Celebrity.dfy @@ -3,16 +3,16 @@ // Celebrity example, inspired by the Rodin tutorial
-static function method Knows<Person>(a: Person, b: Person): bool
+static function method Knows<X>(a: X, b: X): bool
requires a != b; // forbid asking about the reflexive case
-static function IsCelebrity<Person>(c: Person, people: set<Person>): bool
+static function IsCelebrity<Y>(c: Y, people: set<Y>): bool
{
c in people &&
(forall p :: p in people && p != c ==> Knows(p, c) && !Knows(c, p))
}
-method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity0<Z>(people: set<Z>, ghost c: Z) returns (r: Z)
requires exists c :: IsCelebrity(c, people);
ensures r == c;
{
@@ -20,7 +20,7 @@ method FindCelebrity0<Person>(people: set<Person>, ghost c: Person) returns (r: r := cc;
}
-method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity1<W>(people: set<W>, ghost c: W) returns (r: W)
requires IsCelebrity(c, people);
ensures r == c;
{
@@ -43,7 +43,7 @@ method FindCelebrity1<Person>(people: set<Person>, ghost c: Person) returns (r: r := x;
}
-method FindCelebrity2<Person>(people: set<Person>, ghost c: Person) returns (r: Person)
+method FindCelebrity2<V>(people: set<V>, ghost c: V) returns (r: V)
requires IsCelebrity(c, people);
ensures r == c;
{
diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy index d71c735f..a52f994b 100644 --- a/Test/dafny1/MoreInduction.dfy +++ b/Test/dafny1/MoreInduction.dfy @@ -4,7 +4,7 @@ datatype List<X> = Nil | Cons(Node<X>, List<X>);
datatype Node<X> = Element(X) | Nary(List<X>);
-function FlattenMain<X>(list: List<X>): List<X>
+function FlattenMain<M>(list: List<M>): List<M>
ensures IsFlat(FlattenMain(list));
{
Flatten(list, Nil)
@@ -22,7 +22,7 @@ function Flatten<X>(list: List<X>, ext: List<X>): List<X> case Nary(nn) => Flatten(nn, Flatten(rest, ext))
}
-function IsFlat<X>(list: List<X>): bool
+function IsFlat<F>(list: List<F>): bool
{
match list
case Nil => true
diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy index 7b2e7eda..a51a9fd0 100644 --- a/Test/dafny1/SchorrWaite-stages.dfy +++ b/Test/dafny1/SchorrWaite-stages.dfy @@ -176,6 +176,7 @@ abstract module M1 refines M0 { // 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 ...;
+ assume ...;
}
}
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy index 56f689da..ee56e14a 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy @@ -208,6 +208,14 @@ class Node { decreases S - Visited;
{
p, steps, Visited := p.next, steps + 1, Visited + {p};
+
+ // with all: 3s
+ // without this: 20s
+ assert forall t :: 0 <= t < steps ==> Nexxxt(t, S) in Visited;
+ // without this: 5s
+ assert forall q :: q in (Visited - {null}) ==> exists t :: 0 <= t < steps && Nexxxt(t, S) == q;
+ // without this: >60s
+ assert forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S);
}
if (p == null) {
A, B := steps, 1;
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 10004332..4b8c9b4c 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -41,13 +41,13 @@ function qreverse(l: List): List // Here are two lemmas about the List functions.
-ghost method Lemma_ConcatNil()
- ensures forall xs :: concat(xs, Nil) == xs;
+ghost method Lemma_ConcatNil(xs : List)
+ ensures concat(xs, Nil) == xs;
{
}
-ghost method Lemma_RevCatCommute()
- ensures forall xs, ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);
+ghost method Lemma_RevCatCommute(xs : List)
+ ensures forall ys, zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs);
{
}
@@ -64,7 +64,7 @@ ghost method Theorem_QReverseIsCorrect_Calc(l: List) revacc(l, Nil);
{ Lemma_Revacc_calc(l, Nil); }
concat(reverse(l), Nil);
- { Lemma_ConcatNil(); }
+ { Lemma_ConcatNil(reverse(l)); }
reverse(l);
}
}
@@ -81,7 +81,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List) concat(concat(reverse(xrest), Cons(x, Nil)), ys);
// induction hypothesis: Lemma_Revacc_calc(xrest, Cons(x, Nil))
concat(revacc(xrest, Cons(x, Nil)), ys);
- { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ { Lemma_RevCatCommute(xrest); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
revacc(xrest, concat(Cons(x, Nil), ys));
// def. concat (x2)
revacc(xrest, Cons(x, ys));
@@ -102,7 +102,7 @@ ghost method Theorem_QReverseIsCorrect(l: List) Lemma_Revacc(l, Nil);
assert revacc(l, Nil)
== concat(reverse(l), Nil);
- Lemma_ConcatNil();
+ Lemma_ConcatNil(reverse(l));
}
ghost method Lemma_Revacc(xs: List, ys: List)
@@ -120,7 +120,7 @@ ghost method Lemma_Revacc(xs: List, ys: List) concat(concat(reverse(xrest), Cons(x, Nil)), ys)
== // induction hypothesis: Lemma_Revacc(xrest, Cons(x, Nil))
concat(revacc(xrest, Cons(x, Nil)), ys);
- Lemma_RevCatCommute(); // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
+ Lemma_RevCatCommute(xrest); // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs)
assert concat(revacc(xrest, Cons(x, Nil)), ys)
== revacc(xrest, concat(Cons(x, Nil), ys));
@@ -181,7 +181,7 @@ ghost method Lemma_Reverse_Length(xs: List) calc {
length(Cons(x, Nil));
// def. length
- 1 + length(Nil);
+ // 1 + length(Nil); // ambigious type parameter
// def. length
1 + 0;
1;
@@ -231,7 +231,7 @@ ghost method lemma_extensionality(xs: List, ys: List) ensures xs == ys;
{
match xs {
- case Nil =>
+ case Nil =>
calc {
true;
// (0)
@@ -255,7 +255,7 @@ ghost method lemma_extensionality(xs: List, ys: List) y;
}
Cons(y, xrest);
- {
+ {
forall (j: nat | j < length(xrest)) {
calc {
ith(xrest, j);
@@ -265,7 +265,7 @@ ghost method lemma_extensionality(xs: List, ys: List) ith(yrest, j);
}
}
- lemma_extensionality(xrest, yrest);
+ lemma_extensionality(xrest, yrest);
}
Cons(y, yrest);
ys;
diff --git a/Test/dafny2/TreeFill.dfy b/Test/dafny2/TreeFill.dfy index fdd73a1a..9bc95276 100644 --- a/Test/dafny2/TreeFill.dfy +++ b/Test/dafny2/TreeFill.dfy @@ -28,3 +28,4 @@ method Fill<T>(t: Tree, a: array<T>, start: int) returns (end: int) }
}
}
+
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy index e90687e0..acc29ccd 100644 --- a/Test/dafny3/Dijkstra.dfy +++ b/Test/dafny3/Dijkstra.dfy @@ -65,7 +65,7 @@ ghost method lemma_pong(n: nat) <== { lemma_monotonicity_0(n + 1, f(n)); }
f(f(n)) < f(n + 1);
== // P with m := n
- true;
+ true;
}
}
diff --git a/Test/dafny3/InfiniteTrees.dfy b/Test/dafny3/InfiniteTrees.dfy index 030443c0..516a9e4e 100644 --- a/Test/dafny3/InfiniteTrees.dfy +++ b/Test/dafny3/InfiniteTrees.dfy @@ -38,7 +38,7 @@ lemma Tail_Lemma2(s: Stream, n: nat) // Co-predicate IsNeverEndingStream(s) answers whether or not s ever contains Nil.
-copredicate IsNeverEndingStream(s: Stream)
+copredicate IsNeverEndingStream<S>(s: Stream<S>)
{
match s
case Nil => false
@@ -247,7 +247,8 @@ lemma ValidPath_Lemma(p: Stream<int>) match p {
case Nil =>
case Cons(index, tail) => // proof by contradiction
- Tail_Lemma1(Nil, 0, index);
+ var nil : Stream<Tree> := Nil;
+ Tail_Lemma1(nil, 0, index);
}
}
}
diff --git a/Test/dafny3/OpaqueTrees.dfy b/Test/dafny3/OpaqueTrees.dfy index 53540c1d..432d107a 100644 --- a/Test/dafny3/OpaqueTrees.dfy +++ b/Test/dafny3/OpaqueTrees.dfy @@ -10,7 +10,7 @@ function {:opaque} size(t: Tree): nat case Node(left, right) => 1 + size(left) + size(right)
}
-function {:opaque} mirror(t: Tree): Tree
+function {:opaque} mirror<T>(t: Tree<T>): Tree<T>
{
match t
case Leaf(_) => t
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy index d7c142ee..5b7f3a0f 100644 --- a/Test/dafny4/NumberRepresentations.dfy +++ b/Test/dafny4/NumberRepresentations.dfy @@ -8,6 +8,7 @@ function eval(digits: seq<int>, base: int): int
requires 2 <= base;
+ decreases digits; // see comment in test_eval()
{
if |digits| == 0 then 0 else digits[0] + base * eval(digits[1..], base)
}
@@ -16,36 +17,21 @@ lemma test_eval() {
assert forall base :: 2 <= base ==> eval([], base) == 0;
assert forall base :: 2 <= base ==> eval([0], base) == 0;
- forall base | 2 <= base {
- calc {
- eval([0, 0], base);
- 0;
- }
- }
- calc {
- eval([3, 2], 10);
- 3 + 10 * eval([2], 10);
- 23;
- }
+ // To prove this automatically, it is necessary that the Lit axiom is sensitive only to the
+ // 'digits' argument being a literal. Hence, the explicit 'decreases digits' clause on the
+ // 'eval' function.
+ assert forall base :: 2 <= base ==> eval([0, 0], base) == 0;
+
+ assert eval([3, 2], 10) == 23;
+
var oct, dec := 8, 10;
- calc {
- eval([1, 3], oct);
- 1 + oct * eval([3], oct);
- 5 + dec * eval([2], dec);
- eval([5, 2], dec);
- }
+ assert eval([1, 3], oct) == eval([5, 2], dec);
assert eval([29], 420) == 29;
assert eval([29], 8) == 29;
- calc {
- eval([-2, 1, -3], 5);
- -2 + 5 * eval([1, -3], 5);
- -2 + 5 * 1 + 25 * eval([-3], 5);
- -2 + 5 * 1 + 25 * (-3);
- -72;
- }
+ assert eval([-2, 1, -3], 5) == -72;
}
// To achieve a unique (except for leading zeros) representation of each number, we
diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg index c9597a4c..d0b3a85b 100644 --- a/Test/lit.site.cfg +++ b/Test/lit.site.cfg @@ -125,7 +125,7 @@ else: lit_config.warning('Skipping solver sanity check on Windows') # Add diff tool substitution -commonDiffFlags=' --unified=3 --strip-trailing-cr --ignore-all-space' +commonDiffFlags=' --unified=3 --strip-trailing-cr' diffExecutable = None if os.name == 'posix': diffExecutable = 'diff' + commonDiffFlags diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy index 06fca9f0..1e54f02f 100644 --- a/Test/vacid0/SparseArray.dfy +++ b/Test/vacid0/SparseArray.dfy @@ -40,8 +40,8 @@ class SparseArray<T> { ensures |Contents| == N && this.zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
- var aa := AllocateArray(N); this.a := aa;
- var bb := AllocateArray(N); this.b := bb;
+ var aa : seq<T> := AllocateArray(N); this.a := aa;
+ var bb : seq<int> := AllocateArray(N); this.b := bb;
bb := AllocateArray(N); this.c := bb;
this.n := 0;
@@ -101,19 +101,20 @@ class SparseArray<T> { Contents := Contents[i := x];
}
- /* The following method is here only to simulate support of arrays in Dafny */
- /*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
- requires 0 <= n;
- ensures |arr| == n;
+}
+
+/* The following method is here only to simulate support of arrays in Dafny */
+/*private*/ static method AllocateArray<G>(n: int) returns (arr: seq<G>)
+ requires 0 <= n;
+ ensures |arr| == n;
+{
+ arr := [];
+ var i := 0;
+ while (i < n)
+ invariant i <= n && |arr| == i;
{
- arr := [];
- var i := 0;
- while (i < n)
- invariant i <= n && |arr| == i;
- {
- var g: G;
- arr := arr + [g];
- i := i + 1;
- }
+ var g: G;
+ arr := arr + [g];
+ i := i + 1;
}
}
diff --git a/Test/vstte2012/Tree.dfy b/Test/vstte2012/Tree.dfy index 0bfce265..82192e6d 100644 --- a/Test/vstte2012/Tree.dfy +++ b/Test/vstte2012/Tree.dfy @@ -26,7 +26,7 @@ function toList(d: int, t: Tree): seq<int> ensures (toList(d, t)[0] == d) == (t == Leaf);
decreases t;
{
- match t
+ match t
case Leaf => [d]
case Node(l, r) => toList(d+1, l) + toList(d+1, r)
}
@@ -42,11 +42,11 @@ function toList(d: int, t: Tree): seq<int> // sequence that has been consumed.
function method build_rec(d: int, s: seq<int>): Result
ensures build_rec(d, s).Res? ==>
- |build_rec(d, s).sOut| < |s| &&
+ |build_rec(d, s).sOut| < |s| &&
build_rec(d, s).sOut == s[|s|-|build_rec(d, s).sOut|..];
- ensures build_rec(d, s).Res? ==>
+ ensures build_rec(d, s).Res? ==>
toList(d,build_rec(d, s).t) == s[..|s|-|build_rec(d, s).sOut|];
- decreases |s|, (if s==[] then 0 else s[0]-d);
+ decreases |s|, (if s==[] then 0 else s[0]-d);
{
if s==[] || s[0] < d then
Fail
@@ -85,7 +85,7 @@ function method build(s: seq<int>): Result // ensures that the induction hypothesis is applied
// correctly (encoded by calls to this ghost method).
ghost method lemma0(t: Tree, d: int, s: seq<int>)
- ensures build_rec(d, toList(d, t) + s).Res? &&
+ ensures build_rec(d, toList(d, t) + s).Res? &&
build_rec(d, toList(d, t) + s).sOut == s;
{
match(t) {
@@ -121,12 +121,12 @@ ghost method lemma2(s: seq<int>) {
forall t | toList(0,t) == s {
lemma1(t, s);
- }
+ }
}
// This ghost method encodes the completeness theorem.
-// For each sequence for which there is a corresponding
+// For each sequence for which there is a corresponding
// tree, function build yields a result different from Fail.
// The body of the method converts the argument of lemma2
// into a universally quantified variable.
@@ -170,6 +170,8 @@ method harness0() method harness1()
ensures build([1,3,2,2]).Fail?;
{
- assert build_rec(3, [2,2]).Fail?;
- assert build_rec(1, [3,2,2]).Fail?;
+ assert build_rec(1,[1,3,2,2]) == Res(Leaf, [3,2,2]);
+ assert build_rec(3,[2,2]).Fail?;
+ assert build_rec(2,[3,2,2]).Fail?;
+ assert build_rec(1,[3,2,2]).Fail?;
}
|