Added s[..] syntax in anticipation of sequence forming operation. (also updated regression tests.)

2 files changed, 7 insertions, 4 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 7a972f22..a6f1e9b7 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -487,20 +487,20 @@ Execution trace:
 Array.dfy(95,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Array.dfy(107,6): Error: insufficient reads clause to read array element

+Array.dfy(110,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(115,6): Error: insufficient reads clause to read array element

+Array.dfy(118,6): Error: insufficient reads clause to read array element

 Execution trace:

     (0,0): anon7_Else

     (0,0): anon8_Then

     (0,0): anon9_Then

-Array.dfy(131,6): Error: assignment may update an array element not in the enclosing context's modifies clause

+Array.dfy(134,6): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

-Array.dfy(138,6): Error: assignment may update an array element not in the enclosing context's modifies clause

+Array.dfy(141,6): Error: assignment may update an array element not in the enclosing context's modifies clause

 Execution trace:

     (0,0): anon0

 

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;

   }

 }