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,FREEMAIL_FROM autolearn=ham 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.226.10 with SMTP id ro10mr4930516pbc.6.1328278487848; Fri, 03 Feb 2012 06:14:47 -0800 (PST) Path: lh20ni256024pbb.0!nntp.google.com!news1.google.com!news.glorb.com!aioe.org!.POSTED!not-for-mail From: =?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Fri, 03 Feb 2012 15:14:46 +0100 Organization: Ada @ Home Message-ID: References: <82wr86fzos.fsf@stephe-leake.org> <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com> <82k445fu9n.fsf@stephe-leake.org> <1q29nqwr7e7u4.1qrz4gd6twxim.dlg@40tude.net> NNTP-Posting-Host: ASvLW9FqEpkjx+7K3IhuFA.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: Opera Mail/11.61 (Linux) X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset=utf-8; format=flowed; delsp=yes Content-Transfer-Encoding: Quoted-Printable Date: 2012-02-03T15:14:46+01:00 List-Id: Le Fri, 03 Feb 2012 14:18:40 +0100, Dmitry A. Kazakov = a =C3=A9crit: > Supposed to specify the semantics of the operation in terms of the > parameter and result values. Not in Ada 2012, of course... It do: the postcondition refers to both F'Result and its parameter, and = = relate both. > You are confusing the semantics of the language types with the problem= > domain. In the problem domain Format_Error should tell something about= = > the image object, rather than to disallow anything. Your postcondition= = > is not > to deliver that message. The type definition for Parsed_Type express the problem domain. Returnin= g = an access to value and Null when nothing is available was not an option = = (excluded on purpose), and was preferred the SML way to do and defined a= = discriminated record. The function may returns an instance which was parsed, and will not retu= rn = an instance if the input image is erroneously formated. This is not so = randomly, the result is always the same for each same input. Parsed_Type express what the function result can be: either an instance = or = nothing (kind of Null). Format_Error has nothing to tell except nothing was parsed. If Null was = = not an Ada reserved word, I would have name it simply Null. Its purpose = is = indeed to disallow access to an instance which does not exist. It's ther= e = in place of any instance, because there is no instance. Just like you = cannot access any data referred to by a null access: there is no data; = Null has nothing to tell more, except there is nothing there. The postcondition act as an indirect precondition. This is not a = precondition because, first, you cannot refer to F'Result in a = precondition (would not make sens), second, the function returns in any = = case and never raise an exception. From the returned type definition, you have an implicit postcondition: = you = either get an instance or nothing. As Georg explained better than I = previously did, whatever is the reason for the failure to return a = non=E2=80=91null instance, a result meaning nothing was returned is to b= e dropped = (the program won't fix any erroneous input, it just can drop). What ever= = the program will know about why there was a failure, this would always b= e = the same. A complete postcondition (a complex and long one) could tell = more, but this, first, would be useless as still resulting in always the= = same behavior, second, as useless this would just be bloat. But there is still something the postcondition tells, and that's where i= t = acts as an indirect pseudo=E2=80=91precondition: if image's length is ou= t of = bounds, the program is assured Image will return a kind of Null result = (but will not raise an exception). Knowledge of this property, is useful= = for any program using this function. -- = =E2=80=9CSyntactic sugar causes cancer of the semi-colons.=E2=80=9D [1] =E2=80=9CStructured Programming supports the law of the excluded muddle.= =E2=80=9D [1] [1]: Epigrams on Programming =E2=80=94 Alan J. =E2=80=94 P. Yale Univers= ity