Re: SPARK: Defining the meaning of a proof function

[Alexander Senier <mail@senier.net>]

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