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