🚀 go-pugleaf

In article <BLK.90Oct25142230@vanity.mitre.org>, blk@mitre.org (Brian L. Kahn) writes:
> 
> For some time, I've puzzled over the difference (if any) between a
> specification language and a programming language.  The best I can
> come up with is that a spec has less information about data structures
> and/or algorithms than is usually found in code.  ...

That's close, except it doesn't go far enough: a spec may have *no* 
information about data structures and/or algorithms --- and that's good!

It is possible to overemphasize the similarity of specification notations and
executable programming languages.  They are really intended for expressing
different kinds of things.  There is much value in orienting some notations
toward compactness and expressive power rather than executability.

The usefulness of non-executable notations is clear even for quite
prosaic applications; it isn't necessary to get into abstruse (to me) issues
like non-determinism and quantification over infinite domains.  Here is a 
simple example that arises in the specification of the control software for our
medical cyclotron:

The control system includes over 100 analog quantities that represent
things like magnet currents and vacuum pressures.  For each quantity there
is a function called cnv_in_ex ("convert internal to external"), which 
converts from the internal machine representation (essentially, the pattern of
bits on the A to D converter) to the displayed value of the quantity in units
meaningful to the users (amps, millibars...).  Some of these functions are
simple, like a*x + b, others are more complex involving logs and whatnot,
still others are defined as lookup (with interpolation) into empirically 
measured calibration tables.  So, for each quantity the specification 
contains something like:

	cnv_in_ex(x) = ... some formula ...

(Note that there is a *different* cnv_in_ex for each quantity.  The various
notations provide ways to express that).

It's easy to envision a system that would compile all these into
executable code.  But, we also need a bunch of functions cnv_ex_in ("convert
external to internal") that perform the conversion in the other direction.
We just say that for all quantities, cnv_ex_in is the inverse of cnv_in_ex.
In particular notations, you might write this:

	cnv_ex_in(cnv_in_ex(x)) = x

...or this:
                             -1
	cnv_ex_in = cnv_in_ex 

... or something else. This is obviously simpler and more compact than 
presenting over a hundred different formulae that say (y - b)/a etc.  More to
the point, it clearly expresses exactly what we want to convey.  A reader 
might not immediately see that (y - b)/a was used because it is the inverse
of a*x + b, and it gets much harder with the more complex formulae.

Sure, it's possible to envision a very complex compiler that has a bunch of 
rules that tell it how to generate a function which is the inverse of some 
other function.  However, that is not a practical or useful option.  If that 
compiler is going to do a decent job, you 
are going to have to provide it with some additional information about 
what the first function is and maybe even how it is implemented, and when you 
are specifying you don't want to worry about that, maybe you don't even know 
it yet.

- Jon Jacky, University of Washington, Seattle  jon@gaffer.rad.washington.edu