object Union =  a:A or b:B or c:C;
object A;
object B;
object C;

operation u1(u:Union, a:A, b:B, c:C)->(u':Union, a':A, b':B, c':C)
    pre: u.a = a;
    post: u' = {a};	(* ERROR: { ... } is not a union constructor in new
			   semantics.  24mar04: This comment, from 7jun00, is
		           not longer true.  There s a 24mar04 LOG message
			   about it. *)
end u1;

operation u2
    components: ;
    inputs: x:Union, y:Union;
    outputs: z: Union;
    description: (*
	x
    *);
end u2;