| changeset 16417 | 9bc16273c2d4 |
| parent 13806 | fd40c9d9076b |
| child 18556 | dc39832e9280 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
6 Unordered Channel |
6 Unordered Channel |
7 |
7 |
8 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
8 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
9 *) |
9 *) |
10 |
10 |
11 theory Channel = UNITY_Main: |
11 theory Channel imports UNITY_Main begin |
12 |
12 |
13 types state = "nat set" |
13 types state = "nat set" |
14 |
14 |
15 consts |
15 consts |
16 F :: "state program" |
16 F :: "state program" |