equal
deleted
inserted
replaced
7 header "Correctness of Hoare by Fixpoint Reasoning" |
7 header "Correctness of Hoare by Fixpoint Reasoning" |
8 |
8 |
9 theory HoareEx = Denotational: |
9 theory HoareEx = Denotational: |
10 |
10 |
11 text {* |
11 text {* |
12 An example from the HOLCF paper by Mueller, Nipkow, Oheimb, Slotosch \cite{MuellerNvOS99}. |
12 An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch |
13 It demonstrates fixpoint reasoning by showing the correctness of the Hoare |
13 \cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing |
14 rule for while-loops. |
14 the correctness of the Hoare rule for while-loops. |
15 *} |
15 *} |
16 |
16 |
17 types assn = "state => bool" |
17 types assn = "state => bool" |
18 |
18 |
19 constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) |
19 constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) |