Quicksort with Bentley-Bull trick

in 0.82, Coq used 2 times to prove:

  • sorted a (i+1) n needs lemma with sorted_div_sorted. (Coq uses lemma proved by Alt-ergo
  • permut (postcondition) needs permut_weakening
  • Z3 used (after inline transformation) in 2nd partition assertion.

    in 0.83, fully automatic but with combining Alt-ergo, Yices, Z3.

    module QuickSort
    
      use import int.Int
      use import ref.Ref
      use import array.Array
      use import array.IntArraySorted
      use import array.ArrayPermut
      use import array.ArrayEq
    
      predicate div_sub (a: array int) (l m u: int) =
      (forall i: int. l <= i < m -> a[i] <= a[m]) /\
      (forall j: int. m+1 <= j < u -> a[m] <= a[j])
    
      lemma sorted_div_sorted_sub:
        forall a: array int. forall l m u : int.
           sorted_sub a l m -> div_sub a l m u -> sorted_sub a (m+1) u
          -> sorted_sub a l u
    
      lemma permut_sub_trans:
        forall a1 a2 a3: array 'a, l u: int.
        permut_sub a1 a2 l u -> permut_sub a2 a3 l u ->
        permut_sub a1 a3 l u
    
      let swap (a: array 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 rec quick_sort1 (a: array int) lo hi =
        requires { 0 <= lo <= length a /\ 0 <= hi <= length a }
        ensures { sorted_sub a lo hi /\ permut_sub (old a) a lo hi}
    'L:
        if lo < hi - 1 then begin
        let i = ref (lo + 1) in
        for j = lo + 1 to hi - 1 do
          invariant { lo < !i <= j }
          invariant {forall k: int. lo+1 <= k < !i ->  a[k] <= a[lo]}
          invariant {forall k': int. !i <= k' < j -> a[lo] <= a[k']}
          invariant {permut_sub (at a 'L) a (lo+1) hi}
          if a[j] < a[lo] then begin
              swap a !i j;
              i := !i + 1
          end
          done;
          assert {permut_sub (at a 'L) a lo hi };
          swap a lo (!i-1);
          assert {permut_sub (at a 'L) a lo hi };
          assert {div_sub a lo (!i-1) hi };
          quick_sort1 a lo (!i - 1);
          assert {permut_sub (at a 'L) a lo hi };
          assert {div_sub a lo (!i-1) hi };
          quick_sort1 a !i hi;
          assert {permut_sub (at a 'L) a lo hi };
          assert {div_sub a lo (!i-1) hi }
        end
    
      let quick_sort (a: array int) =
        ensures { sorted a /\ permut_all (old a) a}
        quick_sort1 a 0 (Array.length a)
    
    end
    

  • Generated by why3doc 0.85