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 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Thu, 14 May 2015 09:10:50 +0200 Organization: cbb software GmbH Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> <87pp6a1u9w.fsf@jester.gateway.sonic.net> <877fsd1xb5.fsf@jester.gateway.sonic.net> <1d9ioha0kn05$.1durah75rm1yn.dlg@40tude.net> <5d5k4n9blbfl.hx4jw5yqa1o4.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: evoS9sCOdnHjo0GRLLMU1Q.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:25875 Date: 2015-05-14T09:10:50+02:00 List-Id: On Wed, 13 May 2015 20:36:41 -0500, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:5d5k4n9blbfl.hx4jw5yqa1o4.dlg@40tude.net... > ... >> 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. > > Ergo, Dmitry has a truly bizarre world-view. Not much to be learned from > that, sadly. > > Positive is not a type, and never will be a type (from an Ada world-view, > which is all we're talking about here). Makes no sense whatsoever. And it > doesn't help anyone to ignore reality. How do you know if it does? You consider useless any formal definitions and conclusions deduced from (AKA theorems). Thus the only sense anything could make (to you) would be observed practical effects. Not predicted ones, since that would again be those damned theorems... Anyway, consequences are plenty, see accessibility checks. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de