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.13.209.65 with SMTP id t62mr1189852ywd.16.1489757087871; Fri, 17 Mar 2017 06:24:47 -0700 (PDT) X-Received: by 10.157.82.47 with SMTP id e47mr1612103oth.18.1489757087817; Fri, 17 Mar 2017 06:24:47 -0700 (PDT) Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!1.eu.feeder.erje.net!feeder.erje.net!2.us.feeder.erje.net!weretis.net!feeder6.news.weretis.net!feeder.usenetexpress.com!feeder1.iad1.usenetexpress.com!border1.nntp.dca1.giganews.com!nntp.giganews.com!n21no912736qta.1!news-out.google.com!78ni17287itm.0!nntp.google.com!u69no3802438ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail Newsgroups: comp.lang.ada Date: Fri, 17 Mar 2017 06:24:47 -0700 (PDT) In-Reply-To: <2ac671c3-ea12-4a53-9ee8-dc72b9702bb2@googlegroups.com> Complaints-To: groups-abuse@google.com Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=90.115.177.251; posting-account=P04rJQoAAAAcZ1eXXrg_e5YPG0xhsQtg NNTP-Posting-Host: 90.115.177.251 References: <58caf52b$0$24793$426a74cc@news.free.fr> <2ac671c3-ea12-4a53-9ee8-dc72b9702bb2@googlegroups.com> User-Agent: G2/1.0 MIME-Version: 1.0 Message-ID: <966f8f48-13c0-4928-9aad-624d2184418f@googlegroups.com> Subject: Re: [Spark] Proving GCD From: =?UTF-8?B?RnLDqWTDqXJpYyBQUkFDQQ==?= Injection-Date: Fri, 17 Mar 2017 13:24:47 +0000 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Xref: news.eternal-september.org comp.lang.ada:46410 Date: 2017-03-17T06:24:47-07:00 List-Id: Le vendredi 17 mars 2017 14:00:54 UTC+1, Phil Thornley a =C3=A9crit=C2=A0: > >=20 > > And I still have the same message from Spark. Any idea ? >=20 > Any non-trivial code with loops will need to have loop invariants. These = links explain why and a bit about how to write them: > http://www.spark-2014.org/entries/detail/spark-2014-rationale-loop-invari= ants > http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-how-to= -write-loop-invariants There's already one but a really simple one, just stating that Local_B is d= ecreasing. I will check with the links you provided me. > I would also recommend starting with an easier example than the GCD algor= ithm. > A Google search for "SPARK loop invariant" will throw up lots more = examples. > (But some of these will be about the previous version of SPARK - now refe= rred > to as SPARK 2005.) As I own a copy of the "Building High Integrity Applications with SPARK" bo= ok from John W. McCormick and Peter Chapin, I already have several examples= but I found it more interesting to take an example from scratch. Moreover, it was a good point to compare with the unit test method as seen = in http://www2.cs.uni-paderborn.de/cs/ag-schaefer-static/Lehre/Lehrveransta= ltungen/Vorlesungen/SoftwareQualityAssurance/WS0405/SQA-III-p104-182.pdf pa= ge 56. > Note that your postcondition states that the result is a common divisor o= f A > and B, but does not state that it is the greatest such divisor. But doing so would be to rewrite the whole algorithm in the contract, no ? Fred