Re: SPARK - divide algorithm issue

[Maciej Sobczak <see.my.homepage@gmail.com>]

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