section"Correctness of Hoare by Fixpoint Reasoning"
theory HoareEx imports Denotational begin
text‹
An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch cite‹MuellerNvOS99›. It demonstrates fixpoint reasoning by showing
the correctness of the Hoare rule for while-loops. ›
type_synonym assn = "state ==> bool"
definition
hoare_valid :: "[assn, com, assn] ==> bool" (‹|= {(1_)}/ (_)/ {(1_)}›50) where "|= {P} c {Q} = (∀s t. P s ∧ D c⋅(Discr s) = Def t ⟶ Q t)"
lemma WHILE_rule_sound: "|= {A} c {A} ==> |= {A} WHILE b DO c {λs. A s ∧¬ bval b s}" apply (unfold hoare_valid_def) apply (simp (no_asm)) apply (rule fix_ind) apply (simp (no_asm)) ― ‹simplifier with enhanced ‹adm›-tactic› apply (simp (no_asm)) apply (simp (no_asm)) apply blast done
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 und die Messung sind noch experimentell.
