equal
deleted
inserted
replaced
5 |
5 |
6 Specification of Chandy and Charpentier's Allocator |
6 Specification of Chandy and Charpentier's Allocator |
7 *) |
7 *) |
8 |
8 |
9 Alloc = Follows + Extend + PPROD + |
9 Alloc = Follows + Extend + PPROD + |
|
10 |
|
11 constdefs |
|
12 (**TOO STRONG: DELETE**) |
|
13 modular :: "['a, ('a=>'b) program set] => bool" |
|
14 "modular i X == |
|
15 ALL F G. F : X --> drop_prog i F = drop_prog i G --> G : X" |
|
16 |
|
17 |
|
18 (UNITY.thy????????????????*) |
|
19 (*An Idle program can do nothing*) |
|
20 Idle :: 'a program set |
|
21 "Idle == {F. Union (Acts F) <= Id}" |
10 |
22 |
11 (*simplifies the expression of some specifications*) |
23 (*simplifies the expression of some specifications*) |
12 constdefs |
24 constdefs |
13 sub :: ['a, 'a=>'b] => 'b |
25 sub :: ['a, 'a=>'b] => 'b |
14 "sub i f == f i" |
26 "sub i f == f i" |