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.222.71 with SMTP id qk7mr11248691pbc.1.1328092557875; Wed, 01 Feb 2012 02:35:57 -0800 (PST) Path: lh20ni248125pbb.0!nntp.google.com!news1.google.com!news3.google.com!feeder2.cambriumusenet.nl!feed.tweaknews.nl!94.232.116.13.MISMATCH!feed.xsnews.nl!border-3.ams.xsnews.nl!npeer.de.kpn-eurorings.net!npeer-ng0.de.kpn-eurorings.net!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 11:37:31 +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 1328092557 3434 141.54.178.228 (1 Feb 2012 10:35:57 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Wed, 1 Feb 2012 10:35:57 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: <1wn5azarpihb1.13g4tvu7fddve.dlg@40tude.net> Content-Type: TEXT/PLAIN; charset=US-ASCII Date: 2012-02-01T11:37:31+01:00 List-Id: On Wed, 1 Feb 2012, Dmitry A. Kazakov wrote: > But that seems not bad enough. To make the disaster complete, it should > become undefined as well. Right? This doesn't need to be a disaster. 1. For the purpose of proving program correctness, you don't necessarily need complete postconditions. As a trivial example, consider function F(X: Natural) return Natural with Post => (if (X mod 2) = 1 then ...); We don't have any precondition. For even X, we don't even have a postcondition. But using the partial postcondition we have, we can completely define the semantic behavior of Y := F(X) * (F(X) mod 2); If that is all what we need F for, why should we bother with any postcondition or even X? 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. E.g., for a database with confidential and non-confidential data, we be very happy to prove that any response to a query from an unauthorized entity will be derived from non-confidential data only. You have proven your system to be secure! A system may be secure but still be not quite functional. E.g., you may further like to prove that the response to a query from an authorized entity will be derived from all data, the confidential and the non-confidential ones. If you can, fine! Otherwise, apply conventional means ... In fact, some relevant contract requirements may actually be hard to specify. What is the "correct" answer in some informational retrieval setting (e.g., when you google for "Dmitry A. Kazakov")? Do you really propose not to formally specify anything, just because we cannot specify everything? This is pretty much the same in the real world. When you go to a restaurant and order a meal, you expect a tasty meal. But the end, being "tasty" is ... a matter of taste. If you have no other complaints than "it wasn't to my taste", you still have to pay the bill. Thus, being "tasty" is expected by the customer, but not part of the postcondition. On the other hand, certain hygienic standards are defined binding laws for all restaurants (in a given country or state). This is actually a postcondition, inherited from the abstract class of "all restaurants in my country". Would you claim that hygienic standards are useless, because you cannot define tasty Ness? Back to the original poster's question: >> function Parsed (S : String) return Parsed_Type >> with Post => >> (if S'Length not in Image_Length_Type then >> Parsed'Result.Status = Format_Error); >> -- There may be other failure conditions. What is special about that specific failure condition that singles it out from all other failure conditions? -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- ------ I love the taste of Cryptanalysis in the morning! ------