004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maederlibrary Sorting1
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maederspec TotalOrder =
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder pred __<=__ : Elem * Elem
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder forall x,y,z : Elem
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . x <= x %(reflexive)%
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . x <= z if x <= y /\ y <= z %(transitive)%
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . x = y if x <= y /\ y <= x %(antisymmetric)%
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . x <= y \/ y <= x %(dichotomous)%
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maederspec List[Elem] =
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder free type List[Elem] ::= Nil | Cons(Elem; List[Elem])
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder pred __eps__ : Elem * List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder forall x,y:Elem; l:List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . not x eps Nil
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . x eps Cons(y, l) <=> x=y \/ x eps l
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maederspec Sorting[TotalOrder] =
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder preds is_ordered : List[Elem];
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder permutation : List[Elem] * List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder vars x,y:Elem; l,l1,l2:List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . is_ordered( Nil )
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . is_ordered(Cons(x, Nil))
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . is_ordered(Cons(x, Cons(y, l))) <=> x<=y /\ is_ordered(Cons(y, l))
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . permutation(l1,l2) <=> (forall x:Elem . x eps l1 <=>x eps l2)
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder op sorter : List[Elem]->List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder var l:List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . is_ordered(sorter(l))
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . permutation(l,sorter(l))
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder hide is_ordered, permutation
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maederspec InsertSort[TotalOrder] =
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder ops insert : Elem*List[Elem] -> List[Elem];
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder insert_sort : List[Elem]->List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder vars x,y:Elem; l:List[Elem]
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . insert(x, Nil ) = Cons(x, Nil)
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . insert(x, Cons(y, l)) = Cons(x, insert(y,l))
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder when x<=y else Cons(y, insert(x,l))
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . insert_sort( Nil ) = Nil
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder . insert_sort(Cons(x, l)) = insert(x,insert_sort(l))
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maederview InsertSortCorrectness[TotalOrder] :
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder Sorting[TotalOrder] to InsertSort[TotalOrder] =
004688a1d1c27cacba7b01668a30d6ea9068a034Christian Maeder sorter |-> insert_sort