Z spec for Producer/Consumer

Thread View: comp.specification

1 messages

[T] Back to Threads [V] Tree View [G] Group Articles

1 total messages Started by wkh Fri, 07 Jun 1991 15:03

#442

Author: wkh
Date: Fri, 07 Jun 1991 15:03

19 lines
1324 bytes

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

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads