insertion_sort_naive.mlw 5.33 KB
Newer Older
1 2
(*

3
  "naive" version of insertion sort: makes too many swap
4 5 6 7 8

  see insertion_sort.mlw for a better version

*)

9
module InsertionSortNaive
10 11 12 13 14

  use import int.Int
  use import ref.Ref
  use import ref.Refint
  use import array.Array
15
  use import array.IntArraySorted
16 17
  use import array.ArrayPermut

18
  let sort (a:array int)
19
    ensures { sorted a }
20
    ensures { permut_all (old a) a }
21 22 23
  =
   'Init:
   for i = 0 to a.length - 1 do
24
     invariant { permut_all (at a 'Init) a   }
25 26 27 28
     invariant { sorted_sub a 0 i  }
     let j = ref i in
     while !j > 0 && a[!j-1] > a[!j]  do
       invariant { 0 <= !j <= i }
29
       invariant { permut_all (at a 'Init) a   }
30 31 32 33
       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] }
MARCHE Claude's avatar
MARCHE Claude committed
34
       variant { !j }
35 36 37 38 39 40 41 42 43 44 45
       'L:
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (at a 'L) a (!j-1) !j };
       decr j
     done
   done


46 47 48
end


49
module InsertionSortNaiveGen
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70

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

  clone import map.MapSorted as M

  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

71
  let sort (a:array elt)
72
    ensures { sorted a }
73
    ensures { permut_all (old a) a }
74 75 76
  =
   'Init:
   for i = 0 to a.length - 1 do
77
     invariant { permut_all (at a 'Init) a   }
78 79 80 81
     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 }
82
       invariant { permut_all (at a 'Init) a   }
83 84 85 86
       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] }
MARCHE Claude's avatar
MARCHE Claude committed
87
       variant { !j }
88 89 90 91 92 93 94 95 96 97 98 99
       'L:
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (at a 'L) a (!j-1) !j };
       decr j
     done
   done


end
100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132



module InsertionSortParam

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

  type param

  type elt

  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 }
133
    ensures { permut_all (old a) a }
134 135 136
  =
   'Init:
   for i = 0 to a.length - 1 do
137
     invariant { permut_all (at a 'Init) a   }
138 139 140 141
     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 }
142
       invariant { permut_all (at a 'Init) a   }
143 144 145 146
       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] }
MARCHE Claude's avatar
MARCHE Claude committed
147
       variant { !j }
148 149 150 151 152 153
       'L:
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (at a 'L) a (!j-1) !j };
154
       assert { sorted_sub p a.elts (!j-1) (i+1) };
155 156 157 158 159 160 161 162 163
       decr j
     done
   done


end

module InsertionSortParamBad

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

167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194
  use import int.Int
  use import ref.Ref
  use import ref.Refint
  use map.Map
  use import array.Array
  use import array.ArrayPermut

  type param

  type elt

  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 }
195
    ensures { permut_all (old a) a }
196 197 198
  =
   'Init:
   for i = 0 to a.length - 1 do
199
     invariant { permut_all (at a 'Init) a   }
200 201 202 203
     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 }
204
       invariant { permut_all (at a 'Init) a   }
205 206 207 208
       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] }
MARCHE Claude's avatar
MARCHE Claude committed
209
       variant { !j }
210 211 212 213 214 215 216 217 218 219 220 221
       'L:
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
       assert { exchange (at a 'L) a (!j-1) !j };
       decr j
     done
   done


end