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