*To*: John Wickerson <jpw48 at cam.ac.uk>*Subject*: Re: [isabelle] Annotations in Simpl*From*: Gerwin Klein <gerwin.klein at nicta.com.au>*Date*: Tue, 10 Jul 2012 19:15:27 +1000*Cc*: isabelle-users Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <9FB8B822-D488-4598-89A1-19BABE2A6DCB@cam.ac.uk>*References*: <4FFB1C13.4090400@in.tum.de> <A7D5435C-E30C-46E4-BA36-ABCF5C4B515D@nicta.com.au> <9FB8B822-D488-4598-89A1-19BABE2A6DCB@cam.ac.uk>

On 10/07/2012, at 6:26 PM, John Wickerson wrote: >> 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. > > I think it's fine in Hoare logic to prove multiple properties of a function C, like {P1}C{Q1} and {P2}C{Q2}. The point of the rules of conjunction > > {P1}C{Q1} {P2}C{Q2} > -------------------- > {P1∧P2}C{Q1∧Q2} > > and disjunction > > {P1}C{Q1} {P2}C{Q2} > -------------------- > {P1∨P2}C{Q1∨Q2} > > are to allow these multiple properties to be combined. Sure. Maybe I should clarify: I'm not objecting to Hoare logic as such, it's perfectly capable of showing multiple independent properties about a program (that's what we've used in the seL4 proofs I was mentioning, precisely with rules as above). I'm objecting to how it is usually used and presented, and to what tools in turn usually imply for your workflow. The fact that there is precisely one specification statement and one invariant that you can annotate for each procedure/loop in usual tools and presentations is the problem. This is hard to avoid if these annotations go into the program, because it is awkward to differentiate between multiple proofs in one invariant annotation (possible, but very annoying). > But in the "proof outline" representation of a Hoare logic proof, where the program text is interspersed with assertions, you can't really represent this without writing out the program text multiple times, which is a hassle. That is the direction I meant, only that this is already the case with just invariants (which will need to be provided somehow, at least if there is automation/vcg support in some form). It is perfectly possible to mention these annotations in the proof only, and I'm arguing that this is where they belong. Cheers, Gerwin

**References**:**[isabelle] Annotations in Simpl***From:*Lars Noschinski

**Re: [isabelle] Annotations in Simpl***From:*Gerwin Klein

**Re: [isabelle] Annotations in Simpl***From:*John Wickerson

- Previous by Date: Re: [isabelle] Annotations in Simpl
- Next by Date: Re: [isabelle] Annotations in Simpl
- Previous by Thread: Re: [isabelle] Annotations in Simpl
- Next by Thread: Re: [isabelle] Annotations in Simpl
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list