obj IntList =  integer*;

op Median(l:IntList)->i:integer
    pre: ;
    post:
	(*
	 * For a sorted list, say l', with the same elements as l, the median
	 * is the middle element (odd length list) or average of the two middle
	 * elements (even length list).
	 *) 
        exists (l':IntList | Sorted(l') and SameElems(l, l')) (
	    if Odd(#l) then
		i = l'[#l'/2 + 1]
	    else
		i = (l'[#l'/2] + l'[#l'/2 + 1])/2
        );
end Median;

op Sorted(l:IntList)->boolean =  -- Same as specified elsewhere.
    forall (i,j:integer | (i in [1..#l]) and (j in [1..#l]) and (i < j))
	l[i] <= l[j];

op SameElems(l1:IntList, l2:IntList)->boolean = (
    ((l1 =  nil) and (l2 = nil)) or
    (l1[1] in l2) and
	SameElems(l1[2:#l1], l2 - l1[1])

    (* Note that the following will work for set, but not bag:
     *
     *    forall (i:integer) (i in l1) iff (i in l2)
     *)
);

op Odd(i:integer)->boolean = i mod 2 = 1;