From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,7ae8393ad9100e97
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
Received: by 10.68.190.71 with SMTP id go7mr7068314pbc.8.1324337687286;
        Mon, 19 Dec 2011 15:34:47 -0800 (PST)
MIME-Version: 1.0
Path: 
 lh20ni42081pbb.0!nntp.google.com!news2.google.com!goblin2!goblin1!goblin.stu.neva.ru!news.tornevall.net!news.jacob-sparre.dk!pnx.dk!jacob-sparre.dk!ada-dk.org!.POSTED!not-for-mail
From: "Randy Brukardt" <randy@rrsoftware.com>
Newsgroups: comp.lang.ada
Subject: Re: Ada2012 : When to use expression functions rather than function
 bodies?
Date: Mon, 19 Dec 2011 17:34:42 -0600
Organization: Jacob Sparre Andersen Research & Innovation
Message-ID: <jcohmk$lc2$1@munin.nbi.dk>
References: <12acbf57-01fc-43dd-8881-d39c2a63146b@q9g2000yqe.googlegroups.com>
 <jcgqrb$cdv$1@munin.nbi.dk>
 <1697334721345818104.523316rmhost.bauhaus-maps.arcor.de@news.arcor.de>
 <1xbajufyxdf4j.1moa6g6ouhykk$.dlg@40tude.net>
NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net
X-Trace: munin.nbi.dk 1324337685 21890 69.95.181.76 (19 Dec 2011 23:34:45 GMT)
X-Complaints-To: news@jacob-sparre.dk
NNTP-Posting-Date: Mon, 19 Dec 2011 23:34:45 +0000 (UTC)
X-Priority: 3
X-MSMail-Priority: Normal
X-Newsreader: Microsoft Outlook Express 6.00.2900.5931
X-RFC2646: Format=Flowed; Original
X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157
Date: 2011-12-19T17:34:42-06:00
List-Id: <comp.lang.ada>

"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.