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,7fb91ab516cbb7dd,start X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII Received: by 10.68.235.4 with SMTP id ui4mr2148198pbc.3.1331820452859; Thu, 15 Mar 2012 07:07:32 -0700 (PDT) Path: h9ni29145pbe.0!nntp.google.com!news2.google.com!volia.net!news2.volia.net!feed-A.news.volia.net!news.musoftware.de!wum.musoftware.de!feeder.erje.net!news.internetdienste.de!news.tu-darmstadt.de!news.belwue.de!newsfeed.arcor.de!newsspool2.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Thu, 15 Mar 2012 15:07:30 +0100 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: A split between two kinds of Ada programmers? Message-ID: <4f61f7a3$0$6562$9b4e6d93@newsspool4.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 15 Mar 2012 15:07:31 CET NNTP-Posting-Host: 7f4c7388.newsspool4.arcor-online.net X-Trace: DXC=MgI\WmS6[Vi^Y=RbYBPl4`4IUK_dcnc\616M64>jLh>_cHTX3jmgPX_?41jhjo X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit Date: 2012-03-15T15:07:31+01:00 List-Id: THURSDAY MARCH 8, 2012 [GNAT] Improve warnings from -gnatw.t � "When a postcondition is explicitly True or False, it is reasonable to assume that this is exactly what is intended, and it is now the case that warnings for such postconditions are suppressed." (From GNAT Development Log) The message, IMHO, suggests that there are programmers dearly wishing to express, in (pre and) post conditions, what they know about their types. For example, when they know a subprogram needs no special preconditions, that it will compute a state such that Post => ... , no matter what, they say Pre => True. And Post => True as well, because they may have reason to not say more about objects from the subprogram's profile, or about objects in some outer scope. The subprogram may just not affect any of these objects, and, therefore, writing Post => True is reasonable. (If somewhat void, and implicit, in the light of the explicitly listed reasons?) Call them, in pompous terms mabye, the "open", "honest" programmers. Other programmers might consider checked conditions not only a debugging aid(*), but also a tool that allows superiors to oversee the programmers. Why? Because a failed post condition is evidence of an mistake. "This programmer's mistake because he wrote the subprogram!" Whatever the technical truth is, the statement's is superior. How will the programmers react? Will they not resort to always writing Post => True, say, knowing that doing so will make their subprograms look better when assertion policy is Check? Call them the "secretive", "self-protective" programmers. The question then becomes: Can a project use -gnatw.t when integrating source text written by both kinds of programmers? Some data points: I have seen exceptions "explicitly" suppressed by programmers, but sometimes for a reason. They had written empty handlers, no logging. This was partly justified, since, in some cases, the customer would predictably refuse to pay for work that obviously could raise an exception, even in drafted software. So make silent errors a policy. Remembering Eiffel, it seemed somewhat common to just say the equivalent of Post => True when one wanted to defer thinking about what the post condition should really be. __ (*) which, according to J.-P. Rosen's introduction, it very well is, besides functioning as a lemma, and also as part of a contractual obligation.