equal
deleted
inserted
replaced
6 header "Correctness of Hoare by Fixpoint Reasoning" |
6 header "Correctness of Hoare by Fixpoint Reasoning" |
7 |
7 |
8 theory HoareEx imports Denotational begin |
8 theory HoareEx imports Denotational begin |
9 |
9 |
10 text {* |
10 text {* |
11 An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch |
11 An example from the HOLCF paper by Müller, Nipkow, Oheimb, Slotosch |
12 \cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing |
12 \cite{MuellerNvOS99}. It demonstrates fixpoint reasoning by showing |
13 the correctness of the Hoare rule for while-loops. |
13 the correctness of the Hoare rule for while-loops. |
14 *} |
14 *} |
15 |
15 |
16 types assn = "state => bool" |
16 types assn = "state => bool" |