Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!cs.utexas.edu!romp!auschs!awdprime!duke.austin.ibm.com!wkh
From: wkh@duke.austin.ibm.com
Newsgroups: comp.specification
Subject: Z spec for Producer/Consumer
Message-ID: <8288@awdprime.UUCP>
Date: 7 Jun 91 15:03:36 GMT
Sender: news@awdprime.UUCP
Reply-To: wkh@duke.austin.ibm.com ()
Lines: 19


I'm in the midst of learning Z and a co-worker has challenged me to
write a Z spec for the Producer/Consumer problem, i.e. independent
producers and consumers communicating via a bounded buffer. The buffer
itself is no problem, I should be able to model it with a finite
sequence. What I'm not clear on is how to model synchronization; do I
have to write schema for mutexes and condition variables to express the
synchronization constraints? It seems like doing so introduces an
unnecessary "how" into the specification's "what".

A meta-question is: is Z really suited to writing specifications for
distributed systems or am I better off with CSP or CCS as my co-worker claims?

Thanks ... WkH

Ward K Harold				(512) 823-4139 [T/L 793-4139]
IBM Personal Systems Programming	external: wkh@dce.austin.ibm.com
11400 Burnet Rd., Zip 2603		internal: wkh@duke.austin.ibm.com
Austin, TX  78758			vnet: wharrold --ausvmq