8 |
8 |
9 Hoare = Denotation + |
9 Hoare = Denotation + |
10 |
10 |
11 types assn = state => bool |
11 types assn = state => bool |
12 |
12 |
13 consts |
13 constdefs hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50) |
14 hoare :: "(assn * com * assn) set" |
14 "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t" |
15 hoare_valid :: [assn,com,assn] => bool ("|= {(1_)}/ (_)/ {(1_)}" 50) |
|
16 defs |
|
17 hoare_valid_def "|= {P}c{Q} == !s t. (s,t) : C(c) --> P s --> Q t" |
|
18 |
15 |
19 syntax "@hoare" :: [bool,com,bool] => bool ("|- {(1_)}/ (_)/ {(1_)}" 50) |
16 consts hoare :: "(assn * com * assn) set" |
|
17 syntax "@hoare" :: [bool,com,bool] => bool ("|- ({(1_)}/ (_)/ {(1_)})" 50) |
20 translations "|- {P}c{Q}" == "(P,c,Q) : hoare" |
18 translations "|- {P}c{Q}" == "(P,c,Q) : hoare" |
21 |
19 |
22 inductive "hoare" |
20 inductive "hoare" |
23 intrs |
21 intrs |
24 skip "|- {P}Skip{P}" |
22 skip "|- {P}SKIP{P}" |
25 ass "|- {%s.P(s[A a s/x])} x:=a {P}" |
23 ass "|- {%s.P(s[a s/x])} x:=a {P}" |
26 semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" |
24 semi "[| |- {P}c{Q}; |- {Q}d{R} |] ==> |- {P} c;d {R}" |
27 If "[| |- {%s. P s & B b s}c{Q}; |- {%s. P s & ~B b s}d{Q} |] ==> |
25 If "[| |- {%s. P s & b s}c{Q}; |- {%s. P s & ~b s}d{Q} |] ==> |
28 |- {P} IF b THEN c ELSE d {Q}" |
26 |- {P} IF b THEN c ELSE d {Q}" |
29 While "|- {%s. P s & B b s} c {P} ==> |
27 While "|- {%s. P s & b s} c {P} ==> |
30 |- {P} WHILE b DO c {%s. P s & ~B b s}" |
28 |- {P} WHILE b DO c {%s. P s & ~b s}" |
31 conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> |
29 conseq "[| !s. P' s --> P s; |- {P}c{Q}; !s. Q s --> Q' s |] ==> |
32 |- {P'}c{Q'}" |
30 |- {P'}c{Q'}" |
33 |
31 |
34 consts swp :: com => assn => assn |
32 constdefs swp :: com => assn => assn |
35 defs swp_def "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)" |
33 "swp c Q == (%s. !t. (s,t) : C(c) --> Q t)" |
36 |
34 |
37 end |
35 end |