Re: [isabelle] Annotations in Simpl
On 07/10/2012 01:09 AM, Gerwin Klein wrote:
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
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.
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
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 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
Kernel functions in seL4 have probably a different flavor.
This archive was generated by a fusion of
Pipermail (Mailman edition) and