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