why3/examples/insertion_sort_naive.mlw

(*

  "naive" version of insertion sort: makes too many assignments

  see insertion_sort.mlw for a better version

*)

module InsertionSortNaive

  use int.Int
  use ref.Ref
  use ref.Refint
  use array.Array
  use array.IntArraySorted
  use array.ArrayPermut

  let sort (a:array int)
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
   for i = 0 to a.length - 1 do
     invariant { permut_all (old a) a   }
     invariant { sorted_sub a 0 i  }
     let j = ref i in
     while !j > 0 && a[!j-1] > a[!j]  do
       invariant { 0 <= !j <= i }
       invariant { permut_all (old a) a   }
       invariant { sorted_sub a 0 !j }
       invariant { sorted_sub a !j (i+1) }
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                      a[k1] <= a[k2] }
       variant { !j }
       label L in
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (a at L) a (!j-1) !j };
       decr j
     done
   done


end


module InsertionSortNaiveGen

  use int.Int
  use ref.Ref
  use ref.Refint
  use array.Array
  use array.ArrayPermut

  type elt

  val predicate le elt elt

  clone map.MapSorted as M with type elt = elt, predicate le = le

  axiom le_refl: forall x:elt. le x x

  axiom le_asym: forall x y:elt. not (le x y) -> le y x

  axiom le_trans: forall x y z:elt. le x y /\ le y z -> le x z

  predicate sorted_sub (a : array elt) (l u : int) =
    M.sorted_sub a.elts l u

  predicate sorted (a : array elt) =
    M.sorted_sub a.elts 0 a.length

  let sort (a:array elt)
    ensures { sorted a }
    ensures { permut_all (old a) a }
  =
   for i = 0 to a.length - 1 do
     invariant { permut_all (old a) a   }
     invariant { sorted_sub a 0 i  }
     let j = ref i in
     while !j > 0 && not (le a[!j-1] a[!j])  do
       invariant { 0 <= !j <= i }
       invariant { permut_all (old a) a   }
       invariant { sorted_sub a 0 !j }
       invariant { sorted_sub a !j (i+1) }
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                      le a[k1] a[k2] }
       variant { !j }
       label L in
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (a at L) a (!j-1) !j };
       decr j
     done
   done


end



module InsertionSortParam

  use int.Int
  use ref.Ref
  use ref.Refint
  use map.Map
  use array.Array
  use array.ArrayPermut

  type param

  type elt

  val predicate le param elt elt

  axiom le_refl: forall p:param, x:elt. le p x x

  axiom le_asym: forall p:param, x y:elt. not (le p x y) -> le p y x

  axiom le_trans: forall p:param, x y z:elt. le p x y /\ le p y z -> le p x z

  (* a[l..u) is sorted for le *)
  predicate sorted_sub (p:param) (a : Map.map int elt) (l u : int) =
    forall i1 i2 : int. l <= i1 <= i2 < u -> le p (Map.get a i1) (Map.get a i2)

  predicate sorted (p:param) (a : array elt) =
    sorted_sub p a.elts 0 a.length

  let sort (p:param) (a:array elt)
    ensures { sorted p a }
    ensures { permut_all (old a) a }
  =
   for i = 0 to a.length - 1 do
     invariant { permut_all (old a) a   }
     invariant { sorted_sub p a.elts 0 i  }
     let j = ref i in
     while !j > 0 && not (le p a[!j-1] a[!j])  do
       invariant { 0 <= !j <= i }
       invariant { permut_all (old a) a   }
       invariant { sorted_sub p a.elts 0 !j }
       invariant { sorted_sub p a.elts !j (i+1) }
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                      le p a[k1] a[k2] }
       variant { !j }
       label L in
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (a at L) a (!j-1) !j };
       assert { sorted_sub p a.elts (!j-1) (i+1) };
       decr j
     done
   done


end

module InsertionSortParamBad

   (* this version is hard to prove because predicate sorted_sub
      applies to an array instead of a map *)

  use int.Int
  use ref.Ref
  use ref.Refint
  use map.Map
  use array.Array
  use array.ArrayPermut

  type param

  type elt

  val predicate le param elt elt

  axiom le_refl: forall p:param, x:elt. le p x x

  axiom le_asym: forall p:param, x y:elt. not (le p x y) -> le p y x

  axiom le_trans: forall p:param, x y z:elt. le p x y /\ le p y z -> le p x z

  (* a[l..u) is sorted for le *)
  predicate sorted_sub (p:param) (a : array elt) (l u : int) =
    forall i1 i2 : int. l <= i1 <= i2 < u -> le p a[i1] a[i2]

  predicate sorted (p:param) (a : array elt) =
    sorted_sub p a 0 a.length

  let sort (p:param) (a:array elt)
    ensures { sorted p a }
    ensures { permut_all (old a) a }
  =
   for i = 0 to a.length - 1 do
     invariant { permut_all (old a) a   }
     invariant { sorted_sub p a 0 i  }
     let j = ref i in
     while !j > 0 && not (le p a[!j-1] a[!j])  do
       invariant { 0 <= !j <= i }
       invariant { permut_all (old a) a   }
       invariant { sorted_sub p a 0 !j }
       invariant { sorted_sub p a !j (i+1) }
       invariant { forall k1 k2:int. 0 <= k1 < !j /\ !j+1 <= k2 <= i ->
                      le p a[k1] a[k2] }
       variant { !j }
       label L in
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (a at L) a (!j-1) !j };
       decr j
     done
   done


end