All intervals in Dafny are half-open (that is, inclusive on the left and exclusive on the right). That is, when you write something like s[5..8], the subsequence of s that you get is obtained by dropping the first 5 elements and then giving you the next 8-5
elements. In other words, s[5..8] is the subsequence of s that starts at index 5 and has length 8-5 = 3. Stated yet one more way (and assuming 8 < |s|), 5 is the index of the first element you get and 8 is the index of the first element after what you get.
In some mathematical texts, you see a syntax like [5..8) to indicate that the interval is half-open. However, I chose not to do it this way in Dafny, because text editors don't do well with parenthesis matching for different kinds of parentheses. However, since
Dafny is consistent about using half-open intervals, there are no syntactic ambiguities (once you know what the notation means in the first place).
Half-open intervals have nice properties, two of which are the following: For a, b, c, and s such that 0 <= a <= b <= c <= |s|, we have
s[a..b] + s[b..c] == s[a..c]
Furthermore, for a, b, and s such 0 <= a <= b <= |s|,
|s[a..b]| == b - a
Another property is:
s == s[0..|s|]
and, indeed, an omitted lower bound defaults to 0 and an omitted upper bound defaults to |s|. To some functional programmers, the expression s[n..] is known as drop(n, s) and s[..n] is known as take(n, s).
The expression s[j := v] returns a sequence that is like s, except that the element at index j is
by v. Indeed, your function "update" does not return the original element s[index]. Similarly, your function "remove" removes two elements. You had probably intended for these functions to have the following respective
s[..index] + [v] + s[index..] // "index" is used twice, so no elements are lost
s[..index] + s[index+1..] // here, "index" and "index+1" are used, which tells you that (index+1) - index = 1 elements are removed
Dafny's handling of sequences is not complete, in the sense that it frequently happens that properties that you may think are obvious are not automatically known to Dafny. For that reason, you may have to help Dafny along by giving assertions. Here is a simple
Let me explain what's going on with the assertions in your program.
Dafny complains about the assertion
assert 3 in s_0;
on line 22 of your program. This is due to the incomplete automation of sequences. If you help Dafny along with an assertion (which will have the effect of a lemma) after appending 3 to s, by changing line 14 to:
s := s + ; assert 3 in s;
then Dafny will be able to prove the assertion on line 22. (You may ask, "How do I know I need an assertion there?". Often, you don't. My suggestion would be to just be aware of Dafny's incompleteness with respect to sequences, so try some assertions
like this if you find that Dafny doesn't automatically prove what you want you expect.)
For the other assertions that Dafny complains about, it is right to complain, because they may not hold in your program. Since I've now explained above that the s[j := v] does not insert (but, rather replaces) an element in a sequence, it should be no surprise
that "assert 1 in s;" may not hold after the call to "update". But you may wonder how come "assert 0 in s;" does not verify. The reason is that you didn't initialize local variable s, so Dafny will consider its initial value to
be any value of the type. For example, if the initial value of s is a length-1 sequence, like , then s will have the value [8,0,1,2,3] by the time you call "update", and then "update" will return the sequence [8,5,1,2,3], which does
not contain any 0. To fix this, change line 3 to:
s := ;
or insert the code:
s := ;
at the end of line 2, or change line 2 to:
var s := ;