diff options
| author |  Jason Koenig <unknown> | 2011-07-11 17:22:32 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-07-11 17:22:32 -0700 |
| commit | bb6f5a2ad132f7d5553b4506f00bced4f1af3c73 (patch) | |
| tree | 5175078397fff173c81ff3a279ad5c85cf0f91dc /Test/dafny0/Array.dfy | |
| parent | 32bd4d4b3b892d0bbace511372ca53dd8ffad63c (diff) | |
Added s[..] syntax in anticipation of sequence forming operation. (also updated regression tests.)
Diffstat (limited to 'Test/dafny0/Array.dfy')
| -rw-r--r-- | Test/dafny0/Array.dfy | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 60854f63..5f366d10 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -93,6 +93,9 @@ class A { assert y[8] == 30;
assert y[90] + y[91] + y[0] + 20 == y.Length;
assert y[93] == 24; // error (it's 25)
+
+ y[..] := 4; // assign to all elements.
+ assert forall i :: 0 <= i < y.Length ==> y[i] == 4;
}
}
|