SPARK: Defining the meaning of a proof function

SPARK: Defining the meaning of a proof function

[Phil Thornley]

One significant gap in the SPARK language is the absence of any way to
define the meaning of a proof function (i.e. a function declared in
annotations).  The only way to do this is in a user proof rule that is
read by the Simplifier.

If the user were able to define the meaning of a proof function in the
SPARK text then this could be incorporated into the VCs generated by
the Examiner.  This would remove the need for a number of user rules
and make completion of the proofs simpler, quicker and less error-
prone.

At present, a function operation can be given a return annotation, and
this is used to add a hypothesis about the value returned by a call of
that function - but only where that operation appears in code.
Hypotheses are not added when the equivalent proof function appears in
a proof context (pre/post, assert, check).

As an experiment I extended my SPARKRules utility to mimic the effect
of adding proof function definitions to SPARK.  The extended program
edits the Examiner generated VCs to add the hypotheses that (I think)
the Examiner would add if it had definitions for proof functions.

The results were very positive and suggest that the combination of
adding proof function definitions to SPARK and using more capable
solvers via Victor has the potential to make proof a great deal
simpler and quicker.

I used the current version of the Tokeneer software as the trial
application.  Full details of the work and the results are in:
http://www.sparksure.com/resources/Proof_Function_Definitions.pdf

Summarising the results:

* The current version of Tokeneer has 84 distinct user rules (some
very complex) that create 97 rules in 26 user rule files.  These
complete the proofs of 101 VCs in 43 operations.  (There are a further
24 VCs that have review proofs.)

* If the proof function definitions are added and Victor used to
submit the VCs to alt-ergo, then there are just 10 VCs (out of 101)
left unproven in 8 operations (out of 43).  Completion of these
remaining VCs requires 17 user rules (all of which are quite simple).

It is the combination of proof function definitions and Victor that is
effective:
Adding the proof function definitions leaves 58 VCs in 30 operations.
Using Victor leaves 76 VCs in 36 operations.

I hope that this experiment will make the enhancement more likely -
supported customers are encouraged to use their influence to promote
this change.

Although I will not make this extended version of SPARKRules (called
SPARKRulesPF) generally available (since it is not a properly tested
program) I am prepared to make it available on request provided that
the reason for the request is given and an undertaking made to share
any results.  Replies to this message will reach me, or you can use a
sparksure.com address.  The program compiles and runs on both Windows
7 and openSUSE 11.3 using the latest versions of Gnat and SPARK (but
Victor is available only on Linux at present).

Cheers,

Phil Thornley

Re: SPARK: Defining the meaning of a proof function

[Alexander Senier]

On Sun, 27 Feb 2011 04:51:42 -0800 (PST)
Phil Thornley <phil.jpthornley@gmail.com> wrote:

> One significant gap in the SPARK language is the absence of any way to
> define the meaning of a proof function (i.e. a function declared in
> annotations).  The only way to do this is in a user proof rule that is
> read by the Simplifier.

There is another way to define the meaning of proof functions. However,
it is not integrated into the SPARK source text either. The current
release of the Isabelle theorem prover [1] adds the HOL/SPARK proof
environment. This environment can read in the VCs produced by the
Examiner and the Simplifier (and associated FDL rules etc.) and present
them as proof contexts in Isabelle.

Abstract SPARK proof functions can be associated with concrete Isabelle
functions (of suitable type, checked by Isabelle). Using HOL/SPARK can
be advantageous, as e.g. existing powerful proof strategies, automated
external provers and existing proofs may be used to prove open VCs.
Furthermore, it is much harder to introduce logical inconsistencies in
Isabelle/HOL than in hand-written rule files.

Examples for using HOL/SPARK can be found in "src/HOL/SPARK/Examples"
in the Isabelle2011 distribution. Unfortunately,  there is no
documentation available currently (being improved at the moment).

Regards
Alex

[1] http://isabelle.in.tum.de