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,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.241.162 with SMTP id wj2mr8218574pbc.2.1340710618862; Tue, 26 Jun 2012 04:36:58 -0700 (PDT) Path: l9ni21789pbj.0!nntp.google.com!news1.google.com!goblin1!goblin2!goblin.stu.neva.ru!news.internetdienste.de!news.tu-darmstadt.de!news.belwue.de!news.uni-stuttgart.de!news-2.dfn.de!news.dfn.de!news.uni-weimar.de!not-for-mail From: stefan-lucks@see-the.signature Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions Date: Tue, 26 Jun 2012 13:50:28 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> <1oih2rok18dmt.avbwrres5k12.dlg@40tude.net> <4fe59ea0$0$9502$9b4e6d93@newsspool1.arcor-online.net> <1mkp7fzlk1b0y.1ueinfjn48fcy$.dlg@40tude.net> <4fe72b6b$0$9504$9b4e6d93@newsspool1.arcor-online.net> <1bbvp3ghpjb5s.1go1s1qvcmagh$.dlg@40tude.net> <4fe76fad$0$9507$9b4e6d93@newsspool1.arcor-online.net> <1jt8vhzxfrv2i.eohce4d3rwx1$.dlg@40tude.net> <4fe83aaa$0$6624$9b4e6d93@newsspool2.arcor-online.net> <1pkfv0tiod3rn$.onx6dmaa3if9$.dlg@40tude.net> <1i1mp8xs3vtl2.1oc4m66qtfgzq.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 1340710619 11694 141.54.178.228 (26 Jun 2012 11:36:59 GMT) X-Complaints-To: news@tigger.scc.uni-weimar.de NNTP-Posting-Date: Tue, 26 Jun 2012 11:36:59 +0000 (UTC) X-X-Sender: lucks@medsec1.medien.uni-weimar.de In-Reply-To: Content-Type: TEXT/PLAIN; charset=US-ASCII Date: 2012-06-26T13:50:28+02:00 List-Id: On Mon, 25 Jun 2012, Dmitry A. Kazakov wrote: > > Hilbert's program was an attempt to re-build the very foundations of > > Mathematics. No more, no less. See > > . > > Right, and this had nothing to do with justification either logic or > mathematics by means of themselves. Hilbert was very explicit that he wanted to formalize *all* of mathematics axiomatically, and prove the whole formalization consistent. There is an interesting article . > Such an epic task would rather be a job for baron Muenchausen. Here we are in violent agreement. ;-) The program was quite successful in making mathematicans re-think the foundations of their field. BUT it turned out that the required formalization of *all* of mathematics could not work, for the same reason Muenchhausen's famous trick would not work. So Hilbert's program was an epic failure! In any case, this is quite off topic, and we need not discuss Hilbert's program in c.l.a. > Same syntax for things which are far more apart than just semantically > different. What a bizzare idea! You would be switching between contract > specification and implementation per compiler switch! Is this C > preprocessor or Ada? There is a well-defined syntax for contracts, and you can choose between different ways to use them. But contracts are still contracts. No relationship to the C preprocessor. > >> That clearly precludes no.2: handling is within the checker, checker is > >> outside the testee. > > > > Well, this separation is ideal. But most of the time, a testee that > > discovers itself being in a faulty state (and that is, what a failed > > dynamic check actually reveals), the testee is still able to write some > > information to a log file. Sure, you can construct or find the odd > > counterexample -- but in practice almost all the time this approach works. > > (OK, I am assuming your system allows to write some log output at all.) > > Tracing is OK, but what happens afterwards? If continuation is possible, > that requires some cleanup, rollback, retry etc, which has the goal of > putting the system into some definite state. This is not over before over. Don't do that! Emit your messages to to the log file and then terminate! Or try to continue -- but you should never forget that any failed condition indicates a bug that must be fixed soon! This feature may be misused by handling an Assertion_Error and then not fixing the bug. And this feature will be misused by some program authors. But then, what is more important: - Provide tools that support good software engineering practice? or - Prohibit any tools that can be misused? Dynamically checked contracts are such a tool. > How are going to marry exceptions propagating from contracts with contracts > on exceptions? The contract must always state "Assertion error is not raised!" Anything else violates some contract, anyway. (But note that if contracts are not proven, they can be lies.) > Some exceptions are more exceptional than others? Aren't we > fed up with Program_Error? What are your issues with Program_Error? I don't have any. > > Actually, there is one exception that is difficult to specify. It is our > > old fellow > > > > Storage_Error. > > > > On the level of source code analysis, you > > actually cannot prove that this exception will not be raised. > > Firstly, you if you don't want to prove anything about a certain exception, > you would add this exception to all contracts involved and take care about > exceptions of interest. So you just add "can raise Storage_Error" to any contract? (Maybe implicitly.) > Secondly, you would rather prove conditionals, like: Storage_Error is not > propagated when given amount of memory is available in the specified pools. > This is good enough for most cases, which are not about any exact bound, > but about existence of such bound, i.e. about memory leak detection. You are so violately against dynamically checked conditions ... and then you propose some heuristic that you just claim to be "good enough for most cases"? > Thirdly, you would be able to provide axioms. E.g. for some complex > recursive operation, you could just specify the upper memory consumption > bound known to you from other sources, and let the prover to go with that > (the oracle). > > I think conservative Storage_Error proof is pretty doable. If you move the > upper bound a pair Kbytes upward it would eliminate most of problems. Good luck with any recursive program. And (I am sure you know this) any approach to really prove upper bounds on the storage requirements would imply to solve the Halting Problem. > We certainly could learn from Java mistakes rather than repeating them > (e.g. interfaces). Which is probably why Ada so far has no contracted exceptions. Not that they cannot be done -- but nobody knows how to write such contracts that they really become useful. -- ---- Stefan.Lucks (at) uni-weimar.de, University of Weimar, Germany ---- ------ I love the taste of Cryptanalysis in the morning! ------