NetNews Usenet Archive 1992 #27/NN_1992_27.iso/spool/comp/specific/547

Internet Message Format | 1992-11-22 | 5.6 KB

Path: sparky!uunet!mcsun!uknet!pavo.csi.cam.ac.uk!jg
From: [e-mail] (Jim Grundy)
Newsgroups: comp.specification
Subject: Impossible Specs (was: Algebra and Semantic definition)
Keywords: structural operational semantics, denotational semantics
Message-ID: <[e-mail]>
Date: 23 Nov 92 09:26:37 GMT
References: <[e-mail]> <[e-mail]> <[e-mail]> <[e-mail]>
Sender: [e-mail] (USENET news)
Reply-To: [e-mail]
Organization: Cambridge Hardware Verification Group
Lines: 86
Nntp-Posting-Host: razorbill.cl.cam.ac.uk

In article <[e-mail]>, [e-mail] (victor yodaiken) writes:
|> In article <[e-mail]> [e-mail] (William F Ogden) writes:
|> >In article <[e-mail]> [e-mail] (victor yodaiken) writes:
|> >   ...
|> >>In any event, I've never been able to understand the virtue of working
|> >>within a mathematical model of computation which permits description of
|> >>processes that cannot be carried out, even in principle, by any physical
|> >>computing device. What is it that one intends to learn by application of
|> >>these methods?
|> >
|> >If you look at recursion theory, you'll find that it has developed some
|> >rather interesting results about degrees of unsolvability by just such an
|> >approach.
|>
|> You've misunderstood my point, perhaps I relied too much on the context.
|> I was responding to a post which argued that first order equational logic
|> was too restricted to allow description of programs. So, I assumed that
|> we were discussing the subject of the specification and verification of
|> computer programs and devices. In this field, it seems inexplicable to
|> demand, on grounds of generality, that one permit description of physically
|> impossible computations.

I'd like to have a go at advocating specification languages that describe
impossible tasks for you.

I would begin by agreeing that there is little or no point in insisting
for the sake of generality on specification langauges that can permit
impossible specifications (miracles).    However, I believe it is the case
that it is not worth taking a simple and elegant specification langauge
and explicityly removing a class of specifications from it - this tends
to make it a lot more complex.

A good specification langauge tends to have a pretty mathematical structure,
this makes it easy to reason about specifications framed in the language.
It is common, for example, for specifications to form a lattice structure
whith chaos (the specification that is trivial to meet) at the botom,
and miracle (the specification that is impossible to meet) at the top.
Now while I don't advoctate pretty mathematical structures for their own
sake, when I find that what I want to work with has a nice stucture then
I consider that to be good evidence that my intuitions are on the right track.

The presence of miracles in a specification language was not something
that people noticed as advantagous when specifications were done for
specification sake - or even I think when people verified completed programs
against specification.   It is something that people noticed as advantageous
when they began investigating techniques for refining specifications into
programs.
Dijkstra's guarded command langauge (GCL) is popular with exponents of
program refinement.   When Dijkstra first described this langauge he
explicity banned impossible specifications - this was called the law of
the excluded miracle.   Later when people started refining specifications
into programs they found that this law got in their way.   The simple
thing to do was remove the law.   The GCL and its weakest precondition (wp)
semantics are an example of a pretty structure that had an explicit
kink made it in - remove the kink and it worked even better.
For example, the GCL contains nondeterministic conditional and looping
constructs.   When considered as a whole these constructs are nonmiraculous.
However, the invdividual componentes of one these constructs may represent
impossible specifications when considered on their own.   It is nice,
therefore, to have a formalisation that allows us to examine these components
on their own.

I understand that the presence of miracles also has application to data
refinement, but I don't really know anything about this.

A nice analogy, I think made by Carrol Morgan, this that miracles in
a specification langauge are a bit like imaginary numbers in mathematics.
Nethier of them exist - but they both make life a lot easier.
You probably don't want them in your specification or your implementation,
but they can make the process of reasoning about things more simple.

As a final example, consider English as a specification langauge.
Imagine what a mess Engligh would be (I know its a mess now to) if all the
ways to describing impossible behaviour were not valid English.

Jim

===============================================================================
Jim Grundy
University of Cambridge | Phone: [phone]            | This space has
Computer Laboratory     | Fax:   [phone]            | been intentionally
New Museums Site        | Telex: CAMSPLG 81240             | left blank for
Pembroke Street         | email: [e-mail]           | formatting
Cambridge  CB2 3QG      |                                  | purposes.
UNITED KINGDOM          |                                  |
===============================================================================