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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.196.232 with SMTP id ip8mr3971429pbc.6.1340383517887; Fri, 22 Jun 2012 09:45:17 -0700 (PDT) Path: l9ni7485pbj.0!nntp.google.com!news1.google.com!goblin2!goblin1!goblin.stu.neva.ru!newsfeed.straub-nv.de!uucp.gnuu.de!newsfeed.arcor.de!newsspool3.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Fri, 22 Jun 2012 18:45:16 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:13.0) Gecko/20120614 Thunderbird/13.0.1 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <4fe45ce8$0$9508$9b4e6d93@newsspool1.arcor-online.net> <1v3soeviat3z1.f0iwle9giqwk.dlg@40tude.net> <4fe4819d$0$9525$9b4e6d93@newsspool1.arcor-online.net> In-Reply-To: Message-ID: <4fe4a11d$0$9515$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 22 Jun 2012 18:45:17 CEST NNTP-Posting-Host: 55a56bdc.newsspool1.arcor-online.net X-Trace: DXC=^A9:XSU68TOI7\_^6>c20Jic==]BZ:afN4Fo<]lROoRAnkgeX?EC@@@?Z7BlCkWK7Gnc\616M64>JLh>_cHTX3jMi_7nnVHm]QE X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2012-06-22T18:45:17+02:00 List-Id: On 22.06.12 17:05, Dmitry A. Kazakov wrote: > On Fri, 22 Jun 2012 16:30:52 +0200, Georg Bauhaus wrote: > >> On 22.06.12 14:43, Dmitry A. Kazakov wrote: >>> On Fri, 22 Jun 2012 13:54:16 +0200, Georg Bauhaus wrote: >>> >>>> On 22.06.12 09:23, Dmitry A. Kazakov wrote: >>>>> Neither #1 nor #2 is defendable. >>>> >>>> Maybe dynamic checking is not defendable when the attack is >>>> based on some biased, and, frankly, narrow set of assumptions. >>> >>> Sure, the most effective defence is just not to take any position. You >>> might get exposed otherwise. >> >> Who isn't taking a position? > > You. I don't think that #1 xor #2 can be the basis of a meaningful discussion of DbC, because of the frames of reference. The ideal design is when the contract is nothing but documentation, independent of implementation, and checks not affecting the program in ways other than--within specifications--SPACE and TIME. *But*, this state of pre/post is not a property of pre/post per se, it is a property of programmers' style of working. It is not adequate to apply the same reasoning to pre/post aspects and to the non-ignorable part of the program's source. Pre/Post are essentially a tool, not essentially a program; only accidentally. This is why the on/off discussion cannot be decided on the basis of mixing the two (pre/post and the "intended program proper") conceptually. More on accidental accidents below. If the contract "behaves", it does so during the effort at proving a piece of software correct. Ideally. This is why, in the end--provided there is a suitable notion of "end"--assertion checking can be safely turned off, where "safely" means "safe" just as in formal semantics, not physical systems. DbC is a tool. The technical meaning of programs--again in the sense of a "goal"--is to be entirely determined by the program without the assertions, but consistent with the assertions. A goal. The accidental effects of assertions should not matter other than as a programming tool. If they cause accidents, then these accidents are as accidental as all other accident caused by statically undecidable program behavior. The overlap in effects is what makes assertion checking a management issue to be aware of. But it is no major hurdle, since anything that can happen unpredictably, at run time, creates a risk to be assessed based on *business* criteria, not on computer science criteria. > You might also be surprised by Robert Dewar's opinion on and around the > subject, see recent discussion in LinkedIn, group: "Ada Programming > Language", thread: "Imaginary proposal for the next Ada standard: Ada > compilers will automatically generate Package Specification from Package > Body" I don't currently see anything on LinkedIn, takes admission. If the comment is "we will see pre/post being just derived from programs", this has been suggested in Eiffel context before, and is easily answered by referring to the proper discipline: psychology, management, and sociology of the workplace, not DbC. This is an issue of management, and of attitude, not of DbC. > (He was ready to debunk use of exceptions, to dismiss design of Ada I/O. A similar comment on omitting exceptions might be circulated with Parasail, I think. The same Robert Dewar, lecturing at MIT, praises exceptions, comparing them to C's solution (checking return values all along). Could this conviction and readiness to debunk exceptions be a consequence of running a particular business, the small and profitable niche of immensely well funded high tech? > People could do anything in order to save dynamic checks! (:-)) Can you report the gist of the argument?