Re: [isabelle] Annotations in Simpl

On 10/07/2012, at 6:53 PM, Lukas Bulwahn wrote:

> 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.

I'd argue that Hoare logic or not is a separate issue from proving properties separately or not. Any combination of these is possible. It's just that most Hoare logic frameworks practically force you in one direction (and they shouldn't).

> 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.

We have seen some of that effect in our proofs as well, but not everywhere. Some loops for instance need a fairly complex invariant just to be able to say anything about them, and in this case it can be easier to get the strongest statement you can come up with and be done with it. This can be awkward to use, because you will either get a fairly large precondition with many cases or one that is fairly strong and may be harder to establish than necessary, but it may still be worth it overall. 

On the other hand, depending on the use context you might just be interested in the fact that a certain function doesn't change certain parts of the state. This can be a completely automatic proof where you don't even have to state the specification, because a tool can figure it out for you. But if you are only allowed to have precisely one specification per function, you can't make use of such simple automatic side proofs.

In the functional world, the first case is similar to a complex recursion that you may only want to go through once with a specific complex induction, strong induction hypothesis etc. You can be better off proving everything you'll ever need about that function in one go. The second case are the many simple, small functions that make up the bulk of the program. For these you want nice, clean simp and other rules to set up automation.

The point is, you should have the choice to do what fits best.


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