wkh@duke.austin.ibm.com (06/07/91)
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