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=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no 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 go7mr590789pbc.8.1324127507203;
        Sat, 17 Dec 2011 05:11:47 -0800 (PST)
Path: 
 lh20ni32946pbb.0!nntp.google.com!news2.google.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Ada2012 : When to use expression functions rather than function
 bodies?
Date: Sat, 17 Dec 2011 14:11:35 +0100
Organization: cbb software GmbH
Message-ID: <1xbajufyxdf4j.1moa6g6ouhykk$.dlg@40tude.net>
References: <12acbf57-01fc-43dd-8881-d39c2a63146b@q9g2000yqe.googlegroups.com>
 <jcgqrb$cdv$1@munin.nbi.dk>
 <1697334721345818104.523316rmhost.bauhaus-maps.arcor.de@news.arcor.de>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: CJUYLE7DVSf5VOMPMPRb0Q.user.speranza.aioe.org
Mime-Version: 1.0
X-Complaints-To: abuse@aioe.org
User-Agent: 40tude_Dialog/2.0.15.1
X-Notice: Filtered by postfilter v. 0.8.2
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Date: 2011-12-17T14:11:35+01:00
List-Id: <comp.lang.ada>

On 17 Dec 2011 12:45:38 GMT, georg bauhaus wrote:

> "Randy Brukardt" <randy@rrsoftware.com> wrote:
>> 
>> You could write all of your preconditions like:
>> 
>>      procedure Do_It (A, B : in out Integer)
>>          with Pre => Do_It_Precondition (A, B);
>> 
>> but no one would have any idea what the precondition is. 
> 
> 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. As an example
consider:

   function "+" (Left, Right : Dimensioned) return Dimensioned;

The precondition here (IFF measurement units have to be checked statically)
is that Left and Right have the same unit.

If the measurement units cannot be checked statically THEN the precondition
is "true" and the contract of "+" includes Unit_Error.

Argument against Do_It_Precondition is same as against a formula:
declarations should include minimum executable code. The language of
declarations (types algebra operations) must be clearly, visibly separated
from the object (executable) language. All cases when executable code slips
into the declarations cause difficulties because of the contexts mismatch,
e.g.

   procedure Foo (Default : Integer := Get);
       -- What is the default here? When the default is read from standard
       -- input?

Pure and static expressions are OK because the context is irrelevant.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de