local
  e : RANDOM_GENERATOR
do
  !!e.reset(123)
	-- An object of type RANDOM_GENERATOR is created,
        -- initialized, attached to e, and then the
	-- creation procedure reset is called on e
end