(* "naive" version of insertion sort: makes too many swap see insertion_sort.mlw for a better version *) module InsertionSortNaive use import int.Int use import ref.Ref use import ref.Refint use import array.Array use import array.IntArraySorted use import array.ArrayPermut let sort (a:array int) ensures { sorted a } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut_all (at a 'Init) 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 (at a 'Init) 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 } '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 module InsertionSortNaiveGen 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 let sort (a:array elt) ensures { sorted a } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut_all (at a 'Init) 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 (at a 'Init) 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 } '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 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 } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut_all (at a 'Init) 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 (at a 'Init) 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 } '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 }; 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 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 } ensures { permut_all (old a) a } = 'Init: for i = 0 to a.length - 1 do invariant { permut_all (at a 'Init) 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 (at a 'Init) 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 } '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