Denis Koroskin wrote: >> Then I assume you still want to restrict the precondition to being the >> first element in the body? Because putting it in there suggests that it >> may appear anywhere a statement can. > > Why not?
Because a function precondition indicates the set of admissible states before execution of a function. Emphasis on *before* and *function*. -- Michiel Helvensteijn