59189
|
1 |
chapter \<open>The Rely-Guarantee Method\<close>
|
13020
|
2 |
|
59189
|
3 |
section \<open>Abstract Syntax\<close>
|
13020
|
4 |
|
16417
|
5 |
theory RG_Com imports Main begin
|
13020
|
6 |
|
59189
|
7 |
text \<open>Semantics of assertions and boolean expressions (bexp) as sets
|
62042
|
8 |
of states. Syntax of commands \<open>com\<close> and parallel commands
|
|
9 |
\<open>par_com\<close>.\<close>
|
13020
|
10 |
|
42174
|
11 |
type_synonym 'a bexp = "'a set"
|
13020
|
12 |
|
59189
|
13 |
datatype 'a com =
|
13020
|
14 |
Basic "'a \<Rightarrow>'a"
|
|
15 |
| Seq "'a com" "'a com"
|
59189
|
16 |
| Cond "'a bexp" "'a com" "'a com"
|
|
17 |
| While "'a bexp" "'a com"
|
|
18 |
| Await "'a bexp" "'a com"
|
13020
|
19 |
|
42174
|
20 |
type_synonym 'a par_com = "'a com option list"
|
13020
|
21 |
|
62390
|
22 |
end
|