[ProofPower] Proving Properties of SML functions

[Rob Arthan]

On Tuesday 18 May 2004 4:42 pm, Roger Bishop Jones wrote:

> On Tuesday 18 May 2004  3:40 pm, Marcel Oliveira wrote:
> > Do you suggest any better approach to me? I know I am confused
> > right now, and I really neeed some light ;-)
>
> There hasn't been a lot of metatheoretic work done in ProofPower
> as far as I am aware, and some of the things you would
> naturally use for this kind of thing (like recursive datatypes
> for abstract syntax) are not well provided for.

It's not too bad in Z. Z free types give you the recursive data types and 
there is a fairly simple recipe for constructing the induction principle you 
need. This has spurred me to finish the promised supplementary Z example on 
the web site, which you can now find if you go to:

	http://www.lemma-one.com/ProofPower/examples/examples.html

The example is about refinement and partial correctness. It contains one 
document that defines a notion of refinement and another that an abstract 
model of a simple imperative programming language annotated with Floyd-Hoare 
style pre- and post-conditions. It gives the semantics of the language is 
defined along with a notion of correctness for the annotations (using an 
instance of the generic notion of refinement from the first document). It 
then defines a Z model of a pre-condition calculator and proves that it is 
sound with respect to these notions.

The second document provides an example of how to deal with abstract syntax in 
Z, using the recipe I mentioned.

> That means that you have to be smart in the way you
> code these things up.
>
> Fortunately there is one good example provided by Rob Arthan
> who did the metatheory for ProofPower HOL in ProofPower HOL.
> So I recommend you look at that and see whether the methods
> he used will adapt to your problem.
>
> The material is in the ProofPower distribution and
> may be found in the five documents spc001 to spc005.
>
>     * HOL Formalised: Language and Overview
>     * HOL Formalised: Semantics
>     * HOL Formalised: Deductive System
>     * HOL Formalised: Proof Development System
>     * HOL Formalised: Formal Design of the Logical Kernel
>

Thanks for the encomium, Roger. The pre-condition calculator is probably a 
better place to start for Marcel if he wants to specify things in 
"functional" Z, prove things about it and then transcribe the Z into ML 
(assuming he needs an implementation). It's also much shorter than the HOL 
specs. This kind of approach, alas, typically with little funding for doing 
work on proof, has worked well in various applications of ProofPower in the 
past.

Regards,

Rob.