Re: {Pre,Post}conditions and side effects

["Randy Brukardt" <randy@rrsoftware.com>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 1947 bytes --]

"Jean François Martinez" <darkquark99@gmail.com> wrote in message 
news:2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.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.

This was proposed with the original proposal. It was eventually dropped 
because it is too hard to define what a side-effect actually is (easy 
definitions are too fierce).

We tried to invent a "Global" aspect for Ada 2012, but it was considered too 
complex and too immature for Ada 2012. We're going to try again (with the 
parallel effort) for the next version of Ada.

Second, we did insert a rule which gives an implementation permission to 
reject assertions with result-changing side-effects. (11.4.2(27/3)). One 
hopes that as compiler technology improves, implementations will take some 
advantage of this to reject uses that clearly cause trouble.

Third, we also introduced expression functions so that the compiler can see 
more (or all) of the parts of an assertion. We hoped that would allow more 
static analysis (including rejection of bad side-effects).

To summarize, we spent a lot of time agonizing about this particular issue, 
wording solutions, and the like. It's most certainly not the case that it 
wasn't considered, but more that we felt that the alternative of strong 
restrictions would be barely usable.

                               Randy Brukardt, ARG Editor.