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.35.90 with SMTP id k26mr3664442otd.92.1489008329176;
        Wed, 08 Mar 2017 13:25:29 -0800 (PST)
X-Received: by 10.157.4.129 with SMTP id 1mr1275416otm.17.1489008329106; Wed,
 08 Mar 2017 13:25:29 -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!w124no1241632itb.0!news-out.google.com!78ni8361itm.0!nntp.google.com!w124no1241631itb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Wed, 8 Mar 2017 13:25:28 -0800 (PST)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=69.53.212.124;
 posting-account=O1bJfwoAAAC_Vd4l-lauVJNDJxmhacGI
NNTP-Posting-Host: 69.53.212.124
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <08170e98-468b-4e50-b3b5-6a8a68f2d1ba@googlegroups.com>
Subject: Proving A Loop will Terminate in SPARK Question
From: bakolden5@gmail.com
Injection-Date: Wed, 08 Mar 2017 21:25:29 +0000
Content-Type: text/plain; charset=UTF-8
Xref: news.eternal-september.org comp.lang.ada:33502
Date: 2017-03-08T13:25:28-08:00
List-Id: <comp.lang.ada>

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)?