Refuses to verify complete -- verifier loops forever

Dec 4, 2010 at 7:42 PM
Edited Dec 6, 2010 at 5:35 PM

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

Dec 13, 2010 at 12:49 PM

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 min-operator in the loop invariant needs to go until a.Length (not i). I also cleaned up the method body a bit.


  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];