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.157.6.76 with SMTP id 70mr6709096otn.5.1489757323629;
        Fri, 17 Mar 2017 06:28:43 -0700 (PDT)
X-Received: by 10.157.55.247 with SMTP id x110mr135400otb.6.1489757323588;
 Fri, 17 Mar 2017 06:28:43 -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!news.glorb.com!w124no3815342itb.0!news-out.google.com!m191ni1344itc.0!nntp.google.com!u69no3802981ita.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Fri, 17 Mar 2017 06:28:43 -0700 (PDT)
In-Reply-To: <966f8f48-13c0-4928-9aad-624d2184418f@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>
 <eaf03e7d-a2dd-4490-9156-3a25c32634eb@googlegroups.com>
 <2ac671c3-ea12-4a53-9ee8-dc72b9702bb2@googlegroups.com>
 <966f8f48-13c0-4928-9aad-624d2184418f@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <4caef81d-b348-48e2-82df-bbc81491dbe4@googlegroups.com>
Subject: Re: [Spark] Proving GCD
From: =?UTF-8?B?RnLDqWTDqXJpYyBQUkFDQQ==?= <frederic.praca@free.fr>
Injection-Date: Fri, 17 Mar 2017 13:28:43 +0000
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable
Xref: news.eternal-september.org comp.lang.ada:46411
Date: 2017-03-17T06:28:43-07:00
List-Id: <comp.lang.ada>

Le vendredi 17 mars 2017 14:24:48 UTC+1, Fr=C3=A9d=C3=A9ric PRACA a =C3=A9c=
rit=C2=A0:
> 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. Thes=
e links explain why and a bit about how to write them:
> > http://www.spark-2014.org/entries/detail/spark-2014-rationale-loop-inva=
riants
> > 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=
 decreasing.

My mistake, there's no invariant only a variant :)
I will try to find one.

> I will check with the links you provided me.
>=20
> > I would also recommend starting with an easier example than the GCD alg=
orithm. > A Google search for "SPARK loop invariant" will throw up lots mor=
e examples.
> > (But some of these will be about the previous version of SPARK - now re=
ferred > to as SPARK 2005.)
> As I own a copy of the "Building High Integrity Applications with SPARK" =
book from John W. McCormick and Peter Chapin, I already have several exampl=
es 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 see=
n in http://www2.cs.uni-paderborn.de/cs/ag-schaefer-static/Lehre/Lehrverans=
taltungen/Vorlesungen/SoftwareQualityAssurance/WS0405/SQA-III-p104-182.pdf =
page 56.
>=20
> > Note that your postcondition states that the result is a common divisor=
 of 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 =
?
>=20
> Fred