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 | a13064f11fd9609c124f53616ff358623e8bf88c (patch) | |
| tree | 8ac952bfe260a53e1575665c4880744facd0d94d /Test/dafny0/SmallTests.dfy | |
| parent | ce54aa2ac282e71ac77b4f91721061ba5c2e3d4a (diff) | |
Dafny: Test case for sequence of boxed booleans
Diffstat (limited to 'Test/dafny0/SmallTests.dfy')
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 10 |
1 files changed, 10 insertions, 0 deletions
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];
+}
|