Error: assignment may update an array element not in the enclosing context's modifies clause

May 6, 2014 at 5:54 PM
Hi, I try to specify and proof a method to sort an array of integers.
I write the pre and post conditions and then the code. When execute dafny this message error was display: Error: assignment may update an array element not in the enclosing context's modifies clause

What this means? What is wrong?

method Ordenar(a: array<int>) returns (b: array<int>)
requires a != null && a.Length > 0;
ensures forall j :: 0 <= j < a.Length-1 ==> a[j] <= a[j+1];
{
var aux := 0;
var i := 0;
var x := 0;

while (i < a.Length - 1)
{
 x := i + 1;
 while ( x < a.Length )
 {
   if (a[x] < a[i]) {
     aux := a[i];
     a[i] := a[x];
     a[x] := aux;
    }
    x:= x + 1;
 }
 i:= i + 1;
}
return a;
}
May 6, 2014 at 6:01 PM
A method specification must say what the method may modify. In this case, you want to say that the method is allowed to modify the elements of the array, so you should add
modifies a;
to the specification of your method.

Rustan
May 6, 2014 at 6:06 PM
Thank you very much Rustan!