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: a07f3367d7,39579ad87542da0e
X-Google-Attributes: gida07f3367d7,public,usenet
X-Google-NewGroupId: yes
X-Google-Language: ENGLISH,UTF8
X-Received: by 10.180.38.5 with SMTP id c5mr1646562wik.3.1368583788229;
        Tue, 14 May 2013 19:09:48 -0700 (PDT)
Path: 
 hg5ni110158wib.1!nntp.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!194.109.133.86.MISMATCH!newsfeed.xs4all.nl!newsfeed3.news.xs4all.nl!xs4all!newspeer1.nac.net!border4.nntp.dca.giganews.com!border2.nntp.dca.giganews.com!nntp.giganews.com!newsfeed.news.ucla.edu!nrc-news.nrc.ca!News.Dal.Ca!news.litech.org!news.stack.nl!aioe.org!.POSTED!not-for-mail
From: "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>
Newsgroups: comp.lang.ada
Subject: Re: Seeking for papers about tagged types vs access to subprograms
Date: Sat, 11 May 2013 11:16:07 +0200
Organization: cbb software GmbH
Message-ID: <1msoad3apbkf.1optea1ujjydv.dlg@40tude.net>
References: <op.wv8jh1c1ule2fv@cardamome>
 <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <op.wwny5jerule2fv@cardamome>
 <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <op.wwn4oak8ule2fv@cardamome>
 <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <kmbohm$elb$1@loke.gir.dk>
 <p0pf97g5w6xg.jhca6ztjwpde$.dlg@40tude.net> <op.wwq9s4l6ule2fv@cardamome>
 <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <op.wwrefx1pule2fv@cardamome>
 <cps71yzogw24$.7ol98fxcaurj$.dlg@40tude.net> <op.wwriky0dule2fv@cardamome>
 <nd22gfeezrwf$.tlj4yyygrwq3$.dlg@40tude.net> <kmecg6$et4$1@loke.gir.dk>
 <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> <kmh7d4$up3$1@loke.gir.dk>
 <1oy5rmprgawqs.1jz36okze0xju$.dlg@40tude.net> <kmk45u$v45$1@loke.gir.dk>
 <1q2ql1e4rcgko.diszzq1mhaq8$.dlg@40tude.net> <op.wwwtznpsule2fv@cardamome>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: 15waz9CoS+eMakbyhTPyFQ.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="utf-8"
Content-Transfer-Encoding: 8bit
Date: 2013-05-11T11:16:07+02:00
List-Id: <comp.lang.ada>

On Sat, 11 May 2013 10:03:13 +0200, Yannick Duchêne (Hibou57) wrote:

> Le Sat, 11 May 2013 08:37:15 +0200, Dmitry A. Kazakov  
> <mailbox@dmitry-kazakov.de> a écrit:
>> First of all, there are preconditions of operations and the precondition
>> put on individual calls. I don't know which one you mean here. But the
>> preconditions of operations must be statically true.
> 
> That's the point I don't understand or can't visualize: “preconditions of  
> operations must be statically true”. Out of any context?

Yep. The reason for that is that the designed of an operation cannot
control or even foresee the contexts where the operation will be used. It
is neither his responsibility nor his concern.

> Or else, do you  
> suggest to move all the constraints on the types used by the operations?

I suggest that properly designed types should have no constraints of this
kind.
  
> (if so, that's just delegating or moving the condition elsewhere, isn't  
> it?).

The condition is moved to the post-condition. E.g.

# require X >= 0.0
   function sqrt (X : Float) return Float;
# ensure sqrt (X)**2 = X

is replaced with

# require true
   function sqrt (X : Float) return Float;
# ensure sqrt (X)**2 = X or else Constraint_Error raised

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