11 types assn = "state => bool" |
11 types assn = "state => bool" |
12 |
12 |
13 constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) |
13 constdefs hoare_valid :: "[assn,com,assn] => bool" ("|= {(1_)}/ (_)/ {(1_)}" 50) |
14 "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t" |
14 "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t" |
15 |
15 |
16 consts hoare :: "(assn * com * assn) set" |
16 inductive |
17 syntax "_hoare" :: "[bool,com,bool] => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) |
17 hoare :: "assn => com => assn => bool" ("|- ({(1_)}/ (_)/ {(1_)})" 50) |
18 translations "|- {P}c{Q}" == "(P,c,Q) : hoare" |
18 where |
19 |
|
20 inductive hoare |
|
21 intros |
|
22 skip: "|- {P}\<SKIP>{P}" |
19 skip: "|- {P}\<SKIP>{P}" |
23 ass: "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}" |
20 | ass: "|- {%s. P(s[x\<mapsto>a s])} x:==a {P}" |
24 semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" |
21 | semi: "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" |
25 If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==> |
22 | If: "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==> |
26 |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}" |
23 |- {P} \<IF> b \<THEN> c \<ELSE> d {Q}" |
27 While: "|- {%s. P s & b s} c {P} ==> |
24 | While: "|- {%s. P s & b s} c {P} ==> |
28 |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}" |
25 |- {P} \<WHILE> b \<DO> c {%s. P s & ~b s}" |
29 conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> |
26 | conseq: "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> |
30 |- {P'}c{Q'}" |
27 |- {P'}c{Q'}" |
31 |
28 |
32 constdefs wp :: "com => assn => assn" |
29 constdefs wp :: "com => assn => assn" |
33 "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)" |
30 "wp c Q == (%s. !t. (s,t) : C(c) --> Q t)" |
34 |
31 |