Re: [isabelle] Annotations in Simpl
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
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
"whileAnno b (name_loop v) V c = whileAnno b I V c"
by (simp add: whileAnno_def)
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:
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 (hoare_rule HoarePartial.Seq)
apply (hoare_rule I="⦃ ´m = m ∧ ´m * n = ´r + ´m * ´n ⦄" in
apply (simp_all add: mult_Suc_right[symmetric])
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