🚀 go-pugleaf

Ralph Johnson's recent comments about the differences between
specification and implementation call for a few more comments and
questions of clarification.

(1) Ralph gives an example of a simple implementation of stacks and
simple algebraic specification, and concludes:
  "The second (the "abstract" specification) is shorter, but not much
  easier to read.  Most importantly, it is not easier to understand.
  Thus, I claim it is no better as a specification than the first."

I'm not sure I understand the point of this example, except that it is
POSSIBLE for an implementation to be about as short and as simple as
its formal specification.  No argument there.  But the claim that the
algebraic specification is "THE abstract specification" is too strong.
There are other well-known specification methods that, we would both
apparently agree, render specifications easier to comprehend than the
algebraic approach.  Such specifications remain abstract but do not
rely on using equations, as in Ralph's example.  Such alternative
specification methods should result in easier-to-understand
specifications of stacks.

Admittedly these alternatives might look on the surface very much like
Ralph's source code (for this example but not in general).  But they
are subtly and importantly different in meaning precisely BECAUSE they
are abstract.  One might, for example, use a mathematical sequence as
a mathematical model of a stack.  But there would be no implication
that program sequences are used in the implementation, as apparently
Ralph has done in his code.  This is important for lots of reasons,
upon which I can elaborate if the discussion continues along this
line.

(2) Ralph continues:
  "Stacks are about the easiest component for which one can write a
  formal specification.  However, a better example to show the strengths
  of formal specifications would be sorting, since the specification is
  that the output sequence is a permutation of the input sequence and
  that the output sequence is sorted, while most fast sorting algorithms
  take a lot of more code to express.  This is an example of a problem
  for which there exists both fast complex algorithms and slow simple
  algorithms.  The specification I described corresponds to the sorting
  algorithm that takes each permutation and checks whether it is sorted.
  This simple specification could be represented just as well by a
  program."

The general claim here seems to be that for a reusable component with
a compact formal specification, there is also a simple but possibly
inefficient ALGORITHM that is its implementation and that, to some
people at least, would be easier to understand.  This seems unlikely
at best.  Consider a simple example.  Suppose you have a component
that keeps track of a function from some domain type D to some range
type R (both parameters to the component).  You want to specify a
boolean-valued operation that returns "true" given f and r iff
function f maps some value of type D to the specific value r.  This is
easy to specify in the abstract using an existential quantifier;
something like:

	there exists d:D such that f(d) = r

Presumably the source code to explain this behavior consists of a
program to search through all values of type D for one that f maps to
r.  Two problems here.  First, D may not be finite, in which case this
is not an algorithm at all because it may not terminate and could
never return "false".  Second, how do you write this program (except
in pseudocode or something) without knowing what type D is?

But Ralph has provided a good idea here: to challenge specification
writers to design and specify a component that permits one to do
sorting.  I'm happy to oblige, and will post such specs to this forum
if asked to do so.  But we should also be able to see the "simple
specification" mentioned in the last sentence above for comparison
purposes relative to ease of understanding.  A biased audience,
readers of this forum, but we might get some info nonetheless.

Of course, comparisons on other grounds (e.g., ease of verification
that alternative implementations meet the specs; whether the spec
method helps one design a good reusable component in the first place;
lots of other questions) might be too difficult to carry out in this
forum.  But it would be a start at seeing whether people might prefer
to see source code or formal specifications for their reusable
components.

	-Bruce

------

Prof. Bruce W. Weide
Dept. of Computer and Information Science
The Ohio State University
2036 Neil Ave. Mall
Columbus, Ohio  43210-1277
USA

Phone:   614-292-1517
E-mail:  weide@cis.ohio-state.edu