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.74.201 with SMTP id w9mr3415190pbv.0.1328423369065; Sat, 04 Feb 2012 22:29:29 -0800 (PST) MIME-Version: 1.0 Path: lh20ni262209pbb.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!news.tornevall.net!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: Sun, 5 Feb 2012 00:29:21 -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> <82ty36urik.fsf@stephe-leake.org> NNTP-Posting-Host: static-69-95-181-76.mad.choiceone.net X-Trace: munin.nbi.dk 1328423366 22305 69.95.181.76 (5 Feb 2012 06:29:26 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Sun, 5 Feb 2012 06:29:26 +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-05T00:29:21-06:00 List-Id: "Stephen Leake" wrote in message news:82ty36urik.fsf@stephe-leake.org... > "Randy Brukardt" writes: ... >> 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. > > The compiler knows the body; why is the post condition better than that? No, the compiler does *not* know the body (in general). Ada separates specifications and bodies after all. The specification can be compiled long before the body is created, and calls written and compiled against that specification. A large part of the problem that I see with proof tools is that they often require peeking into the body to verify calls. This is just plain wrong, because it means that the proof has to be redone if the body changes. And it also means that the body has to exist (and in a near-final form) before the proof can be valuable. An Ada compiler knows even less; when it generates a call it probably knows nothing about the body. (Janus/Ada was designed so that the compiler literally knows nothing about the body, and cannot get access to any information about the body even if it wanted to [other than the one being compiled, of course]. That's why Janus/Ada doesn't do any inlining [at compile time], as that requires breaking that absolute separation of specifications and bodies.) And an Ada compiler cannot presume to know anything about the body when compiling a call (as noted, the body may not have been written yet). The postcondition (and precondition) moves this "contract" information to where it belongs (on the specification). That allows the compiler to take advantage of that information, and in many cases completely eliminate the associated checks (just like the compiler can eliminate a large proportion of constraint checks). Like constraint checks, well-written contracts should never need to be turned off (as always, it's like taking off the seatbelts when you leave the garage...). Randy.