insertion_sort_naive.mlw 5.21 KB
 MARCHE Claude committed Jan 23, 2013 1 2 ``````(* `````` MARCHE Claude committed Feb 07, 2013 3 `````` "naive" version of insertion sort: makes too many swap `````` MARCHE Claude committed Jan 23, 2013 4 5 6 7 8 `````` see insertion_sort.mlw for a better version *) `````` MARCHE Claude committed Feb 07, 2013 9 ``````module InsertionSortNaive `````` MARCHE Claude committed Jan 23, 2013 10 `````` `````` Andrei Paskevich committed Jun 15, 2018 11 12 13 14 15 16 `````` use int.Int use ref.Ref use ref.Refint use array.Array use array.IntArraySorted use array.ArrayPermut `````` MARCHE Claude committed Jan 23, 2013 17 `````` `````` Jean-Christophe Filliatre committed Feb 24, 2014 18 `````` let sort (a:array int) `````` MARCHE Claude committed Jan 23, 2013 19 `````` ensures { sorted a } `````` 20 `````` ensures { permut_all (old a) a } `````` MARCHE Claude committed Jan 23, 2013 21 22 `````` = for i = 0 to a.length - 1 do `````` Guillaume Melquiond committed Mar 16, 2016 23 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 23, 2013 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 } `````` Guillaume Melquiond committed Mar 16, 2016 28 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 23, 2013 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 committed Jan 23, 2014 33 `````` variant { !j } `````` Guillaume Melquiond committed Mar 16, 2016 34 `````` label L in `````` MARCHE Claude committed Jan 23, 2013 35 36 37 38 `````` let b = !j - 1 in let t = a[!j] in a[!j] <- a[b]; a[b] <- t; `````` Guillaume Melquiond committed Mar 16, 2016 39 `````` assert { exchange (a at L) a (!j-1) !j }; `````` MARCHE Claude committed Jan 23, 2013 40 41 42 43 44 `````` decr j done done `````` MARCHE Claude committed Jan 23, 2013 45 46 47 ``````end `````` MARCHE Claude committed Feb 07, 2013 48 ``````module InsertionSortNaiveGen `````` MARCHE Claude committed Jan 23, 2013 49 `````` `````` Andrei Paskevich committed Jun 15, 2018 50 51 52 53 54 `````` use int.Int use ref.Ref use ref.Refint use array.Array use array.ArrayPermut `````` MARCHE Claude committed Jan 23, 2013 55 `````` `````` Guillaume Melquiond committed Mar 24, 2016 56 57 58 59 `````` type elt val predicate le elt elt `````` Andrei Paskevich committed Jun 15, 2018 60 `````` clone map.MapSorted as M with type elt = elt, predicate le = le `````` MARCHE Claude committed Jan 23, 2013 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 `````` Jean-Christophe Filliatre committed Feb 24, 2014 74 `````` let sort (a:array elt) `````` MARCHE Claude committed Jan 23, 2013 75 `````` ensures { sorted a } `````` 76 `````` ensures { permut_all (old a) a } `````` MARCHE Claude committed Jan 23, 2013 77 78 `````` = for i = 0 to a.length - 1 do `````` Guillaume Melquiond committed Mar 16, 2016 79 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 23, 2013 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 } `````` Guillaume Melquiond committed Mar 16, 2016 84 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 23, 2013 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 committed Jan 23, 2014 89 `````` variant { !j } `````` Guillaume Melquiond committed Mar 16, 2016 90 `````` label L in `````` MARCHE Claude committed Jan 23, 2013 91 92 93 94 `````` let b = !j - 1 in let t = a[!j] in a[!j] <- a[b]; a[b] <- t; `````` Guillaume Melquiond committed Mar 16, 2016 95 `````` assert { exchange (a at L) a (!j-1) !j }; `````` MARCHE Claude committed Jan 23, 2013 96 97 98 99 100 101 `````` decr j done done end `````` MARCHE Claude committed Jan 29, 2013 102 103 104 105 106 `````` module InsertionSortParam `````` Andrei Paskevich committed Jun 15, 2018 107 108 109 110 111 112 `````` use int.Int use ref.Ref use ref.Refint use map.Map use array.Array use array.ArrayPermut `````` MARCHE Claude committed Jan 29, 2013 113 114 115 116 117 `````` type param type elt `````` Guillaume Melquiond committed Mar 24, 2016 118 `````` val predicate le param elt elt `````` MARCHE Claude committed Jan 29, 2013 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 } `````` MARCHE Claude committed Jan 29, 2013 136 137 `````` = for i = 0 to a.length - 1 do `````` Guillaume Melquiond committed Mar 16, 2016 138 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 29, 2013 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 } `````` Guillaume Melquiond committed Mar 16, 2016 143 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 29, 2013 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 committed Jan 23, 2014 148 `````` variant { !j } `````` Guillaume Melquiond committed Mar 16, 2016 149 `````` label L in `````` MARCHE Claude committed Jan 29, 2013 150 151 152 153 `````` let b = !j - 1 in let t = a[!j] in a[!j] <- a[b]; a[b] <- t; `````` Guillaume Melquiond committed Mar 16, 2016 154 `````` assert { exchange (a at L) a (!j-1) !j }; `````` Jean-Christophe Filliatre committed Feb 05, 2014 155 `````` assert { sorted_sub p a.elts (!j-1) (i+1) }; `````` MARCHE Claude committed Jan 29, 2013 156 157 158 159 160 161 162 163 164 `````` decr j done done end module InsertionSortParamBad `````` Jean-Christophe Filliatre committed Feb 24, 2014 165 166 `````` (* this version is hard to prove because predicate sorted_sub applies to an array instead of a map *) `````` MARCHE Claude committed Feb 07, 2013 167 `````` `````` Andrei Paskevich committed Jun 15, 2018 168 169 170 171 172 173 `````` use int.Int use ref.Ref use ref.Refint use map.Map use array.Array use array.ArrayPermut `````` MARCHE Claude committed Jan 29, 2013 174 175 176 177 178 `````` type param type elt `````` Guillaume Melquiond committed Mar 24, 2016 179 `````` val predicate le param elt elt `````` MARCHE Claude committed Jan 29, 2013 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 } `````` MARCHE Claude committed Jan 29, 2013 197 198 `````` = for i = 0 to a.length - 1 do `````` Guillaume Melquiond committed Mar 16, 2016 199 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 29, 2013 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 } `````` Guillaume Melquiond committed Mar 16, 2016 204 `````` invariant { permut_all (old a) a } `````` MARCHE Claude committed Jan 29, 2013 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 committed Jan 23, 2014 209 `````` variant { !j } `````` Guillaume Melquiond committed Mar 16, 2016 210 `````` label L in `````` MARCHE Claude committed Jan 29, 2013 211 212 213 214 `````` let b = !j - 1 in let t = a[!j] in a[!j] <- a[b]; a[b] <- t; `````` Guillaume Melquiond committed Mar 16, 2016 215 `````` assert { exchange (a at L) a (!j-1) !j }; `````` MARCHE Claude committed Jan 29, 2013 216 217 218 219 220 221 `````` decr j done done end``````