{Pre,Post}conditions and side effects

["Jean François Martinez" <darkquark99@gmail.com>]

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.

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.

SEcond and biggest problem is that it is too late.

Jean François Martinez