For some procedures, a formal definition in the expression language is supplied. These formal definitions do not handle errors. A correct implementation would need first to verify that arguments meet the requirements indicated by the procedure prototypes and the procedure description.