Re: [isabelle] Annotations in Simpl



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

John




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