Re: Ada2012 : When to use expression functions rather than function bodies?

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

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:1xbajufyxdf4j.1moa6g6ouhykk$.dlg@40tude.net...
> On 17 Dec 2011 12:45:38 GMT, georg bauhaus wrote:
...
>> I'm guessing that Dmitry will suggest
>>
>>   Procedure Do_It (A, B: Int_Sats_Pre) with
>>     Pre => True;
>>
>> will be safer and will convey the idea
>> of the precondition better: it is in the type system.
>
> Not really. The key question is whether Do_It_Precondition is statically
> checkable. Note also that it is not always possible to break a [true]
> precondition into a set of *independent* subtype constraints.

Right. We had this (sub)discussion in the ARG. It seemed better to extend 
subtype constraints for parameters rather than the heavier mechanism of 
preconditions. But the counter argument is that a constraint can act only on 
a single parameter, while a precondition might involve multiple parameters. 
Dmitry shows a good example.

BTW, we recently added a rule stating that it is a bounded error to call a 
function from a contract (precondition, predicate, etc.) that has a side 
effect that changes the value of some other contract of the same evaluation. 
The latter part is a sop to the people who insist that we have to support 
"benign" side-effects (such as "memo functions"). (IMHO, there are no benign 
side-effects, but there are strong opinions to the contrary out there.)

The effect is that the vast majority of contracts will be "pure" 
expressions, so Dmitry will be happier. (The state-of-the-art will not allow 
static checking of these things today in general, but as the technology 
improves that should become possible without having to rewrite your code).

                                                   Randy.