[Prev][Next][Index]
Re:
-
To: makofka@monet.vill.edu (Spring 93 )
-
Subject: Re:
-
From: horning
-
Date: Thu, 15 Dec 94 17:33:27 -0800
-
Cc: horning
-
Delivery-Date: Thu, 15 Dec 94 17:33:35 -0800
-
In-Reply-To: Message of Thu, 15 Dec 94 19:23:12 EST
Doug,
Don't be bashful about asking questions like this of the whole list. It
gives you a chance to get more views than my own, and also keeps others
aware of both the questions that are asked and the answers given. (We
don't have a Larch FAQ yet, but someday...)
In the particular example that you pose, I would argue that, while
'fprintf()' and 'write()' share some state, it ought to be possible to
specify separately the effect that each has on that shared state. If you
are absolutely set on a more operational style of specification, you will
probably be happier with a more operational methodology, such as VDM.
For a good, although informal, example of dealing with multiple IO
interfaces, I would direct you to SRC Report 53, "IO Streams: Abstract
Types, Real Programs," by Mark R. Brown and Greg Nelson, 1989. A revised
version is Chapter 6 of "Systems Programming with Modula-3," Greg Nelson
(ed.), Prentice Hall, 1991, ISBN 0-13-590464-1. The research report
version may be ordered by sending e-mail to src-report@pa.dec.com, or using
the URL
http://www.research.digital.com/SRC/publications/src-rr.html
Jim H.