Sequences and 'update' function from tutorial

Feb 6, 2014 at 4:56 PM
Hello,

I was experimenting with the 'update' function from the sequences tutorial. I changed the function to a function method just to play and to get a better understanding of what Dafny knows of sequences. However, there were weird results using the 'in' operator to test if the elements in the old sequence were in the new sequence.

What I was trying to do: if I wanted to add a new element '5' to the middle of the sequence, s, [0, 1, 2, 3], I should be able to create a new sequence, s_0, [0, 1, 5, 2, 3] using concatenation (I may not have the positioning of '5' correct, but I'm only interested in inserting '5' somewhere in the middle of the sequence). In the update function, I thought that's what its doing: slicing the beginning of the sequence, inserting '5' into the middle, and concatenating the rest of the sequence. This is demonstrated in the code below.

Here's the code I was playing with (here):
method test_sequences() {
    var s : seq<int>;
    s := s + [0];
    s := s + [1];
    
    assert 0 in s;  // verifies
    assert 1 in s;  // verifies
    
    s := s + [2];
    assert 0 in s;  // verifies
    assert 1 in s;  // verifies 
    assert 2 in s;  // verifies
        
    s := s + [3];
    
    var i := 1;
    var s_0 := update(s, i, 5);
    assert update(s, i, 5) == s[i := 5];
    assert 0 in s_0;    // doesn't verify
    assert 1 in s_0;    // doesn't verify
    assert 2 in s_0;    // does verify
    assert 3 in s_0;    // doesn't verify
    assert 5 in s_0;    // does verify
    
    
    var s_1 := remove(s, i, 2);
    // none of the assertions below verify.
    /*
    assert 0 in s_1;
    assert 1 in s_1;
    assert 2 in s_1;
    assert 3 in s_1;
    */
}

function method update(s: seq<int>, index: int, v: int): seq<int>
   requires 0 <= index < |s|;
   ensures update(s, index, v) == s[index := v];
{
   s[..index] + [v] + s[index+1..]
}


function method remove(s: seq<int>, index: int, v: int): seq<int>
   requires 0 < index < |s|;
   ensures remove(s, index, v) == s[0..index-1] + s[index+1..|s|];
{
   s[..index-1] + s[index+1..]
}
Notice after I call 'var s_0 := update(s, i, 5)', Dafny only asserts that '2' and '5' are the only elements in the new sequence! Why is that? Why does Dafny not assert that '0', '1', and '3' are also in the new sequence? Is the way I'm using the 'in' operator a valid test in this scenario?

Thanks,

Matt
Coordinator
Feb 7, 2014 at 12:00 AM
Hi Matt,

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 replaced 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 bodies:
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 example: http://rise4fun.com/Dafny/e9eW

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 + [3];  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 [8], 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 := [0];
or insert the code:
s := [];
at the end of line 2, or change line 2 to:
var s := [];
Rustan
Marked as answer by rustanleino on 2/6/2014 at 5:00 PM
Feb 7, 2014 at 4:51 PM
Thank you very much, Rustan. The explanation was very helpful and informative.

I played with the code some more, and got it to where I wanted it via your help here.

Thanks again!
Matt
Coordinator
Feb 7, 2014 at 11:53 PM
Hi Matt,

Great. One more thing. In Dafny, methods are "opaque", in the sense that a caller only sees the specification, never the implementation. In contrast, functions (in the same module) are transparent. This means that the caller gets to "see" the body of the function. For this reason, you often don't need to give any "ensures" clauses of functions; in particular, it is not needed in your example, see http://rise4fun.com/Dafny/kXxZ.

There are some cases where postconditions ("ensures" clauses) on functions is useful. One such case is if the function is recursive, because Dafny will only do a small, fixed number of unrollings of the function when reasoning about it. So, suppose you have a function that computes the factorial and you want to say that Factorial(n) is always at least n. This property cannot be inferred automatically, so you will need a postcondition for Factorial (http://rise4fun.com/Dafny/iCZT ):
function Factorial(n: nat): nat
  ensures n <= Factorial(n);
{
  if n == 0 then 1 else n * Factorial(n-1)
}

method Test(k: int)
  requires 1000 <= k;
{
  assert 1000 <= Factorial(k);
}
Alternatively, you can write a separate lemma that proves this property about Factorial, like this (http://rise4fun.com/Dafny/B0hR ):
function Factorial(n: nat): nat
{
  if n == 0 then 1 else n * Factorial(n-1)
}

lemma FactorialProperty(n: nat)
  ensures n <= Factorial(n);
{
}

method Test(k: int)
  requires 1000 <= k;
{
  FactorialProperty(k);
  assert 1000 <= Factorial(k);
}
The other case where you may need to use a postcondition of (or, again, a lemma about) a function is when the function is to be used outside the module. The reason for this is that Dafny treats inter-module functions (and predicates) as being opaque -- only their declared postconditions are "exported" to other modules.

Rustan
Feb 10, 2014 at 8:22 PM
Thanks for the tip, Rustan. The less postconditions I have to write, the better :)

Matt