sort

func sort(ls : List+Set, order : Map) -> List
  pre order = Undefined
    or eval(order [x y]) in Boolean forall x, y in ls*ls
  post #ls = #result and mkset(result) = mkset(ls)
  post order = Undefined and ascending(result)
    or eval(order [result(i) result(i+1)]) forall i in [1..#ls-1]

Returns a list consisting of the same elements as the given list or set, but sorted into the specified order.

The post condition given above is probably stronger than that provided by the actual implementation, while the pre condition is probably too weak. Any suggestions for rewriting the pre and post conditions will be most welcome.

Herman Venter

This is Slim documentation as snarfed on 27 May 1999 by dB.