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.99.152.85 with SMTP id l21mr3803726pgo.66.1489072387813;
        Thu, 09 Mar 2017 07:13:07 -0800 (PST)
X-Received: by 10.157.56.117 with SMTP id r50mr1579987otd.12.1489072387754;
 Thu, 09 Mar 2017 07:13:07 -0800 (PST)
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!u69no1556944ita.0!news-out.google.com!78ni9184itm.0!nntp.google.com!w124no1557025itb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 9 Mar 2017 07:13:06 -0800 (PST)
In-Reply-To: <08170e98-468b-4e50-b3b5-6a8a68f2d1ba@googlegroups.com>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=88.97.49.112;
 posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
NNTP-Posting-Host: 88.97.49.112
References: <08170e98-468b-4e50-b3b5-6a8a68f2d1ba@googlegroups.com>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <76290fda-916b-43d5-8a3c-630527939eda@googlegroups.com>
Subject: Re: Proving A Loop will Terminate in SPARK Question
From: Phil Thornley <phil.jpthornley@gmail.com>
Injection-Date: Thu, 09 Mar 2017 15:13:07 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:33509
Date: 2017-03-09T07:13:06-08:00
List-Id: <comp.lang.ada>

On Wednesday, March 8, 2017 at 9:25:29 PM UTC, Brian Kolden wrote:
> I got my hands on "Building High Integrity Applications with SPARK" and wanted to do some tests with loop proofs. I quickly ran into a case that I did not know how to verify.
> 
> 	procedure Test is
> 		type Big is mod 2**16;
> 		I : Big := 1;
> 	begin
> 		while I /= 0 loop
> 			I := 2**Natural(I);
> 		end loop;
> 	end Test;
> 
> Theoretically, this loop will end however if the condition was I /= 256, it will not. Is it possible to check if I will reach the condition, given a specific starting value of I (1, in this case)?

This isn't really a good example of how to use SPARK. The procedure has no inputs and has no external effect other than either terminating or running for ever, so has no meaningful contract.

In practice SPARK is mostly about creating contracts for subprograms, and the various proof pragmas inserted into the code, such as Loop_Invariant, are there to support the proof that the code meets its contract.

If I had to write a loop invariant for this code I would start with something like:
I = 1 or I = 2 or I = 4 or I = 16

Cheers,

Phil Thornley