equal
deleted
inserted
replaced
|
1 (* Title: HOL/UNITY/Channel |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Unordered Channel |
|
7 |
|
8 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3 |
|
9 *) |
|
10 |
|
11 Channel = WFair + Option + |
|
12 |
|
13 types state = nat set |
|
14 |
|
15 consts |
|
16 F :: state program |
|
17 |
|
18 constdefs |
|
19 minSet :: nat set => nat option |
|
20 "minSet A == if A={} then None else Some (LEAST x. x:A)" |
|
21 |
|
22 rules |
|
23 |
|
24 UC1 "F : (minSet -` {Some x}) co (minSet -` (Some`atLeast x))" |
|
25 |
|
26 (* UC1 "F : {s. minSet s = x} co {s. x <= minSet s}" *) |
|
27 |
|
28 UC2 "F : (minSet -` {Some x}) leadsTo {s. x ~: s}" |
|
29 |
|
30 end |