equal
deleted
inserted
replaced
8 |
8 |
9 theory Hoare imports Denotation begin |
9 theory Hoare imports Denotation begin |
10 |
10 |
11 types assn = "state => bool" |
11 types assn = "state => bool" |
12 |
12 |
13 constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) |
13 definition |
14 "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t" |
14 hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) where |
|
15 "|= {P}c{Q} = (!s t. (s,t) : C(c) --> P s --> Q t)" |
15 |
16 |
16 inductive |
17 inductive |
17 hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) |
18 hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) |
18 where |
19 where |
19 skip: "|- {P}\<SKIP>{P}" |
20 skip: "|- {P}\<SKIP>{P}" |
24 | While: "|- {%s. P s & b s} c {P} ==> |
25 | While: "|- {%s. P s & b s} c {P} ==> |
25 |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}" |
26 |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}" |
26 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> |
27 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> |
27 |- {P'}c{Q'}" |
28 |- {P'}c{Q'}" |
28 |
29 |
29 constdefs wp :: "com => assn => assn" |
30 definition |
30 "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)" |
31 wp :: "com => assn => assn" where |
|
32 "wp c Q = (%s. !t. (s,t) : C(c) --> Q t)" |
31 |
33 |
32 (* |
34 (* |
33 Soundness (and part of) relative completeness of Hoare rules |
35 Soundness (and part of) relative completeness of Hoare rules |
34 wrt denotational semantics |
36 wrt denotational semantics |
35 *) |
37 *) |