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.189.72 with SMTP id gg8mr6535644pbc.4.1328336822636; Fri, 03 Feb 2012 22:27:02 -0800 (PST) Path: lh20ni258539pbb.0!nntp.google.com!news2.google.com!goblin3!goblin2!goblin.stu.neva.ru!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: Sat, 04 Feb 2012 07:27:00 +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: zaLIqR6OtyZgOpmrUj6pWA.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-04T07:27:00+01:00 List-Id: Le Sat, 04 Feb 2012 04:16:34 +0100, Randy Brukardt = a =C3=A9crit: > But to claim that just because it's practically impossible to describe= = > the complete behavior of real systems does not mean that there is no = > benefit to describing the easy part. And that is exactly what you are = = > arguing -- and it should be clear to any Ada programmer that that is a= = > fallicy. At least an Ada practice was always there, even far prior it integrated = = DbC=E2=84=A2: express as much validity constraints as you can with the t= ype system. The type system cannot express every constraint (and that's clear to = everyone), but it still useful. The same with DbC. Moreover, with DbC, y= ou = may indeed have to care about efficiency. Anyway, if one want very stric= t = proof and cases coverage, there are other tools or languages: SPARK & Ci= e. = There is no way to impose such things to every application and every Ada= = source author. On the opposite, this would even prevent authors from = keeping Ada in mind as an option. 98% is not 100%, but better what you can really and practically get than= = any promise you will not ever access to, and which will turn a something= = far below 98% or to simply nothing. Time to recall safety and proof level is not to be the same for every Ad= a = applications, and to recall this level is to be defined by the = application's specifications. No need to design an application outside o= f = its specifications (except as a game, challenge or other experiments). -- = =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