(* Title: Examples using Hoare Logic for Total Correctness
Author: Walter Guttmann
*)
section \<open>Examples using Hoare Logic for Total Correctness\<close>
theory ExamplesTC
imports Hoare_Logic
begin
text \<open>
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 \<open>m \<le> a\<close>.
\<close>
lemma multiply_by_add: "VARS m s a b
{a=A \<and> b=B}
m := 0; s := 0;
WHILE m\<noteq>a
INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
DO s := s+b; m := m+(1::nat) OD
{s = A*B}"
by vcg_simp
text \<open>
Here is the total-correctness proof for the same program.
It needs the additional invariant \<open>m \<le> a\<close>.
\<close>
lemma multiply_by_add_tc: "VARS m s a b
[a=A \<and> b=B]
m := 0; s := 0;
WHILE m\<noteq>a
INV {s=m*b \<and> a=A \<and> b=B \<and> m\<le>a}
VAR {a-m}
DO s := s+b; m := m+(1::nat) OD
[s = A*B]"
apply vcg_tc_simp
by auto
text \<open>
Next, we prove partial correctness of a program that computes powers.
\<close>
lemma power: "VARS (p::int) i
{ True }
p := 1;
i := 0;
WHILE i < n
INV { p = x^i \<and> i \<le> n }
DO p := p * x;
i := i + 1
OD
{ p = x^n }"
apply vcg_simp
by auto
text \<open>
Here is its total-correctness proof.
\<close>
lemma power_tc: "VARS (p::int) i
[ True ]
p := 1;
i := 0;
WHILE i < n
INV { p = x^i \<and> i \<le> n }
VAR { n - i }
DO p := p * x;
i := i + 1
OD
[ p = x^n ]"
apply vcg_tc
by auto
text \<open>
The last example is again taken from HOL/Hoare/Examples.thy.
We have modified it to integers so it requires precondition \<open>0 \<le> x\<close>.
\<close>
lemma sqrt_tc: "VARS r
[0 \<le> (x::int)]
r := 0;
WHILE (r+1)*(r+1) <= x
INV {r*r \<le> x}
VAR {nat (x-r)}
DO r := r+1 OD
[r*r \<le> x \<and> 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 \<open>
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.
\<close>
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
end
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
