# [isabelle] Annotations in Simpl

Hi everyone,
I am working on formalizing some algorithms using Simpl from the AFP.

`Is there some lightweight way (in a procedures definition) to annotate a
``loop with the property that a variable stays unchanged? For procedures,
``there is the may-not-modify-globals syntax; but a similar thing does not
``seem to exist for loops (and it is not clear, how this would fit in). At
``the moment, I am using the ANNO command for this purpose:
`
procedures mult1 (n :: nat, m :: nat | r :: nat)
"
ANNO τ.
{τ}
´r :== (0 :: nat) ;;
WHILE ´n ≠ 0
INV ⦃ ´m = ⇗τ⇖m ∧ ´m * ⇗τ⇖n = ´r + ´m * ´n ⦄
DO
´r :== ´r + ´m ;;
´n :== ´n - 1
OD
⦃ ´r = ⇗τ⇖m * ⇗τ⇖n ⦄
"
lemma (in mult1_impl) mult1:
"∀m n. Γ ⊢ ⦃´m = m ∧ ´n = n⦄ ´r :== PROC mult1(´m, ´n) ⦃´r = m * n⦄"
apply vcg
apply (simp_all add: mult_Suc_right[symmetric])
done

`Here I need a full write down a full specification already in the
``procedure definition. This is particularly annoying for ANNO statements
``deeper in the procedure definition.
`

`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

`Here, it is harder to see which invariants are actually used for which
``loop (and I can only use the full vcg after I reached the loop), so I
``would like to know about nicer solutions (if there are any).
`
-- Lars

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