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.189.72 with SMTP id gg8mr17246654pbc.4.1328114152408; Wed, 01 Feb 2012 08:35:52 -0800 (PST) Path: lh20ni249044pbb.0!nntp.google.com!news1.google.com!goblin1!goblin.stu.neva.ru!newsfeed.straub-nv.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!not-for-mail From: stefan-lucks@see-the.signature Newsgroups: comp.lang.ada Subject: Re: Silly and stupid =?UTF-8?B?cG9zdOKAkWNvbmRpdGlvbiBvciBub3TCoA==?= =?UTF-8?B?Pw==?= Date: Wed, 1 Feb 2012 17:37:28 +0100 Organization: Bauhaus-Universitaet Weimar 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: stefan-lucks@see-the.signature NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 X-Trace: tigger.scc.uni-weimar.de 1328114151 4433 141.54.178.228 (1 Feb 2012 16:35:51 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Wed, 1 Feb 2012 16:35:51 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: Content-Type: TEXT/PLAIN; charset=US-ASCII Date: 2012-02-01T17:37:28+01:00 List-Id: 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. I.e., value of Y is predictable. If X is odd, one needs the postcondition to predict Y. If X is even, then Y is 0, regardless of the value of F(X). But note that I follow the SPARK-inspired assumption that for even X, F(X) can be any value of the given type, but computing F(X) must not propagate an exception! I didn't actually try it, but I am sure that I could verify the correctness of a SPARK program with such a structure. Of course, SPARK would still force me to actually prove that F doesn't raise an exception, even for the case of X being even. Furthermore, the good thing about SPARK is that it would have thrown a bunch of unprovable verification conditions at me, had I tried to verify the example with the typo. Unfortunately, Ada 2012 lacks a way to specify a subprogram not to propagate an exception (*). Waiting for Ada 2020! > > 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. E.g., specifying (or even better, proving) 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); for some applications would be a big deal, even though there are four different cases for the postcondition (any combination of the Booleans Authorized(U) and Asks_For_Secret_Stuff(Q), and only one of these four cases is formally specified. ---- (*) Of course, by the language's own means, without gnatmem or some other tool, one can actually be never really sure about Storage_Error ... -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- ------ I love the taste of Cryptanalysis in the morning! ------