equal
deleted
inserted
replaced
1 |
|
2 header {* \chapter{The Rely-Guarantee Method} |
|
3 |
|
4 \section {Abstract Syntax} |
|
5 *} |
|
6 |
|
7 theory RG_Com imports Main begin |
|
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 |
|