SPARK and other provers (Was: Re: What's wrong with C++?)

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

On Oct 11, 8:45 am, Yannick Duchêne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Le Mon, 10 Oct 2011 15:31:21 +0200, Paul Colin Gloster  
> <Colin_Paul_Glos...@acm.org> a écrit:
>
> > Yannick Duchêne (Hibou57) <yannick_duch...@Yahoo.Fr> sent on October  
> > 9th, 2011:
> > |-------------------------------------|
> > |"[..]                                |
> > |[..] SPARK [..] and there is no ready|
> > |accessible alternatives)."           |
> > |-------------------------------------|
>
> > There are many alternatives, but they lack built-in
> > integration with Ada by default.
>
> Yes, it has too infer value ranges and other implicit validity conditions  
> automatically, without explicit specifications from the author (will have  
> a look at Alt-Ergo a future day, and an even farer future day, will have  
> some personal experiments with something).
>

If you are considering using Alt-Ergo with SPARK you may be interested
in this result from an experiment.

Using some code that was already proved using the Simplifier (and
which required a number of user rules) I let Alt-Ergo have a go at all
the VCs that the Simplifer was unable to prove directly (i.e. without
user rules).

The first discovery was that the default proof steps limit (set to
5000 in GPS) is way too high (at least for my desktop - Core
i5/750@2.67GHz).  I had to bring it down to the 300-500 range.

Secondly the Victor driver (the interface to Alt-Ergo) supplied with
SPARK (and used by GPS) is very inflexible:
- It enforces the option that all conclusions of a VC are 'fused' - so
that failure to prove any one conclusion means that none of the
conclusions are reported as proved - and there seems to be no way to
find out which conclusion(s) are/are not provable.
- There is no way for the user to supply any user rules to Alt-Ergo.
This is essential if Alt-Ergo is going to have any chance of proving
VCs that reference proof functions.
(These restrictions can be easily worked round by some simple mods to
the victor driver program.)

Using the victor driver from the command line would also get round
these problems, but the documentation provides no help with this.

With these changes, the figures from the POGS summary are (omitting
columns with all zeros):

Total VCs by type:
                       -----------Proved By Or Using-----------
                Total  Spark   Simp (User) ViCToR
Assert/Post       118      0    100(   36)     18
Precondition       45      0     36(    3)      9
Check stmnt.      222      0    206(  154)     16
Runtime check     195      0    195             0
Refinem. VCs        6      5      1(    1)      0
Inherit. VCs        0      0      0             0
=================================================
Totals:           586      5    538(  194)     43
%Totals:                  1%    92%(  33%)     7%

So Alt-Ergo completes the proof of 43 out of 237 VCs that are not
directly proved by the Simplifier.

That's one data point - does anyone else have any others?

Cheers,

Phil