1 |
|
2 header {* \chapter{The Owicki-Gries Method} |
|
3 |
|
4 \section{Abstract Syntax} *} |
|
5 |
|
6 theory OG_Com imports Main begin |
|
7 |
|
8 text {* Type abbreviations for boolean expressions and assertions: *} |
|
9 |
|
10 types |
|
11 'a bexp = "'a set" |
|
12 'a assn = "'a set" |
|
13 |
|
14 text {* The syntax of commands is defined by two mutually recursive |
|
15 datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a |
|
16 com"} for non-annotated commands. *} |
|
17 |
|
18 datatype 'a ann_com = |
|
19 AnnBasic "('a assn)" "('a \<Rightarrow> 'a)" |
|
20 | AnnSeq "('a ann_com)" "('a ann_com)" |
|
21 | AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" |
|
22 | AnnCond2 "('a assn)" "('a bexp)" "('a ann_com)" |
|
23 | AnnWhile "('a assn)" "('a bexp)" "('a assn)" "('a ann_com)" |
|
24 | AnnAwait "('a assn)" "('a bexp)" "('a com)" |
|
25 and 'a com = |
|
26 Parallel "('a ann_com option \<times> 'a assn) list" |
|
27 | Basic "('a \<Rightarrow> 'a)" |
|
28 | Seq "('a com)" "('a com)" |
|
29 | Cond "('a bexp)" "('a com)" "('a com)" |
|
30 | While "('a bexp)" "('a assn)" "('a com)" |
|
31 |
|
32 text {* The function @{text pre} extracts the precondition of an |
|
33 annotated command: *} |
|
34 |
|
35 consts |
|
36 pre ::"'a ann_com \<Rightarrow> 'a assn" |
|
37 primrec |
|
38 "pre (AnnBasic r f) = r" |
|
39 "pre (AnnSeq c1 c2) = pre c1" |
|
40 "pre (AnnCond1 r b c1 c2) = r" |
|
41 "pre (AnnCond2 r b c) = r" |
|
42 "pre (AnnWhile r b i c) = r" |
|
43 "pre (AnnAwait r b c) = r" |
|
44 |
|
45 text {* Well-formedness predicate for atomic programs: *} |
|
46 |
|
47 consts atom_com :: "'a com \<Rightarrow> bool" |
|
48 primrec |
|
49 "atom_com (Parallel Ts) = False" |
|
50 "atom_com (Basic f) = True" |
|
51 "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)" |
|
52 "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)" |
|
53 "atom_com (While b i c) = atom_com c" |
|
54 |
|
55 end |
|