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.29.51 with SMTP id h39mr4729874yha.12.1429963712770; Sat, 25 Apr 2015 05:08:32 -0700 (PDT) X-Received: by 10.140.97.7 with SMTP id l7mr34048qge.0.1429963712755; Sat, 25 Apr 2015 05:08:32 -0700 (PDT) Path: border2.nntp.dca1.giganews.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!z60no3644869qgd.0!news-out.google.com!a41ni846qgf.1!nntp.google.com!j5no3644026qga.1!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Sat, 25 Apr 2015 05:08:32 -0700 (PDT) In-Reply-To: <871tj9dp5b.fsf@theworld.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=87.91.37.131; posting-account=hya6vwoAAADTA0O27Aq3u6Su3lQKpSMz NNTP-Posting-Host: 87.91.37.131 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> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: Subject: Re: {Pre,Post}conditions and side effects From: vincent.diemunsch@gmail.com Injection-Date: Sat, 25 Apr 2015 12:08:32 +0000 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Xref: number.nntp.giganews.com comp.lang.ada:192922 Date: 2015-04-25T05:08:32-07:00 List-Id: Le samedi 25 avril 2015 02:31:57 UTC+2, Bob Duff a =E9crit=A0: > Same reason we put comments in the code. Comments are not "essential > program logic" in the sense defined above -- if you delete all the > comments, the program will still work. But we still want comments. > Likewise, one should normally write assertions (like Pre and Predicate) > so the program still works if they are deleted. >=20 > Assertions are like comments, except we have a higher confidence > that they are actually true. >=20 I agree. Assertions express logical properties of the program. One can have= a high confidence in them for two reasons : 1. mathematical correctness according to a given theory 2. proof that the code is coherent with the assertion, using a tool. But Assertions should stay as comments, for they are not code but logical f= ormula expressed in a mathematical langage. They were comments in Spark 05 and it is still t= he case in Frama-C or many formal proof systems. Hoare logic is supposed to give "correctness = by construction" :=20 which is the ability to never fail on a runtime test. This is required in s= afety critical systems. But what Ada and SPARK=A02014 are doing is "design by contract", as Bertran= d Meyer=20 called it. This makes a confusion between a precondition and a runtime test= . It may look appealing in the beginning but it is nothing else than a test harness = put around a subprogram. With all the problems related to it : how to debug it ? Shoul= d it raise exceptions ? It breaks the separation between specification and implementat= ion etc. Therefore, I don't think that it is the right choice for a langage that is = mainly used in safety critical systems. https://groups.google.com/forum/#!searchin/comp.lang.ada/future$20of$20spar= k/comp.lang.ada/klr0i37j0uk/5IeGMdlh7PYJ Kind regards, Vincent