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 min-operator 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++;
        }
     }    
  }