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 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Fri, 8 May 2015 09:28:43 +0200 Organization: cbb software GmbH Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: enOx0b+nfqkc2k+TNpOejg.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:25772 Date: 2015-05-08T09:28:43+02:00 List-Id: On Thu, 7 May 2015 21:40:27 +0200, Stefan.Lucks@uni-weimar.de wrote: > But then, the Ada standard would have to define the underlying theorem > prover, for compatibility reasons. Else, the same program may be proven > correct by one prover, where another prover fails. Yes this is a huge problem in my eyes. If you make program legality dependent on the prover you will have false negatives of worst kind: proven correct programs rejected because the standard falsely thought this cannot be proven. >> You ought to fix your >> program (probably by adding an appropriate predicate) so that the check >> *can* be eliminated (or pushed to somewhere where the cost is irrelevant). > > Why do I need to fix the program, if I know it is correct? Just because > the compiler isn't good enough at theorem proving? Right, that is. Consider exceptions as an example. Let P promises not to raise E. If you cannot prove that P is illegal. A think a possible way out is a construct (a pragma) that would allow the programmer to give his word for certain parts of the proof, e.g. some kind of weak axioms. The prover would try to prove without them and if that fails with them (giving a warning). Only if both fails then the program is incorrect. >>> Turning off the checks just hides the problem. > > *IF* there is a problem at all. Sometimes checks fire without any problem, e.g. accessibility checks. In many cases they fail in correct programs. What they actually catch is not the program's behavior being wrong, they do the program design. It is far to late for run time to complain about the design! This is same as with dynamic predicates. They try to deal with something that fundamentally cannot be dealt with at run time. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de