insertion_sort_naive.mlw 5.21 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 15 16
  use int.Int
  use ref.Ref
  use ref.Refint
  use array.Array
  use array.IntArraySorted
  use array.ArrayPermut
17

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


45 46 47
end


48
module InsertionSortNaiveGen
49

50 51 52 53 54
  use int.Int
  use ref.Ref
  use ref.Refint
  use array.Array
  use array.ArrayPermut
55

Guillaume Melquiond's avatar
Guillaume Melquiond committed
56 57 58 59
  type elt

  val predicate le elt elt

60
  clone map.MapSorted as M with type elt = elt, predicate le = le
61 62 63 64 65 66 67 68 69 70 71 72 73

  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

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


end
102 103 104 105 106



module InsertionSortParam

107 108 109 110 111 112
  use int.Int
  use ref.Ref
  use ref.Refint
  use map.Map
  use array.Array
  use array.ArrayPermut
113 114 115 116 117

  type param

  type elt

Guillaume Melquiond's avatar
Guillaume Melquiond committed
118
  val predicate le param elt elt
119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134

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


end

module InsertionSortParamBad

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

168 169 170 171 172 173
  use int.Int
  use ref.Ref
  use ref.Refint
  use map.Map
  use array.Array
  use array.ArrayPermut
174 175 176 177 178

  type param

  type elt

Guillaume Melquiond's avatar
Guillaume Melquiond committed
179
  val predicate le param elt elt
180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195

  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 }
196
    ensures { permut_all (old a) a }
197 198
  =
   for i = 0 to a.length - 1 do
199
     invariant { permut_all (old a) 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 (old a) 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
       label L in
211 212 213 214
       let b = !j - 1 in
       let t = a[!j] in
       a[!j] <- a[b];
       a[b] <- t;
215
       assert { exchange (a at L) a (!j-1) !j };
216 217 218 219 220 221
       decr j
     done
   done


end