op Median(l:IntList)->i:integer
    pre: ;
    post: (* Half of the elements of l are < i and half are >. *)
            (* There are #l/2 elements of l  < i and #l/2 elements of l > i *)
        exists (l':IntList | Sorted(l') and SameElems(l, l')) (
             FirstHalfLessThan(l', i) and
             SecondHalfGreaterThan(l', i)
        );
end Median;

op FirstHalfLessThan(l:IntList, i:integer)->boolean =
    forall (j in [1 .. #l/2])
	i >= l.body[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;

obj GenericList
    components: body:GenericElem*;
    operations:
        Sorted(GenericList)->boolean;
	SameElems(GenericList,GenericList)->boolean;
end GenericList;

obj GenericElem;

op Sorted(GenericList)->boolean;
op SameElems(GenericList,GenericList)->boolean;

obj IntElem < GenericElem;
obj IntList < GenericList = IntElem*;