Re: SPARK - divide algorithm issue

[Phil Thornley <phil.jpthornley@gmail.com>]

In article <957ef6e4-23d8-499f-ba19-20d32e82a7df@googlegroups.com>, 
see.my.homepage@gmail.com says...
> 
> Playing further with implementing division in SPARK, but this time an example from John Barnes book is causing problems:
> 
>     procedure Divide (M, N : in Integer; Q, R : out Integer);
>     --# derives Q, R from M, N;
>     --# pre M >= 0 and N > 0;
>     --# post (M = Q * N + R) and (R < N) and R >= 0;
> 
>     procedure Divide (M, N : in Integer; Q, R : out Integer) is
>     begin
>         Q := 0;
>         R := M;
>         loop
>             --# assert M = Q * N + R and R >= 0;
>             exit when R < N;
>             Q := Q + 1;   -- here
>             R := R - N;
>         end loop;
>     end Divide;
> 
> In this example SPARK cannot prove that the marked line (Q := Q + 1) is safe with respect to Integer'Last. What is most frustrating is that this is a book example, where it is claimed to verify OK.

You should not expect too much of the SPARK Simplifier - there are many 
proveable VCs that it fails to prove and this is one of them:

procedure_divide_5.
H1:    q * n + r <= 2147483647 .
H2:    n <= 2147483647 .
H3:    q * n + r >= 0 .
H4:    n > 0 .
H5:    r <= 2147483647 .
H6:    n <= r .
H7:    q >= - 2147483648 .
H8:    q <= 2147483647 .
H9:    integer__size >= 0 .
       ->
C1:    q <= 2147483646 .

This can be proved by contradiction: if q >= 2147483647 then there is a 
contradiction with H1, H4 and H6 (remembering that n is integer). 

Victor/Alt-Ergo does prove this VC:
,divide,procedure,,,5,,true,0.016,,,

No matter how good the proof tools are, there will probably always be 
some proveable VCs that they fail to prove in practicable time - so it's 
up to the analyst to distinguish these from unproveable ones.

If you are using worked examples to help with understanding SPARK proof, 
you may find the proof tutorials at:
http://www.sparksure.com
helpful.
(But these are now somewhat out-of-date with respect to the recent 
versions of SPARK, and particularly with respect to the change in the 
way return annotations are handled in the 2012 GPL version.)

Cheers,

Phil