author | blanchet |
Tue, 09 Sep 2014 20:51:36 +0200 | |
changeset 58249 | 180f1b3508ed |
parent 42174 | d0be2722ce9f |
child 58310 | 91ea607a34d8 |
permissions | -rw-r--r-- |
13020 | 1 |
|
2 |
header {* \chapter{The Owicki-Gries Method} |
|
3 |
||
4 |
\section{Abstract Syntax} *} |
|
5 |
||
16417 | 6 |
theory OG_Com imports Main begin |
13020 | 7 |
|
8 |
text {* Type abbreviations for boolean expressions and assertions: *} |
|
9 |
||
42174 | 10 |
type_synonym 'a bexp = "'a set" |
11 |
type_synonym 'a assn = "'a set" |
|
13020 | 12 |
|
13 |
text {* The syntax of commands is defined by two mutually recursive |
|
14 |
datatypes: @{text "'a ann_com"} for annotated commands and @{text "'a |
|
15 |
com"} for non-annotated commands. *} |
|
16 |
||
58249
180f1b3508ed
use 'datatype_new' (soon to be renamed 'datatype') in Isabelle's libraries
blanchet
parents:
42174
diff
changeset
|
17 |
datatype_new 'a ann_com = |
13020 | 18 |
AnnBasic "('a assn)" "('a \<Rightarrow> 'a)" |
19 |
| AnnSeq "('a ann_com)" "('a ann_com)" |
|
20 |
| AnnCond1 "('a assn)" "('a bexp)" "('a ann_com)" "('a ann_com)" |
|
21 |
| AnnCond2 "('a assn)" "('a bexp)" "('a ann_com)" |
|
22 |
| AnnWhile "('a assn)" "('a bexp)" "('a assn)" "('a ann_com)" |
|
23 |
| AnnAwait "('a assn)" "('a bexp)" "('a com)" |
|
24 |
and 'a com = |
|
25 |
Parallel "('a ann_com option \<times> 'a assn) list" |
|
26 |
| Basic "('a \<Rightarrow> 'a)" |
|
27 |
| Seq "('a com)" "('a com)" |
|
28 |
| Cond "('a bexp)" "('a com)" "('a com)" |
|
29 |
| While "('a bexp)" "('a assn)" "('a com)" |
|
30 |
||
31 |
text {* The function @{text pre} extracts the precondition of an |
|
32 |
annotated command: *} |
|
33 |
||
39246 | 34 |
primrec pre ::"'a ann_com \<Rightarrow> 'a assn" where |
13020 | 35 |
"pre (AnnBasic r f) = r" |
39246 | 36 |
| "pre (AnnSeq c1 c2) = pre c1" |
37 |
| "pre (AnnCond1 r b c1 c2) = r" |
|
38 |
| "pre (AnnCond2 r b c) = r" |
|
39 |
| "pre (AnnWhile r b i c) = r" |
|
40 |
| "pre (AnnAwait r b c) = r" |
|
13020 | 41 |
|
42 |
text {* Well-formedness predicate for atomic programs: *} |
|
43 |
||
39246 | 44 |
primrec atom_com :: "'a com \<Rightarrow> bool" where |
13020 | 45 |
"atom_com (Parallel Ts) = False" |
39246 | 46 |
| "atom_com (Basic f) = True" |
47 |
| "atom_com (Seq c1 c2) = (atom_com c1 \<and> atom_com c2)" |
|
48 |
| "atom_com (Cond b c1 c2) = (atom_com c1 \<and> atom_com c2)" |
|
49 |
| "atom_com (While b i c) = atom_com c" |
|
13020 | 50 |
|
51 |
end |