Re: [isabelle] Annotations in Simpl

Hi Lars.

You may not necessarily need to single-step the vcg. Have a look at whileAnno_def: "whileAnno b I V c == While b c". Since this is full equality, you can add or remove annotations with fold/unfold if this is useful.

The annotations are really just hints to the vcg, not elements of the syntax or semantics of SIMPL.

So, one thing you could do is annotate the loops with names, and then substitute them on the spot.

definition "name_loop v = UNIV"

(in proc defn):

WHILE ´n ≠ 0
     INV name_loop ''foo''
     DO ... OD


lemma annotate_named_loop:
  "whileAnno b (name_loop v) V c = whileAnno b I V c"
  by (simp add: whileAnno_def)

(in unfolding)
apply (simp add: annotate_named_loop[where name="''foo''" and I="..."])

Not a lot nicer, but maybe a bit less fiddly.

I guess it would be nicer if SIMPL provided a facility by which you could add such invariant declarations/redeclarations into the context and have the vcg notice them as necessary. There might even be a way to do this already, though I can't think what it would be.


On 10/07/12 09:09, Gerwin Klein wrote:
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
    ´r :== ´r + ´m ;;
    ´n :== ´n - 1

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)
   apply (hoare_rule I="⦃ ´m = m ∧ ´m * n = ´r + ´m * ´n  ⦄" in
   apply vcg
   apply (simp_all add: mult_Suc_right[symmetric])
  apply vcg
  apply simp
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.