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: 103376,ad06d2d7cb045687 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,UTF8 Received: by 10.68.74.201 with SMTP id w9mr13963448pbv.0.1328018018041; Tue, 31 Jan 2012 05:53:38 -0800 (PST) Path: lh20ni244983pbb.0!nntp.google.com!news1.google.com!goblin1!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid =?UTF-8?B?cG9zdOKAkWNvbmRpdGlvbiBvciBub3TCoA==?= =?UTF-8?B?Pw==?= Date: Tue, 31 Jan 2012 14:52:59 +0100 Organization: cbb software GmbH Message-ID: <12pod8zxdo56v.16pnewlc853au$.dlg@40tude.net> References: <12kegkefstjiy.115bw2vmx23ll.dlg@40tude.net> <4f27b5e8$0$6628$9b4e6d93@newsspool2.arcor-online.net> <19jyp0vyqkcop$.6oatj9p6pcp1$.dlg@40tude.net> <4f27dfa5$0$6570$9b4e6d93@newsspool4.arcor-online.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.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: 2012-01-31T14:52:59+01:00 List-Id: On Tue, 31 Jan 2012 13:33:41 +0100, Georg Bauhaus wrote: > On 31.01.12 11:22, Dmitry A. Kazakov wrote: >> On Tue, 31 Jan 2012 10:35:35 +0100, Georg Bauhaus wrote: >> >>> On 31.01.12 09:54, Dmitry A. Kazakov wrote: >>>> On Tue, 31 Jan 2012 00:11:43 +0100, Yannick Duchêne (Hibou57) wrote: >>>> >>>>> function Parsed (S : String) return Parsed_Type >>>>> with Post => >>>>> (if S'Length not in Image_Length_Type then >>>>> Parsed'Result.Status = Format_Error); >>>>> -- There may be other failure conditions. >>>>> >>>>> >>>>> Is such a post‑condition a good or bad practice in your humble or >>>>> authoritative opinion ? >>>> >>>> I would say it would be a bad practice. The reason is that IMO the >>>> postcondition must be complete, it must tell all truth or nothing. Your >>>> prostcondition is a partial truth, it does not describe all cases when >>>> Status is mandated to be Format_Error. >>> >>> One way to express a "hints only" postcondition is >>> >>> with Post => True or -- yes, mathniks, just FTR: >>> (if ... then ... >>> >>> The idea is that the partial truth, in the shape of a >>> formal note, can later lead to an improved program >>> structure. >> >> Apply your idea to the case statement: >> >> case Char is >> when 'A' => Put_Line ("Got A"); >> end case; > > I was only picking up the idea that a case statement's completeness > is decidable and postconditions aren't. The case statement was designed with a mindset opposite to this idea. This is why the alternatives of a case are required to be static, why the choice cannot be a class-wide object. > Nor need they be. So are the alternatives of case. In other languages alternatives are tested in the order of their appearance, no big deal, they say. > Yet, incomplete > information ("lies") can add value to the "about" part of the > annotated thing. Incomplete information /= exhaustiveness. Considering paraconsistent, fuzzy, probabilistic and other logics used to handle unknown things, they long for all alternatives to be specified even more than the conventional logic does. In order to infer anything useful in such a logic, you need to know something about both A and not A, since A or not A is no more true (the law of excluded middle fails). Using the example of the case statement, all incomplete information is concentrated in the value of the choice. There is nothing incomplete in the case's alternatives. Take another example, let you see: x := 1; The information about x is incomplete. You know that it could probably accommodate the value 1, and that is. You may argue at nausea that this "adds value", but that is not Ada, which requires the type of x manifested before its use. And what does a type declaration? It lists all possible values of x, exhaustively. Again, there are languages that take a different path, so my comment is Ada's POV, of course. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de