Re: [isabelle] Annotations in Simpl

Hi Lars,

On 10/07/2012, at 3:59 AM, Lars Noschinski wrote:
> The only other solution I have found would be adding the invariants only in the proof:
> procedures mult2 (n :: nat, m :: nat | r :: nat)
> "
>  ´r :== (0 :: nat) ;;
>  WHILE ´n ≠ 0
>  DO
>    ´r :== ´r + ´m ;;
>    ´n :== ´n - 1
>  OD
> "
> lemma (in mult2_impl) mult2:
>  "∀m n. Γ ⊢ ⦃´m = m ∧ ´n = n⦄ ´r :== PROC mult2(´m, ´n) ⦃´r = m * n⦄"
>  apply vcg_step
>  apply (hoare_rule HoarePartial.Seq)
>   defer
>   apply (hoare_rule I="⦃ ´m = m ∧ ´m * n = ´r + ´m * ´n  ⦄" in
>     HoarePartial.reannotateWhileNoGuard)
>   apply vcg
>   apply (simp_all add: mult_Suc_right[symmetric])
>  apply vcg
>  apply simp
>  done

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.

From that point of view, I'm fairly convinced that annotations and invariants belong with the proof, not with the program (or everything belongs with the program). It would be nice to have a better notation for connecting them, though.


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