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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable 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!nntp-feed.chiark.greenend.org.uk!ewrotcd!reality.xs3.de!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Fri, 8 May 2015 17:58:54 -0500 Organization: Jacob Sparre Andersen Research & Innovation 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> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1431125935 730 24.196.82.226 (8 May 2015 22:58:55 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Fri, 8 May 2015 22:58:55 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:25777 Date: 2015-05-08T17:58:54-05:00 List-Id: "Dmitry A. Kazakov" wrote in message news:mnn1t6yjuegl$.2tsyoc7gm7rk.dlg@40tude.net... > 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. It's certainly true that there is a potential portability problem here, but I think we have no choice but to allow it. Otherwise, we have to force these sorts of things into warnings, which means that they have no real force and worse that the Standard cannot talk about them. In such a case, programming will never get better. > 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. No, the problem is in portability. The standard cannot get involved in what can and cannot be proven (other, perhaps than setting some minimum requirements). Beyond that, through, it has to be implementation-defined. So the question boils down to do we allow one compiler to reject a program because it can't be proved that it does not raise an exception (for example) while another compiler allows it because it can prove that? I think we HAVE to allow that sort of non-portability; for one thing, it gives vendors a serious incentive to improve their compilers. On top of which, it is idiocy to require a compiler to reject something that it can tell is not a problem. (Particularly, something optional like exception contracts.) I expect this to be the defining question of Ada 202x; we can't have exception contracts without deciding this question somehow, and I don't see much possible advancement for Ada without those contracts. Randy.