1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
|
-- FILE: /home/diacon/LANG/Cafe/prog/cws.mod
-- CONTENTS: behavioural specification of a counter with switch object
-- featuring concurrent object composition with synchronization
-- AUTHOR: Shuusaku Iida
-- DIFFICULTY: ***
-- -------------------------------------------------------------
-- ON-OFF
-- -------------------------------------------------------------
mod! ON-OFF {
[ Value ]
ops on off : -> Value
}
-- -------------------------------------------------------------
-- SWITCH
-- -------------------------------------------------------------
mod* SWITCH {
protecting(ON-OFF)
*[ Switch ]*
op init : -> Switch
bop on_ : Switch -> Switch -- method
bop off_ : Switch -> Switch -- method
bop state_ : Switch -> Value -- attribute
var S : Switch
eq state init = off .
eq state(on S) = on .
eq state(off S) = off .
}
-- -------------------------------------------------------------
-- COUNTER
-- -------------------------------------------------------------
mod* COUNTER {
protecting(INT)
*[ Counter ]*
op init : -> Counter
bop add : Int Counter -> Counter -- method
bop read : Counter -> Int -- attribute
var I : Int
var C : Counter
eq read(init) = 0 .
eq read(add(I, C)) = I + read(C) .
}
-- --------------------------------------------
-- concurrent connection of SWITCH and COUNTER
-- --------------------------------------------
mod* COUNTER-WITH-SWITCH {
protecting(SWITCH + COUNTER)
*[ Cws ]*
op init : -> Cws
bop put : Int Cws -> Cws -- method
bop add_ : Cws -> Cws -- method
bop sub_ : Cws -> Cws -- method
bop read : Cws -> Int -- attribute
bop counter_ : Cws -> Counter -- projection function
bop switch_ : Cws -> Switch -- projection function
var N : Int
var C : Cws
eq read(C) = read(counter C) . -- abbreviation equation for "read"
-- -------------------------------------
-- equations for switch
-- -------------------------------------
eq switch(init) = init .
eq switch put(N, C) = switch C .
eq switch add(C) = on(switch C) .
eq switch sub(C) = off(switch C) .
-- -------------------------------------
-- equations for counter
-- -------------------------------------
eq counter(init) = init .
ceq counter(put(N, C)) = add(N, counter(C))
if state(switch(C)) == on .
ceq counter(put(N, C)) = add(-(N), counter(C))
if state(switch(C)) == off .
eq counter add(C) = counter C .
eq counter sub(C) = counter C .
}
-- -----------------------------------------------------------------
-- proof module (adding hidden equivalence relation to
-- COUNTER-WITH-SWITCH)
-- -----------------------------------------------------------------
module CWS-PROOF {
protecting (COUNTER-WITH-SWITCH)
bop addc : Int Cws -> Cws -- a derived method
-- -------------------------------------
-- eqns for the derived method addc
-- -------------------------------------
var C : Cws
var N : Int
ceq addc(N, C) = put(N, C) if state(switch C) == on .
ceq addc(N, C) = put(-(N), C) if state(switch C) == off .
-- the behavioural equivalence
op _R_ : Cws Cws -> Bool { coherent }
vars C1 C2 : Cws
eq C1 R C2 = switch(C1) =*= switch(C2) and
counter(C1) =*= counter(C2) .
-- a lemma
eq -(- N) = N .
}
--> ---------------------------------------------------------------
--> sub put(m, add put(n, sub init)) R put(n, sub put(m, add init))
--> ---------------------------------------------------------------
open CWS-PROOF .
ops m n : -> Nat .
--> should be true
red sub(put(m, add(put(n, sub(init))))) R put(n, sub(put(m, add(init)))) .
--> should be true
red read(put(m, add(put(n, sub(init))))) ==
read(put(n, sub(put(m, add(init))))) .
close
-- ------------------------------------------------------
-- Theorem: COUNTER-WITH-SWITCH is a (correct) concurrent
-- conection of SWITCH and COUNTER
-- ------------------------------------------------------
-- the synchronization part consists only of a hidden sort
-- the synchronization morphisms are obvious
-- the morphism \psi_1 : SWITCH -> COUNTER-WITH-SWITCH is:
-- -- init -> init
-- -- on -> add
-- -- off -> sub
-- -- state -> state switch
-- the morphism \psi_2 : COUNTER -> COUNTER-WITH-SWITCH is:
-- -- init -> init
-- -- add -> addc ** defined in CWS-PROOF
-- -- read -> read
--> prove that COUNTER-WITH-SWITCH refines COUNTER via \psi_2
open CWS-PROOF .
op c : -> Cws .
op n : -> Int .
--> case 1: state(switch c) = on .
eq state(switch c) = on .
red read(addc(n, c)) == n + read(c) .
close
open CWS-PROOF .
op c : -> Cws .
op n : -> Int .
--> case 2: state(switch c) = off .
eq state(switch c) = off .
red read(addc(n, c)) == n + read(c) .
close
--> prove that COUNTER-WITH-SWITCH refines SWITCH via \psi_1
open CWS-PROOF .
op c : -> Cws .
op n : -> Int .
red state switch add(c) == on .
red state switch sub(c) == off .
close
--> prove the commutativity eqns corresponding to the methods
open CWS-PROOF .
op c : -> Cws .
op n : -> Int .
--> case 1:
eq state(switch c) = on .
red add(addc(n, c)) R addc(n, add(c)) .
red sub(addc(n, c)) R addc(n, sub(c)) .
close
open CWS-PROOF .
op c : -> Cws .
op n : -> Int .
--> case 2: state(switch c) = off .
eq state(switch c) = off .
red add(addc(n, c)) R addc(n, add(c)) .
red sub(addc(n, c)) R addc(n, sub(c)) .
close
--> prove the commutativity eqns corresponding to the attributes
open CWS-PROOF .
op c : -> Cws .
op n : -> Int .
red state(switch put(n, c)) == state(switch c) .
red read(counter add(c)) == read(counter c) .
red read(counter sub(c)) == read(counter c) .
close
--
eof
--
$Id: cws.mod,v 1.1.1.1 2003-06-19 08:30:10 sawada Exp $
|
