obj IntList =  integer*;

op Median(l:IntList)->i:integer
    pre: ;
    post:
	(*
	 * Half of the elements of l are < i and half are > i.  More precisely,
	 * for a sorted list, say l', with the same elements as l, the first
	 * half of l' is < i and the second half of l' is > i.
	 *) 
        exists (l':IntList | Sorted(l') and SameElems(l, l')) (
             FirstHalfLessThan(l', i) and
             SecondHalfGreaterThan(l', i)
        );
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 FirstHalfLessThan(l:IntList, i:integer)->boolean =
    forall (j in [1 .. #l/2])
	i >= l[j];
	
op SecondHalfGreaterThan(l:IntList, i:integer)->boolean =
    if Even(i) then
	forall (j in [#l/2 +  1 .. #l])
	    i <= l[j]
    else
	forall (j in [#l/2 +  2 .. #l])
	    i <= l[j];

op Even(i:integer)->boolean = i mod 2 = 0;