mjl@cs.rit.edu (03/04/90)
So where are the articles in this newsgroup? I saw the creation message
come through awhile back, but so far we've received no 'real' articles
here at RIT. What gives?
Just in case everyone was waiting for someone else to get the ball
rolling, I'll expose my ignorance by asking a couple of questions
w.r.t. formal specifications. I'd really appreciate a thoughtful
answer, even if its "your looking at the wrong specification system --
try xxx." For reference, the two systems I'm most familiar with (not
to say I'm an expert) are VDM and Z.
1. In specifying the data types, invariants, and operations in a card game,
I've run into a snag trying to specify the "shuffle" operation.
Intuitively, I (think) I want to say the shuffled deck is a permutation
of the original deck, but that the permutation has certain statistical
properties. Actually, these properties only manifest themselves over
many shuffles, as any given permutation is a possible outcome for a
given shuffle. How can I do this without defining all of probability
theory from first principles? If I simply say I want a permutation,
an implementor could maliciously or ignorantly perform the identity
operation -- or something real crude like a "rotate by 1" function.
As in all specifications, I don't want to detail the algorithm, just
the effect.
- current solution: the desired statistical properties are
- given as comments in a rigorous
- mathematical style.
2. How do I specify "interruptible" operations. For instance, we have a
"paint" program that can take a long time to fill a region, so by
pushing a mouse button I can terminate it (leaving the region partially
filled). Other examples are ATTN signals to discard unexpectedly
voluminous output while remaining in the application. Can this type
of effect by specified in VDM, Z, or similar notation? Do I have to
resort to Petri nets or the like -- and if so, how to I connect this
all to my functional specification?
- current solution: NONE
3. How can I model the effects of expected hardware failure? For instance,
how can I specify something like a commit protocol for database transactions
so that the essence of this technique in recovery from hardware failure
shows through?
- current solution: NONE
4. How can I specify an open-ended system? For instance, I'm working on
a project to automate software installation. The installation
system manages the high-level details, but the actual effects of
installation vary from package to package, so they are left as
abstract or virtual operations. How can I reason about such a
system?
- current solution: I define what is expected of a package
- installation "loosely" -- i.e., in
- English I say "don't corrupt the password
- file"
I think all of these are quite precise; they don't get into qualitative
areas like "user-friendliness." Any suggestions or help appreciated.
Mike Lutz
Rochester Institute of Technology
Mike Lutz Rochester Institute of Technology, Rochester NY
UUCP: {rutgers,cornell}!rochester!rit!mjl
INTERNET: mjl@csrit.edu