From: bowen@prg.ox.ac.uk (Jonathan Bowen)
Newsgroups: comp.arch,comp.lang.misc,comp.software-eng,comp.specification
Subject: Specification v. design languages (was Re: Goals, Cost, and Flexibility)
Date: 15 Oct 92 09:03:26 GMT
Reply-To: Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen)
Organization: Programming Research Group, Oxford University, UK
Originator: bowen@topaz.comlab

In article <Bw4MuE.8GL@exnet.co.uk> dhd@exnet.co.uk (Damon) writes:
>In article <1992Oct14.040754.14470@CS.ORST.EDU>
> crowl@jade.CS.ORST.EDU (Lawrence Crowl) writes:
>>
>>Overloading is _not_ ambiguity.  Overloading in one manner in which a
>>context-free language becomes a context-sensitive language.  My point
>>is that in a (good) programming language, constructs have a clearly
>>defined meaning, and are unambiguous.  Programming languages can handle
>>overloading unambiguously because they have formal rules for
>>interpreting context.  Mathematical notation has no formal rules for
>>resolving ambiguity.  Formal languages are a necessity in programming,
>>but are not in mathematics.
>>
>>Please note, I am _not_ saying mathematical notation is flawed for the
>>purposes of math.  Mathematical notation has been serving the needs of
>>mathematitions for decades.  I am saying that mathematical notation, as
>>it is defined now, is too informal to serve as a programming language.
>
>Which is why (I may be starting a new thread here, or have missed
>something earlier), Z is not much good as a *specification* language
>since it just uses any mathematical construct you care to employ.

But Z was devised as a formal specification language and has been used
very successfully as such in a number of real developments, the most
notable of which is the IBM CICS project. It has a formal syntax and
semantics (although the standard is still at the draft stage) - it can
perhaps be thought of as formalised mathematics (in the area of typed
set theory and first order predicate calculus) if that is not too
glib.

>SML, on the other hand, even though it is not completely characterised,
>is much nearer the mark and can actually execute too.  Quite quickly in
>fact, since what optimisations are permissible can be worked out...

Yes, SML is great for prototyping, and may be fast enough in practice
as well for some applications. But it is executable (you have to think
about *how* it is going to run, not just *what* you want to do), so it
is not ideal for specification. And non-deterministic specifications
which allow the designer freedom of choice in certain aspects of the
design which need not be fixed at the specification stage are of course
impossible.

>CCS is a great spec language for concurrency.  Might make a good
>parallel asm language.

CCS (and CSP) are great *design* languages if you are targeting
your implementation onto a parallel system. You may also want to
think about the system at a more abstract level (e.g., at the
requirements stage).

>In fact I've done CCS -> SML -> C, but actually demoed the SML in
>real-time for a network router.

Great! I'd be interested to hear about the mapping from CCS to SML.
Can this (was this) undertaken in a rigorous and systematic manner?

-- 

--
Jonathan Bowen, <Jonathan.Bowen@comlab.ox.ac.uk>
Oxford University Computing Laboratory.
Newsgroups: comp.arch