Dec 4, 2010 at 8:42 PM
Edited Dec 6, 2010 at 6:35 PM

EDIT: Nvm I solved it just expressed the post condition in another way. Mod can delete this topic now!



I just looked at your emaple anyway. The problem is that the loop invariant was wrong. Here is a version that verifies. Note that the range of the minoperator in the loop invariant needs to go until a.Length (not i). I also cleaned up the method body a
bit.
Peter
static void selectionSort(int[]! a)
modifies a[*];
ensures forall{int k in (0:a.Length); a[k]==min{int l in (k: a.Length); a[l]}};
{
int smallest = 0;
int i = 0;
int temp = 0;
if (a.Length>1) {
while (i<a.Length)
invariant 0<=i && i<=a.Length;
invariant forall{int k in(0:i); a[k]==min{int l in (k:a.Length); a[l]}};
{
smallest = returnMinIndex(a,i);
temp = a[i];
a[i]=a[smallest];
a[smallest]=temp;
i++;
}
}
}

