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.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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.213.68 with SMTP id nq4mr1530945pbc.2.1328171157821; Thu, 02 Feb 2012 00:25:57 -0800 (PST) Path: lh20ni251484pbb.0!nntp.google.com!news1.google.com!goblin2!goblin.stu.neva.ru!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Silly and stupid =?UTF-8?B?cG9zdOKAkWNvbmRpdGlvbiBvciBub3TCoA==?= =?UTF-8?B?Pw==?= Date: Thu, 2 Feb 2012 09:25:00 +0100 Organization: cbb software GmbH Message-ID: References: <12kegkefstjiy.115bw2vmx23ll.dlg@40tude.net> <4f27b5e8$0$6628$9b4e6d93@newsspool2.arcor-online.net> <19jyp0vyqkcop$.6oatj9p6pcp1$.dlg@40tude.net> <4f27dfa5$0$6570$9b4e6d93@newsspool4.arcor-online.net> <12pod8zxdo56v.16pnewlc853au$.dlg@40tude.net> <4f280a00$0$6583$9b4e6d93@newsspool3.arcor-online.net> <4f284488$0$6634$9b4e6d93@newsspool2.arcor-online.net> <1wn5azarpihb1.13g4tvu7fddve.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: FbOMkhMtVLVmu7IwBnt1tw.user.speranza.aioe.org Mime-Version: 1.0 X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit Date: 2012-02-02T09:25:00+01:00 List-Id: On Wed, 1 Feb 2012 17:37:28 +0100, stefan-lucks@see-the.signature wrote: > On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote: > >> On Wed, 1 Feb 2012 11:37:31 +0100, stefan-lucks@see-the.signature wrote: >> >>> 1. For the purpose of proving program correctness, >> >> Proving incorrectness, you mean, since the thing is partial. > > With apologies to you and all the c.l.a readers, there was a really bad > typo in my example. So here is the correct example > > function F(X: Natural) return Natural > with Post => (if (X mod 2) = 1 then ...); > > So any program, which's correctness depends on a statement such as > > Y := F(X) * (X mod 2); -- not "F(X) * (F(X) mod 2)", as I wrote before > > may be proven correct (there is nothing "partial" here), in spite of the > incomplete postcondition for F. You could it have much simpler. Consider programs which do not call F at all. That does the trick too. The idea of pre-/postcondition is that it tells something about a set of programs, of all legal programs actually. If you wanted to narrow that set, then, well, you should at least specify that set. >>> 2. Sometimes, it may hard to prove the entire contract. So we will try to >>> prove the "important" requirements in the contract, and try to convince >>> ourselves by conventional means (testing, code review, ...) that other >>> requirements are also satisfied. >> [...] >> >> No. In that case, and this was my point, the thing must be designed in a >> way which clearly distinguished the provable/specified/defined part from >> the rest. I proposed to introduce Length_Error to indicate a contracted >> error case. > > I see. However, I would claim that an incomplete postcondition actually > "distinguishes the provable/specified/defined part from the rest", as you > put it. It is a cart before the horse. In Ada we believe that specifications come first. Yes, for each given program there exists a specification wich would fit it. Bad design. > procedure Ask_Database(U: User; Q: Query; R: out Response) > with post(if (not Authorized(U)) and (Asks_For_Secret_Stuff(Q)) > then R=Empty_Response); BTW, contracts to be stated in terms of equivalence rather than implications. I.e. R=Empty_Response <=> not Authorized(U)) or ... -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de