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,ASCII-7-bit X-Received: by 10.224.10.6 with SMTP id n6mr22375828qan.4.1368583776834; Tue, 14 May 2013 19:09:36 -0700 (PDT) Path: y6ni44345qax.0!nntp.google.com!border1.nntp.dca.giganews.com!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" Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Sat, 11 May 2013 09:42:14 +0200 Organization: cbb software GmbH Message-ID: References: <17ceq51ydy3s0.s94miqqzbg5w.dlg@40tude.net> <1vrhb7oc4qbob$.q02vuouyovp5$.dlg@40tude.net> <19lrzzbgm77v6.1dzpgqckptaj6.dlg@40tude.net> <1bfhq7jo34xpi.p8n2vq6yjsea.dlg@40tude.net> <12gn9wvv1gwfk.10ikfju4rzmnj.dlg@40tude.net> <1oy5rmprgawqs.1jz36okze0xju$.dlg@40tude.net> <1q2ql1e4rcgko.diszzq1mhaq8$.dlg@40tude.net> <518dedd4$0$6581$9b4e6d93@newsspool3.arcor-online.net> 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="us-ascii" Content-Transfer-Encoding: 7bit Date: 2013-05-11T09:42:14+02:00 List-Id: On Sat, 11 May 2013 09:06:11 +0200, Georg Bauhaus wrote: > On 11.05.13 08:37, Dmitry A. Kazakov wrote: >> 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. Meaning: a declared >> operation can be called anywhere. The client may annotate his calls to the >> operation with additional preconditions related to the logic of the program >> that uses the operation. These are not the property of the operation and >> unrelated to the type. >> >> The idea that the precondition of first kind should depend on the state of >> the objects involved in the operation is a very, VERY bad idea. > > How do you specify the preconditions of the second kind (on individual > calls) in such a way that a programmer, wishing to calling these operations, > ensures the calls won't fail as a consequence of violating these > preconditions? "Fail" is a wrong word here. The right wording is ensuring postconditions. That is completely unrelated issue, IMO. I have a feeling that people confuse typing with this, which is basically program correctness en large. You cannot ensure program correctness through types. And since full correctness proof is unachievable anyway I want to separate it from types. Second kind checks (e.g. SPARK) should be optional so that the programmer would add or remove checks depending on requirements and provability. Especially because there is also a big difference in the design of type checks and correctness checks. We design types top-down, at least the most important ones. Type design is frequently irreversible, few things can be changed later without big troubles. It is almost waterfall. On the contrary, the correctness checks are bottom-up. You probably never get to the top. But you can well figure up essential things at the bottom for which it were possible and desirable to check things statically. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de