Re: [isabelle] Annotations in Simpl

On 07/10/2012 01:09 AM, Gerwin Klein wrote:

This is what we used for the kernel proof. It doesn't look nice and has the disadvantages you explain. It does have the advantage that you can pick different invariants/annotations for each proof about that function.

Slight side rant: It's strange that Hoare logic insists that one would only ever prove one property about a function, have one invariant, and one annotation that fits them all. In theory this is all equivalent and there is a "complete specification", but in practise that is not how things are proved or should be proved.

Just think about what we do for functional programs in Isabelle. Nothing is more cumbersome and useless than having to state one lemma that says everything about one function.
This observation motivated me back in 2007 to NOT define a Hoare logic for Imperative-HOL, but to do all the case studies just with a simple predicate capturing the operational semantics. Composition of facts of the same program therefore does not even require any special rule and use of object connectives, but can be done with resolution, e.g. the OF attribute.

As that was so non-standard, other people seem to have defined a Hoare logic for Imperative-HOL nevertheless.

I tried to prove properties of the imperative programs separately.
In my case studies, the properties of the functions relied heavily one on the previous one, which required me to re-state properties again and again.

The solution I then came up with is still quite adhoc: I came up with richer induction rules to obtain already proved facts in the context with names.

With the infrastructure at the moment, I think proving all the facts at once would have been simpler in my case. The most difficult case study, the imperative unification algorithm, is still managable by proving all properties at once, and the most reasoning of the different properties overlap in various places in the proof.

Kernel functions in seL4 have probably a different flavor.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.