Proving A Loop will Terminate in SPARK Question

Proving A Loop will Terminate in SPARK Question

[bakolden5]

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

Re: Proving A Loop will Terminate in SPARK Question

[Phil Thornley]

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