insertion_sort_naive.mlw 5.33 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 11 12 13 14 `````` use import int.Int use import ref.Ref use import ref.Refint use import array.Array `````` Jean-Christophe Filliatre committed Mar 28, 2014 15 `````` use import array.IntArraySorted `````` MARCHE Claude committed Jan 23, 2013 16 17 `````` use import array.ArrayPermut `````` 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 23 `````` = 'Init: for i = 0 to a.length - 1 do `````` 24 `````` invariant { permut_all (at a 'Init) a } `````` MARCHE Claude committed Jan 23, 2013 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 } `````` MARCHE Claude committed Jan 23, 2013 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 committed Jan 23, 2014 34 `````` variant { !j } `````` MARCHE Claude committed Jan 23, 2013 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 `````` MARCHE Claude committed Jan 23, 2013 46 47 48 ``````end `````` MARCHE Claude committed Feb 07, 2013 49 ``````module InsertionSortNaiveGen `````` MARCHE Claude committed Jan 23, 2013 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 `````` Jean-Christophe Filliatre committed Feb 24, 2014 71 `````` let sort (a:array elt) `````` MARCHE Claude committed Jan 23, 2013 72 `````` ensures { sorted a } `````` 73 `````` ensures { permut_all (old a) a } `````` MARCHE Claude committed Jan 23, 2013 74 75 76 `````` = 'Init: for i = 0 to a.length - 1 do `````` 77 `````` invariant { permut_all (at a 'Init) a } `````` MARCHE Claude committed Jan 23, 2013 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 } `````` MARCHE Claude committed Jan 23, 2013 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 committed Jan 23, 2014 87 `````` variant { !j } `````` MARCHE Claude committed Jan 23, 2013 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 `````` MARCHE Claude committed Jan 29, 2013 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 } `````` MARCHE Claude committed Jan 29, 2013 134 135 136 `````` = 'Init: for i = 0 to a.length - 1 do `````` 137 `````` invariant { permut_all (at a 'Init) a } `````` MARCHE Claude committed Jan 29, 2013 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 } `````` MARCHE Claude committed Jan 29, 2013 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 committed Jan 23, 2014 147 `````` variant { !j } `````` MARCHE Claude committed Jan 29, 2013 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 }; `````` Jean-Christophe Filliatre committed Feb 05, 2014 154 `````` assert { sorted_sub p a.elts (!j-1) (i+1) }; `````` MARCHE Claude committed Jan 29, 2013 155 156 157 158 159 160 161 162 163 `````` decr j done done end module InsertionSortParamBad `````` Jean-Christophe Filliatre committed Feb 24, 2014 164 165 `````` (* this version is hard to prove because predicate sorted_sub applies to an array instead of a map *) `````` MARCHE Claude committed Feb 07, 2013 166 `````` `````` MARCHE Claude committed Jan 29, 2013 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 } `````` MARCHE Claude committed Jan 29, 2013 196 197 198 `````` = 'Init: for i = 0 to a.length - 1 do `````` 199 `````` invariant { permut_all (at a 'Init) 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 } `````` 204 `````` invariant { permut_all (at a 'Init) 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 } `````` MARCHE Claude committed Jan 29, 2013 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``````