SPARK - divide algorithm issue

SPARK - divide algorithm issue

[Maciej Sobczak]

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.
Is it possible that in the meantime there were changes in the toolchain that caused this to stop working?
If yes, what would be the proper strategy to hint the prover that the loop will never run longer than the range of positive values?

(This example looks nicer with Natural and Positive types used where appropriate, but I wanted to make it as close to the original as possible.)

Again, this is SPARK GPL 2011.

-- 
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com

Re: SPARK - divide algorithm issue

[Phil Thornley]

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

Re: SPARK - divide algorithm issue

[Maciej Sobczak]

W dniu sobota, 20 kwietnia 2013 11:02:18 UTC+2 użytkownik Phil Thornley napisał:

> 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,,,

Thank you for directions!

> No matter how good the proof tools are, there will probably always be 
> some proveable VCs that they fail to prove in practicable time

Yes, but the notion of "practicability" is a bit sensitive. :-) In this case the tool gives up after just few milliseconds and then the programmer has to spend orders of magnitude longer with the interactive prover. It would be practical for the tool to invest more effort (that is, more time and memory), as the potential savings are huge. Would one second be enough for the tool to exhaustively try various combinations of available hypotheses (there are only 9 of them here) and contradict them? Certainly, I would be happy to wait that much.
Or maybe 10 seconds would be fine, too?
Or maybe the actual meaning of "practicable" should be a config parameter?

In any case, what is most intriguing is the fact that this example is claimed to verify OK in the book. Is it a regression in the toolchain?

> If you are using worked examples to help with understanding SPARK proof, 
> 
> you may find the proof tutorials at:
> 
> http://www.sparksure.com
> 
> helpful.

Yes, I'm aware of this site and I appreciate your efforts in this area. :-)
Thank you again,

-- 
Maciej Sobczak * http://www.msobczak.com * http://www.inspirel.com