(*
 * Operation with postcondition specifying sorted output.
 *)
operation Sort(l:integer*)->(l':integer*)
    pre: ;
    post:
        forall (i:integer | (i >= 1) and (i < #l))
	    l'[i] < l'[i+1];
end Sort;

(*
 * This is a testing function to try to see what's going on in the bounded
 * quantifier.  It's a hack, but it shouldn't blow up, which it currently
 * does.
 *)
function f1(upper:integer) = upper;
--    forall (i in [1..upper]) (
--	set l1 = l1 + i;
--        true;
--    );

> f1(4);		-- when commented out, results are different

> "Validation of Sort([3,2,1]) ?-> [1,2,3] should be {true,true}:";
> Sort([3,2,1]) ?-> [1,2,3];