The formal specification of oberon