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,FREEMAIL_FROM autolearn=unavailable autolearn_force=no version=3.4.4 X-Received: by 10.236.216.52 with SMTP id f50mr33084714yhp.13.1431508442267; Wed, 13 May 2015 02:14:02 -0700 (PDT) X-Received: by 10.140.23.50 with SMTP id 47mr296015qgo.24.1431508442253; Wed, 13 May 2015 02:14:02 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!peer03.iad.highwinds-media.com!news.highwinds-media.com!feed-me.highwinds-media.com!z60no8070585qgd.0!news-out.google.com!k20ni2269qgd.0!nntp.google.com!j5no8065010qga.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Wed, 13 May 2015 02:14:02 -0700 (PDT) In-Reply-To: <709f632c-7e94-4b89-b392-f1ff444ad2e3@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=185.30.133.97; posting-account=hya6vwoAAADTA0O27Aq3u6Su3lQKpSMz NNTP-Posting-Host: 185.30.133.97 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> <5f0cdb00-27de-4f2d-ae84-8a0a1a199200@googlegroups.com> <709f632c-7e94-4b89-b392-f1ff444ad2e3@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <8c654092-053b-4847-9b32-31a2cc6636cc@googlegroups.com> Subject: Re: {Pre,Post}conditions and side effects From: vincent.diemunsch@gmail.com Injection-Date: Wed, 13 May 2015 09:14:02 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Received-Bytes: 2930 X-Received-Body-CRC: 3630974549 Xref: news.eternal-september.org comp.lang.ada:25861 Date: 2015-05-13T02:14:02-07:00 List-Id: Le mardi 12 mai 2015 16:53:47 UTC+2, john...@googlemail.com a =E9crit=A0: > Claire Dross has a post on this .. sounds relevant but > I'm not sure! >=20 > http://www.spark-2014.org/entries/detail/manual-proof-in-spark-2014 >=20 > J. Hum... I find this proof excessivly complicated. The idea of describing the proof function as a functional language would do it, through "ghost code" result = in the mixing of numerical computation and symbolic manipulations by the same = code as ML on OCaml like to do it. The problem with this approach is : how can you be sure that your proof is = correct if it is hardly readable ? By the way this is one of the consequences of not keeping logical formulas = separate from Ada code : one ends up by writing pseudo Ada code for the sol= e purpose of handling logical formula. The result is a kind of mess. I prefer the Peter Chapin approach (see his message below). Vincent =20