Insertion sort is stable

  • fully automatic
  • but why3 0.82 cannot prove invariant 'stable a' in inner loop. Need twice inlined manually!!

    module InsertionSortStable
    
     use import int.Int
     use import ref.Ref
     use import array.Array
     use import array.ArrayPermut
    
     type eltpair 'a 'b = {v: 'a; attr: 'b}
    
     predicate sorted_sub (a : array (eltpair int int)) (l u: int) =
        forall i1 i2 : int.
           l <= i1 <= i2 < u -> a[i1].v <= a[i2].v
    
     predicate sorted (a : array (eltpair int int)) = sorted_sub a 0 (length a)
    
     predicate stable_sub (a : array (eltpair int int)) (l u: int) =
        forall i1 i2 : int.
           l <= i1 <= i2 < u -> a[i1].v = a[i2].v -> a[i1].attr <= a[i2].attr
    
     predicate stable (a : array (eltpair int int)) = stable_sub a 0 (length a)
    
     let swap (a: array (eltpair int int)) (i: int) (j: int) =
       requires { 0 <= i < length a /\ 0 <= j < length a }
       ensures { exchange (old a) a i j }
      let v = a[i] in
       a[i] <- a[j];
       a[j] <- v
    
     let insertionSortStable (a: array (eltpair int int)) =
       requires { stable a }
       ensures { stable a }
    'L:
       for i = 1 to length a - 1 do
        invariant { stable a }
         let j = ref i in
         while !j > 0 && a[!j - 1].v > a[!j].v do
         invariant { 0 <= !j <= i }
    (*   invariant { stable a }  *)
         invariant {forall i1 i2 : int. 0 <= i1 <= i2 < (length a) -> a[i1].v = a[i2].v -> a[i1].attr <= a[i2].attr }
           swap a (!j-1) !j;
           j := !j - 1
         done
       done
    
    end
    

  • Generated by why3doc 0.85