Non-trivial termination

Apr 28, 2014 at 9:14 PM
I have the following code: http://rise4fun.com/Dafny/frkY

The code trivially sets the value of each array element to its index (requiring initially that this is not the case, for all indices).

I am using a slightly non-trivial termination condition. As you can see, Dafny agrees with the assertions in the code that variable s is indeed greater than s'. Hence it seems to me that s is an appropriate variant for the loop.

However, Dafny does not agree. How could I fix this? In general, how would I be able to add a lemma for a variant? As opposed to pre and post conditions, it appears that I need two mathematical variables but have just a single state variable.
Coordinator
May 3, 2014 at 4:17 PM
The problem is that nothing is known about s at the beginning of the loop body. Such information needs to be supplied using a loop invariant, like this: http://rise4fun.com/Dafny/QMaS

Instead of using a loop invariant, your attempt had used an assignment to s inside the loop body. It so happened that you were assigning to s the value that it already had, but that would be known to Dafny only with a loop invariant. In general, if you just assign an arbitrary value to such a variable, then termination does not follow:
var i:=0;
var s := 1000;
while true
  decreases s;
{
  s := 29;    
  i:=i+1;
  var s' := 4;
  assert s' < s;  // yes, but this does not ensure termination of the loop
  s := s;
}
Btw, as you may know, Dafny allows you to achieve the postcondition of your method without using a loop. You can use the aggregate statement forall:
forall i | 0 <= i < L.Length {
  a[i] := i;
}
Rustan
Marked as answer by rustanleino on 5/3/2014 at 9:17 AM
May 3, 2014 at 7:59 PM
Thank you Rustan, you make a compelling point with your example.

One last question regarding this issue. In the following simplified code I avoid using a variable for the termination measure altogether: http://rise4fun.com/Dafny/JvTU.

It appears that the lemmas are the same, and that now Dafny should know the value of set x| i<=x<L.Length && L[x]!=x at the top of the loop. What am I missing here?