diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-16 18:24:57 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-16 18:24:57 -0700 |
| commit | c76d588dd2768de8505d3d08f43f3de0b5f84dae (patch) | |
| tree | 9773259335b63a5772d6df44cfd9eed9b49da72d /Test | |
| parent | 5dcda744e4ace3b8f627fe98ac837ec10624272d (diff) | |
Dafny: Test case for sequence of boxed booleans
Diffstat (limited to 'Test')
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 10 |
2 files changed, 11 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 070aa6be..2463b0e5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -209,7 +209,7 @@ Execution trace: (0,0): anon15
(0,0): anon25_Else
-Dafny program verifier finished with 39 verified, 14 errors
+Dafny program verifier finished with 41 verified, 14 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index ef2049a3..a5f02dc6 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -308,3 +308,13 @@ method QuantifierRange2<T>(a: seq<T>, x: T, y: T, N: int) assert x == y;
}
}
+
+// ----------------------- tests that involve sequences of boxed booleans --------
+
+ghost method M(zeros: seq<bool>, Z: bool)
+ requires 1 <= |zeros| && Z == false;
+ requires forall k :: 0 <= k && k < |zeros| ==> zeros[k] == Z;
+{
+ var x := [Z];
+ assert zeros[0..1] == [Z];
+}
|