Theory ExamplesTC

(* Title:      Examples using Hoare Logic for Total Correctness
   Author:     Walter Guttmann
*)

section ‹Examples using Hoare Logic for Total Correctness›

theory ExamplesTC
  imports Hoare_Logic
begin

text ‹
This theory demonstrates a few simple partial- and total-correctness proofs.
The first example is taken from HOL/Hoare/Examples.thy written by N. Galm.
We have added the invariant ‹m ≤ a›.
›

lemma multiply_by_add: "VARS m s a b
  {a=A ∧ b=B}
  m := 0; s := 0;
  WHILE m≠a
  INV {s=m*b ∧ a=A ∧ b=B ∧ m≤a}
  DO s := s+b; m := m+(1::nat) OD
  {s = A*B}"
  by vcg_simp

text ‹
Here is the total-correctness proof for the same program.
It needs the additional invariant ‹m ≤ a›.
›

lemma multiply_by_add_tc: "VARS m s a b
  [a=A ∧ b=B]
  m := 0; s := 0;
  WHILE m≠a
  INV {s=m*b ∧ a=A ∧ b=B ∧ m≤a}
  VAR {a-m}
  DO s := s+b; m := m+(1::nat) OD
  [s = A*B]"
  apply vcg_tc_simp
  by auto

text ‹
Next, we prove partial correctness of a program that computes powers.
›

lemma power: "VARS (p::int) i
  { True }
  p := 1;
  i := 0;
  WHILE i < n
    INV { p = x^i ∧ i ≤ n }
     DO p := p * x;
        i := i + 1
     OD
  { p = x^n }"
  apply vcg_simp
  by auto

text ‹
Here is its total-correctness proof.
›

lemma power_tc: "VARS (p::int) i
  [ True ]
  p := 1;
  i := 0;
  WHILE i < n
    INV { p = x^i ∧ i ≤ n }
    VAR { n - i }
     DO p := p * x;
        i := i + 1
     OD
  [ p = x^n ]"
  apply vcg_tc
  by auto

text ‹
The last example is again taken from HOL/Hoare/Examples.thy.
We have modified it to integers so it requires precondition ‹0 ≤ x›.
›

lemma sqrt_tc: "VARS r
  [0 ≤ (x::int)]
  r := 0;
  WHILE (r+1)*(r+1) <= x
  INV {r*r ≤ x}
  VAR { nat (x-r)}
  DO r := r+1 OD
  [r*r ≤ x ∧ x < (r+1)*(r+1)]"
  apply vcg_tc_simp
  by (smt (verit) div_pos_pos_trivial mult_less_0_iff nonzero_mult_div_cancel_left)

text ‹
A total-correctness proof allows us to extract a function for further use.
For every input satisfying the precondition the function returns an output satisfying the postcondition.
›

lemma sqrt_exists:
  "0 ≤ (x::int) ⟹ ∃r' . r'*r' ≤ x ∧ x < (r'+1)*(r'+1)"
  using tc_extract_function sqrt_tc by blast

definition "sqrt (x::int) ≡ (SOME r' . r'*r' ≤ x ∧ x < (r'+1)*(r'+1))"

lemma sqrt_function:
  assumes "0 ≤ (x::int)"
    and "r' = sqrt x"
  shows "r'*r' ≤ x ∧ x < (r'+1)*(r'+1)"
proof -
  let ?P = "λr' . r'*r' ≤ x ∧ x < (r'+1)*(r'+1)"
  have "?P (SOME z . ?P z)"
    by (metis (mono_tags, lifting) assms(1) sqrt_exists some_eq_imp)
  thus ?thesis
    using assms(2) sqrt_def by auto
qed

text ‹Nested loops!›

lemma "VARS (i::nat) j
  [ True ]
  WHILE 0 < i
    INV { True }
    VAR { z = i }
     DO i := i - 1; j := i;
        WHILE 0 < j
        INV { z = i+1 }
        VAR { j }
        DO j := j - 1 OD
     OD
  [ i ≤ 0 ]"
  apply vcg_tc
  by auto

end