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 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,ASCII-7-bit Received: by 10.68.227.40 with SMTP id rx8mr3703389pbc.5.1328238791332; Thu, 02 Feb 2012 19:13:11 -0800 (PST) MIME-Version: 1.0 Path: lh20ni254350pbb.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!nuzba.szn.dk!news.jacob-sparre.dk!pnx.dk!jacob-sparre.dk!ada-dk.org!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid post-condition or not ? Date: Thu, 2 Feb 2012 21:13:04 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <82wr86fzos.fsf@stephe-leake.org> <5af407fc-2868-44ca-84d2-c51a2a64104d@o4g2000pbc.googlegroups.com> <82k445fu9n.fsf@stephe-leake.org> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1328238788 30859 69.95.181.76 (3 Feb 2012 03:13:08 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 3 Feb 2012 03:13:08 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Date: 2012-02-02T21:13:04-06:00 List-Id: "Stephen Leake" wrote in message news:82k445fu9n.fsf@stephe-leake.org... ... > I agree with Dmitry; post conditions should be _complete_. If the Ada > post condition language is not strong enough to be complete, don't use > it; use natural language comments. That's a pretty silly position, it essentially says that everything that makes Ada great is not worthwhile because it only can detect a portion of the problems. If you really believe this, you might as well be programming in a dynamically typed language, because then there is essentially no benefit to what Ada provides. For instance, if you have an object Dart_Score : Natural range 1 .. 60; -- Holds the score for a single dart. The range 1 .. 60 is not a complete specification of the possible scores. (For instance, 58 is not a possible score, but it is allowed by the range.) But even so, this specification still catches a lot of errors. Your comment above denies this and says that it is better to just have the comment rather than the range (because it is not "complete" in some sense). [Aside: Ada 2012 has a way to make this complete, but of course there are many other things that are too hard to describe.] My philosophy is that it is always preferable to at least be able to tell the compiler what you (the programmer) knows about a program entity. That allows the compiler and other tools to make checks (both compile-time and run-time) about that information -- and my years of experience shows me that those checks catch a lot of bugs (but by no means all). Moreover, as tools and compilers get better, they get able to do more with the information they are given, so you want to give them as much information as you can now -- it's a lot harder to retrofit that information in after the fact. So I want to describe as much as I can in terms of contracts (preconditions, postconditions, predicates, constraints, exclusions, and invariants for Ada 2012, hopefully exception and data contracts in the future), but not to the extent of necessarily requiring completeness. At some point it just gets too hard. I've always hated the emphasis on completeness of these things, because it is *exactly* the wrong approach to getting something in wide-spread use (even in the Ada community). Something like SPARC, that requires an all-or-nothing approach, very often ends up with nothing. OTOH, an approach that just applies the easiest contracts first sets up a positive feedback loop for newcomers to Ada. They'll add a few range constraints and discover that those have detected some bugs early (possibly even at compile time). Which encourages them to add more contracts, which discovers more bugs early, and so on. That's how *I* learned the real benefits of Ada years ago - and I find it hard to believe that I'm unusual. I think that things like SPARC can actually be harmful, as they focus attention on the wrong things. There is a lot that can be proved about dynamic constructs in Ada (far more than in other most languages), and it is unfortunate that instead of taking advantage of this (and making widely usable results), most of effort has been on proving the Fortran 66 subset of Ada. (I do see signs that this is changing, finally, but I think a lot of the work should have been done years ago.) Randy.