Lately me and Benjamin Nauck have been investigating languages with proving functionality, such as the variant of Ada known as SPARK. The basic idea of such languages is that the programmer can supply a set of contracts on the inputs and outputs of each function, and then a prover (gnatprove) is run on the program which checks that the contracts are indeed fulfilled for every possible combination of inputs. This is great for catching lots of bugs, for example issues due to overflow or when math functions are given atypical floating points numbers like ∞ or NaN (not-a-number). By comparison languages such as C or C++ are not able to provide guarantees like these, not even current popular "safe" languages like Rust or Go. Update: there are some inaccuracies in this post, see the comments section.
I decided to make a Saturday project out of writing a primality tester and integer square root function in Ada, then throwing some SPARK contracts on top of them. Both the primality testing (IsPrime) and integer square root functions (Isqrt and Isqrt2) are limited by the maximum range of Integer in Ada: 2147483647. This also happens to be a Mersenne prime. IsPrime does typical trial division up to the square root of the input value. Integer square roots are done because Sqrt in Ada.Numerics.Elementary_Functions gives no guarantees on the returned values beyond them being >= 0. gnatprove also has trouble proving that if some integer x is >= 5 then Float(x) >= 5.0. For these reasons I decided to implement my own square root function.
I decided to write two integer square root implementations. The first implementation (Isqrt) iterates i from 2 .. 46340 (floor(sqrt(2147483647))) and checks at every step if i² >= num and returns either i or i-1 if that is the case. This is of course very slow, but fairly easy to prove correct. The key to proving this was the Loop_Invariant pragma. Isqrt is listed below:
-- Returns floor(sqrt(num)) for 0 <= num <= 2147483647 (Natural'Last)
function Isqrt (num : Natural) return Natural with
SPARK_Mode => On,
Post =>
(if num < 46340*46340 then
num in Isqrt'Result**2 .. (Isqrt'Result + 1)**2 - 1)
and then (if num >= 46340*46340 then Isqrt'Result = 46340)
is
begin
-- 0 -> 0, 1 -> 1
if num < 2 then
return num;
end if;
for i in 2 .. 46340 loop
if i*i = num then
return i;
end if;
if i*i > num then
return i-1;
end if;
pragma Loop_Invariant(i*i < num);
end loop;
return 46340;
end Isqrt;
The second integer square root (Isqrt2) computes the value by recursion. A range is kept and halved at every step until it is known that the solution lies between two consecutive integers. Then the lowest of those two integers is returned. This variant turned out to be easier to write. Isqrt2 and the recursive Isqrt2_inner are given below:
function Isqrt2_inner (num, lo, hi : Natural) return Natural with
SPARK_Mode => On,
Pre =>
lo in 1 .. 46340 and then
hi in 1 .. 46340 and then
lo < hi and then
num in lo**2 .. hi**2-1,
Post =>
num in Isqrt2_inner'Result**2 .. (Isqrt2_inner'Result + 1)**2 - 1
is
mid : Natural;
begin
if lo = hi-1 then
return lo;
end if;
mid := (lo + hi) / 2;
pragma Assert (mid in lo+1 .. hi-1);
if mid**2 > num then
return Isqrt2_inner(num, lo, mid);
else
return Isqrt2_inner(num, mid, hi);
end if;
end Isqrt2_inner;
-- Faster, recursive version of Isqrt
function Isqrt2 (num : Natural) return Natural with
SPARK_Mode => On,
Post =>
(if num < 46340*46340 then
Isqrt2'Result < 46340 and then
num in Isqrt2'Result**2 .. (Isqrt2'Result + 1)**2 - 1)
and then (if num >= 46340*46340 then Isqrt2'Result = 46340)
is
begin
-- 0 -> 0, 1 -> 1
if num < 2 then
return num;
end if;
if num >= 46340*46340 then
return 46340;
end if;
return Isqrt2_inner(num, 1, 46340);
end Isqrt2;
IsPrime itself is not very interesting. I don't prove that the function actually behaves correctly, such a proof would be very involved. All we can know is that it will terminate and that its assertions are correct.
The complete code listing will be given below. There are three files: isprime.adb which has the bulk of the code, isprime.ads is like a header, and main.adb which does user interaction:
-- isprime.adb
package body IsPrime is
-- Returns floor(sqrt(num)) for 0 <= num <= 2147483647 (Natural'Last)
function Isqrt (num : Natural) return Natural with
SPARK_Mode => On,
Post =>
(if num < 46340*46340 then
num in Isqrt'Result**2 .. (Isqrt'Result + 1)**2 - 1)
and then (if num >= 46340*46340 then Isqrt'Result = 46340)
is
begin
-- 0 -> 0, 1 -> 1
if num < 2 then
return num;
end if;
for i in 2 .. 46340 loop
if i*i = num then
return i;
end if;
if i*i > num then
return i-1;
end if;
pragma Loop_Invariant(i*i < num);
end loop;
return 46340;
end Isqrt;
function Isqrt2_inner (num, lo, hi : Natural) return Natural with
SPARK_Mode => On,
Pre =>
lo in 1 .. 46340 and then
hi in 1 .. 46340 and then
lo < hi and then
num in lo**2 .. hi**2-1,
Post =>
num in Isqrt2_inner'Result**2 .. (Isqrt2_inner'Result + 1)**2 - 1
is
mid : Natural;
begin
if lo = hi-1 then
return lo;
end if;
mid := (lo + hi) / 2;
pragma Assert (mid in lo+1 .. hi-1);
if mid**2 > num then
return Isqrt2_inner(num, lo, mid);
else
return Isqrt2_inner(num, mid, hi);
end if;
end Isqrt2_inner;
-- Faster, recursive version of Isqrt
function Isqrt2 (num : Natural) return Natural with
SPARK_Mode => On,
Post =>
(if num < 46340*46340 then
Isqrt2'Result < 46340 and then
num in Isqrt2'Result**2 .. (Isqrt2'Result + 1)**2 - 1)
and then (if num >= 46340*46340 then Isqrt2'Result = 46340)
is
begin
-- 0 -> 0, 1 -> 1
if num < 2 then
return num;
end if;
if num >= 46340*46340 then
return 46340;
end if;
return Isqrt2_inner(num, 1, 46340);
end Isqrt2;
-- Tests whether a Positive is prime
function IsPrime (num : Positive) return Boolean with
SPARK_Mode => On
is
top : Positive;
begin
if num = 2 or num = 3 then
return True;
end if;
if num mod 2 = 0 then
return False;
end if;
top := Isqrt2(num);
pragma Assert (top < num);
for i in Integer range 3 .. top loop
pragma Assert (i < num);
if num mod i = 0 then
return False;
end if;
end loop;
return True;
end IsPrime;
end IsPrime;
-- isprime.ads
package IsPrime is
function IsPrime (num : Positive) return Boolean with
SPARK_Mode => On,
Pre => num >= 2;
end IsPrime;
-- main.adb
with Ada.Text_IO;
with Ada.Integer_Text_IO;
with IsPrime;
procedure Main
is
num : Integer;
begin
Ada.Text_IO.Put_Line("Enter an integer to test");
Ada.Integer_Text_IO.Get(num);
--num := 2147483647; -- largest Positive, also a prime
if num < 2 then
Ada.Text_IO.Put_Line("Number must be >= 2");
return;
end if;
Ada.Text_IO.Put_Line(Boolean'Image(IsPrime.IsPrime(num)));
end Main;
Example gnatprove output on the entire project:
gnatprove -P/home/thardin/projects/ada/exempel/default.gpr --level=0 --ide-progress-bar -U
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
Summary logged in /home/thardin/projects/ada/exempel/obj/gnatprove/gnatprove.out
[2018-01-20 21:24:42] process terminated successfully, elapsed time: 05.20s
Report:
Summary of SPARK analysis
=========================
--------------------------------------------------------------------------------------------------------
SPARK Analysis results Total Flow Interval CodePeer Provers Justified Unproved
--------------------------------------------------------------------------------------------------------
Data Dependencies . . . . . . .
Flow Dependencies . . . . . . .
Initialization 6 6 . . . . .
Non-Aliasing . . . . . . .
Run-time Checks 26 . . . 26 (CVC4) . .
Assertions 5 . . . 5 (CVC4) . .
Functional Contracts 6 . . . 6 (CVC4) . .
LSP Verification . . . . . . .
--------------------------------------------------------------------------------------------------------
Total 43 6 (14%) . . 37 (86%) . .
Analyzed 2 units
in unit isprime, 4 subprograms and packages out of 4 analyzed
IsPrime.IsPrime at isprime.ads:3 flow analyzed (0 errors and 0 warnings) and proved (6 checks)
IsPrime.Isqrt at isprime.adb:3 flow analyzed (0 errors and 0 warnings) and proved (10 checks)
IsPrime.Isqrt2 at isprime.adb:55 flow analyzed (0 errors and 0 warnings) and proved (6 checks)
IsPrime.Isqrt2_inner at isprime.adb:30 flow analyzed (0 errors and 0 warnings) and proved (15 checks)
in unit main, 0 subprograms and packages out of 1 analyzed
Main at main.adb:5 skipped
I tried to prove that Main behaves correctly, but unfortunaly the Text_IO functions do not provide any suitable contracts:
gnatprove -P/home/thardin/projects/ada/exempel/default.gpr --ide-progress-bar --level=0 -u main.adb
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
main.adb:10:15: warning: no Global contract available for "Put_Line"
main.adb:10:15: warning: assuming "Put_Line" has no effect on global items
main.adb:11:23: warning: no Global contract available for "Get"
main.adb:11:23: warning: assuming "Get" has no effect on global items
main.adb:15:18: warning: no Global contract available for "Put_Line"
main.adb:15:18: warning: assuming "Put_Line" has no effect on global items
main.adb:19:15: warning: no Global contract available for "Put_Line"
main.adb:19:15: warning: assuming "Put_Line" has no effect on global items
Summary logged in /home/thardin/projects/ada/exempel/obj/gnatprove/gnatprove.out
[2018-01-20 21:26:37] process terminated successfully, elapsed time: 02.20s
This Stackoverflow question seems to indicate that a SPARK.Ada.Text_IO module exists. Unfortunately I don't have that package in my setup. It was previously known as SPARK_IO, which also does not exist on my machine.
There are however some major limitations with SPARK. The biggest one is that dynamic memory allocation is not allowed. All SPARK functions must also terminate. So SPARK is not suitable for every case at least. There is however a separation kernel called Muen which is written in SPARK, so clearly a lot can be done with it.
Finally, I'll mention that there are other tools and languages with similar functionality, such as Coq and Idris. I haven't looked at those yet, but Coq seems especially popular among mathematicians.
Comments
Piotr Trojanek has this to say, prompted by my future post about Frama-C:
Hi Tomas,
I just read your old blog post "Trying out Ada SPARK". Thanks for describing
your experience! It looks like not everything went well with your trial but
perhaps I could clarify some of the issues.
* "Integer square roots are done because Sqrt in
Ada.Numerics.Elementary_Functions gives no guarantees on the returned values
beyond them being >= 0."
Even if SPARK would exactly model the guarantees provided by the Ada RM
G.2.4(6) (i.e. "The maximum relative error exhibited by [Sqrt] is 2.0 ·
EF.Float_Type'Model_Epsilon"), I would still suggest you to stick with
integers, as otherwise you easily risk imprecision.
See https://en.wikipedia.org/wiki/Floating-point_arithmetic, which says: "Any
integer with absolute value less than 2^24 can be exactly represented in the
single precision format". In particular, the Integer'Last can't be represented
exactly as Float.
* "gnatprove also has trouble proving that if some integer x is >= 5 then
Float(x) >= 5.0."
Indeed, the 2017 public SPARK release only included the alt-ergo solver, which
isn't great at floating-point problems (you could add other solvers on your own
and we know that some researchers did). The 2018 release includes also the CVC4
solver, which can easily prove what you describe:
$ cat test.adb
procedure Test (X : Integer) with Pre => X >= 5, SPARK_Mode is
begin
pragma Assert (Float (X) >= 5.0);
end;
$ gnatprove -P test.gpr -f --report=statistics
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
test.adb:1:11: warning: subprogram "Test" has no effect
test.adb:3:19: info: assertion proved (CVC4: 1 VC in max 0.0 seconds and 1 step)
test.adb:3:26: info: range check proved (Interval)
Summary logged in /tmp/flo/gnatprove/gnatprove.out
Finally, the SPARK Pro release can use the CodePeer analyser and as described
in the User's Guide:
"CodePeer analysis is particularly interesting when analyzing code using
floating-point computations, as CodePeer is both fast and precise for
proving bounds of floating-point operations."
http://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_run_gnatprove.html#using-codepeer-static-analy
* the Post aspect of the non-recursive Isqrt function can be simplified :) i.e.
Post =>
(if num < AAA then XXX)
and then
(if num >= AAA then YYY);
is equivalent to
Post => (if num < AAA then XXX else YYY);
* you don't really need to special-case 0 and 1, I believe; you can handle them
in the FOR loop, i.e.:
for i in 0 .. 46340 loop ...
* you can nest the "inner" function of the recursive implementation inside
Isqrt2 and then it won't need the "num" parameter, i.e.:
function Isqrt2 (num : Natural) return Natural with ... is
function Isqrt2_inner (lo, hi : Natural) return Natural with ... is
begin
... here you can reference the parameter of the enclosing routine ...
end Isqrt2_inner;
begin
...
end Isqrt;
This could be marginally faster (because less data is put on the stack when
calling the "inner" routine), but I didn't measure.
* "I tried to prove that Main behaves correctly, but unfortunaly the Text_IO
functions do not provide any suitable contracts"
The warnings that you see do not prevent gnatprove from proving your code!
They only mean that the side-effect of writing to the standard output is not
modelled by the tool (which only matters if you are paranoid about leaking the
information out of your program).
* "Unfortunately I don't have [the SPARK.Ada.Text_IO] package in my setup."
You should have it as share/examples/spark/spark_io/spark-text_io.ads. It was
included in both 2017 and 2018 releases.
And in your latest blog post on Frama-C you say:
* "The assigns clause is something we didn't see in Ada SPARK."
It looks like you missed a whole lot of the SPARK's functionality! The "assign"
in Frama-C is a simple variant of the Global contract in SPARK. See
http://docs.adacore.com/spark2014-docs/html/ug/en/source/subprogram_contracts.html#data-dependencies
You might also want to explore the Depends contract, which carries even more
information than the Global; Frama-C doesn't have anything like that.
* "[in SPARK] every program must terminate"
This is not quite true, because you can annotate procedures with the No_Return
aspect :) However, termination is indeed an important issue in SPARK and we
describe it in detail in the User's Guide:
http://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_write_subprogram_contracts.html#subprogram-termination
* [subprograms in SPARK] can't perform dynamic memory allocation"
Hopefully not for long! See https://www.reddit.com/r/ada/comments/8jsyl2/borrowing_safe_pointers_from_rust_in_spark/
I am looking forward to read about your experience with other tools for the
formal verification! If you find any issues with the SPARK toolchain in the
future, please do not hesitate to ask at spark2014-discuss@lists.adacore.com.
--
Piotr