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-Received: by 10.112.162.228 with SMTP id yd4mr292635lbb.8.1431544519800;
 Wed, 13 May 2015 12:15:19 -0700 (PDT)
Path: 
 border2.nntp.dca1.giganews.com!nntp.giganews.com!j5no8330216qga.1!news-out.google.com!ul5ni227044lbb.0!nntp.google.com!goblin3!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: {Pre,Post}conditions and side effects
Date: Wed, 13 May 2015 21:15:12 +0200
Organization: cbb software GmbH
Message-ID: <5d5k4n9blbfl.hx4jw5yqa1o4.dlg@40tude.net>
References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com>
 <alpine.CYG.2.11.1412231747100.4196@WIL414CHAPIN.vtc.vsc.edu>
 <wccegrpq2om.fsf@shell01.TheWorld.com>
 <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com>
 <ce4af31e-d491-479f-a5b3-0b3eedea2a68@googlegroups.com>
 <midvq5$2u3$1@loke.gir.dk> <alpine.DEB.2.11.1505071103310.14859@debian>
 <migc9a$jp8$1@loke.gir.dk> <alpine.DEB.2.11.1505072052570.16448@debian>
 <mijen0$1hj$1@loke.gir.dk> <87pp6a1u9w.fsf@jester.gateway.sonic.net>
 <mirhjl$kvm$1@loke.gir.dk> <877fsd1xb5.fsf@jester.gateway.sonic.net>
 <mitt8a$goo$1@loke.gir.dk> <huo4vktkck8l$.15z81uhs8zx2h.dlg@40tude.net>
 <mivdul$bh9$1@dont-email.me> <1d9ioha0kn05$.1durah75rm1yn.dlg@40tude.net>
 <mivlmn$7af$1@dont-email.me> <fzyfvl2v29oi.1u7eycnwiwqzy$.dlg@40tude.net>
 <mivub6$a4o$1@dont-email.me>
Reply-To: mailbox@dmitry-kazakov.de
NNTP-Posting-Host: evoS9sCOdnHjo0GRLLMU1Q.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
Xref: number.nntp.giganews.com comp.lang.ada:193176
Date: 2015-05-13T21:15:12+02:00
List-Id: <comp.lang.ada>

On Wed, 13 May 2015 18:33:45 +0200, G.B. wrote:

> On 13.05.15 16:21, Dmitry A. Kazakov wrote:
>> On Wed, 13 May 2015 16:06:18 +0200, G.B. wrote:
>>
>>> On 13.05.15 14:47, Dmitry A. Kazakov wrote:
>>>> Operations are defined on types.
>>>
>>> Or, operations are of a type and Ada has no way to name
>>> this type directly?
>>
>> All types have names in Ada.
> 
> But what is the type of an operation,

Anonymous. Operations are second-class citizens in Ada.

> so that conditions
> (plural) on them do not create an untyped mess, but are
> adequately representing a well designed contract?
> 
> Conjecture: Types and operations is like hens and eggs.

Which is another way to say the operations cannot have independent on types
contracts.

I remind you earlier discussions on whether Positive is a type and about
merits of LSP. Each time you change anything, you create a *new* type. Thus
when you constraint the set of values in an operation, e.g. by putting a
precondition, you create a *new* type that carries this constraint. If you
keep on pretending this new type same to the original type, you depart
strong typing and go to weak typing or no typing. And you will be dearly
punished for that by debugging countless exceptions popping here and there,
always when you expect them least.

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