I’m trying to see what SPARK is like, get a feel for it, see how much of this year’s AoC I can complete with it, but trying the simplest of problems ( #1 Multiples of 3 or 5 - Project Euler ) leads me to some problems that are not (easily) found on the net.
When converting the simple Ada solution to SPARK, I ran into overflow problems. The function body looks like this:
for I in Lwb .. Upb - 1 loop
if I mod 3 = 0 or else I mod 5 = 0 then
Sum := Sum + I;
end if;
end loop;
and the third line causes an overflow. Understandable. So I limited the types of Lwb and Upb to this:
type Sqrt_Int_Range is range 0 .. 50000;
and added:
Pre => Lwb <= Upb and then Upb > 0 and then
Natural (Upb) * Natural (Upb) < Natural'Last,
Then I want to assert in the loop invariant that Sum will always be less than I * I, which should be enough proof. However, I can’t even get there, because now the pre-condition has an overflow (“overflow check might fail, cannot prove upper bound”). So I tried
I’m hoping the book I ordered (Building High Integrity Applications with SPARK) can give some guidance, but it can take two weeks more to arrive, so does anybody know how to proceed in the mean time? Or some other way to attack this (trivial) problem?
Note that for 32-bit natural, the square root is less than 50000.
with Ada.Text_IO;
with Ada.Integer_Text_IO;
with Integer_Sqrt;
procedure Sqrt
is
pragma SPARK_Mode (Off);
use Ada;
subtype Sqrt_Nat_Range
is Natural
range 0 .. Integer_Sqrt.Sqrt (Natural'Last);
begin
Text_IO.Put ("Natural'last = ");
Integer_Text_IO.Put (Natural'last);
Text_Io.New_Line;
Text_IO.Put ("sqrt(Natural'last) = ");
Integer_Text_IO.Put (Sqrt_Nat_Range'last);
Text_IO.New_Line;
end Sqrt;
--------------------------------------------------------------------------------
package Integer_Sqrt is
pragma Pure;
function Sqrt (N : Natural) return Natural;
end Integer_Sqrt;
--------------------------------------------------------------------------------
package body Integer_Sqrt is
function Sqrt (N : Natural) return Natural is
X : Natural := N;
Y : Natural := (if X = Natural'Last then X / 2 else (X + 1) / 2);
begin
while Y < X loop
X := Y;
Y := (X + N / X) / 2;
end loop;
return X;
end Sqrt;
end Integer_Sqrt;
Thanks. First, I thought Natural was like unsigned long, so 2^32-1.
But your solution unfortunately doesn’t bring me closer. The prover doesn’t accept that Sqrt_Nat_Range'Last * Sqrt_Nat_Range'Last <= Natural'Last, so then I would have to add that as a Post condition to Integer_Sqrt.Sqrt leading me to the same problem. And I didn’t know how to prove termination of the loop nor how to prove (X + N / X) / 2 doesn’t overflow.
So instead, I lowered the upper bound of the range to 40000. As I also couldn’t find where to place pragma Overflow_mode, I ended up adding -gnato13 to the compiler flags, which has the same effect, but globally. Not entirely satisfying, but it works.
The overflow warning on Sum := Sum + I; (which is what this is all about in the first place) I got rid of by adding the loop invariant Sum <= I * I. It’s unclear to me how much maths the prover knows, but it did accept it.