(* "naive" version of insertion sort: makes too many swap 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