From: bakolden5@gmail.com
Subject: Proving A Loop will Terminate in SPARK Question
Date: Wed, 8 Mar 2017 13:25:28 -0800 (PST)
Date: 2017-03-08T13:25:28-08:00 [thread overview]
Message-ID: <08170e98-468b-4e50-b3b5-6a8a68f2d1ba@googlegroups.com> (raw)
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)?
next reply other threads:[~2017-03-08 21:25 UTC|newest]
Thread overview: 2+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-03-08 21:25 bakolden5 [this message]
2017-03-09 15:13 ` Proving A Loop will Terminate in SPARK Question Phil Thornley
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox