Re: {Pre,Post}conditions and side effects

[Florian Weimer <fw@deneb.enyo.de>]

* Brad Moore:

> There is a proposal to have a Global aspect to be considered for Ada
> 202x, that could be applied to subprograms. Such an aspect would
> indicate if a subprogram body referenced any global variables. It
> would also indicate if a subprogram references no globals.
>
> eg.
>        function Foo (X : Integer) return Integer
>              with Globals => null;
>
> I believe such a subprogram would not have side-effects

It could still call subprograms which modify global variables, or use
its arguments to modify global state.

Even if you solve this (different, quite feasible approaches exist),
(lack of) termination of the evaluation of conditions would still be a
visible side effect, and that's more difficult to tackle.