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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!mx05.eternal-september.org!feeder.eternal-september.org!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Seeking for papers about tagged types vs access to subprograms Date: Mon, 13 May 2013 21:29:15 -0500 Organization: Jacob Sparre Andersen Research & Innovation 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> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: loke.gir.dk 1368498556 9179 69.95.181.76 (14 May 2013 02:29:16 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Tue, 14 May 2013 02:29:16 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:15547 Date: 2013-05-13T21:29:15-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:hxkln519n179.1kt13z7phxg2f.dlg@40tude.net... > 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. Which is why I'm suggesting something built on top of Ada's types for this purpose. > 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. Again, this is precisely what I'm talking about. SPARK is a disaster because it insists that you do everything it's way, or nothing at all. I want to be able to incrementally add checks as they become apparent. The big disconnect is that you (and lots of other misguided people) think that types have something to do with operations. Types are more fundamental than operations; they get *used* in operations, rather than the operations being part of the type. Ideally, a type is nothing but a black box (an Ada private type). Operations are the next level of complexity, and exist separately from the types. Randy.