Re: {Pre,Post}conditions and side effects

[Brad Moore <brad.moore@shaw.ca>]

On 14-12-22 09:22 AM, Jean François Martinez wrote:
> First time I read about Pre-Post conditions in Ada 2012 I felt some disconfort about functions invoked in pre/post conditions being allowed to have side effects.  Tus it is possible to have programs that work when checks are enabled and break when they are disabled that because the side effets "make them work".   I don't like "solutions" like "the compiler will allow you to soot yourself in the foot so be careful".  That is C not Ada
>
> Perhaps it would have been a good idea to have a No_Side_Effects aspect and only functions labelled with this pragma would be allowed in pre/post conditions.  Such functions would not be able to modify global variables and would be restricted to invoking only functions/procedures marked with this aspect.   This is somewhat akin with the restrictions for packages marked with elaboration pragmas or with pragmas realated to distributed system annex. In both a package may only with a "lower or equal" package.

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

>
> First problem I see is that I/O functions have side effect so when debugging No_Side_Effects_functions it would impossible to use the good-old method of inseting Puts in  the code.

Agreed. I suppose you could comment out the Globals => null during 
debugging, and uncomment it once the debugging had been removed.

>
> SEcond and biggest problem is that it is too late.

Too late for Ada 2012, but not for Ada 202X. Or you could consider using 
SPARK 2014 for this code, as it already has this Global aspect. Or you 
might ask your compiler vender to provide an implementation specific 
solution.

Brad


>
> Jean François Martinez
>