🚀 go-pugleaf

I recently suggested an operation that I claimed could be more easily
specified abstractly than by giving source code for an implementation:
 ">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?"

John Hogg has subsequently suggested that I claimed that the
specification "was unimplementable."  Sorry for the confusion; this is
not what I meant to imply.  It is quite implementable.  It's just that
the "obvious," and therefore presumably easy-to-understand
implementation that would make the "source code specification" of
behavior simple, is not in fact a correct implementation.

John goes on to say:
 "This isn't quite fair, because he's given a specification of a
  component or function g without specifying the function f that it
  uses.  If f is specified, then we can enumerate through the range
  of g ({true, false}) in quite acceptable time.  The specification of f is
  executed in the same manner."

Perhaps I wasn't being clear enough, or I don't understand John's
point.  The reusable component I have in mind provides a type whose
ABSTRACT MATHEMATICAL MODEL is a function from D to R; let's call it
type "foo" so we don't confuse it with a program function.  The
component also provides operations that permit the client to construct
a foo, and also provides an operation that asks the question above:
for the foo variable f (which has been constructed in this way), does
any value of its domain map to r?  The specified doesn't know what
mathematical function models f.  All he/she knows about f is that it
has been constructed by the client using the operations provided by
the component to operate on variables of type foo.  The fact that the
abstract specification of this component may talk about f as though it
were a mathematical function is what makes the abstract specifications
simple.  That source code doesn't have this abstract view of f is
what, I claim, will make writing "source code specifications" more
difficult and make them harder to understand.  (Not impossible, just
clumsier.)

Overall I agree with most of John's points, and in particular with his
view of what verification is all about and what properties it should
have (modularity, soundness, etc.).  This is another reason for having
abstract specifications.  If one wishes to reason about the
correctness of programs -- whether they meet their specifications --
one should probably draw on the ready supply of techniques, notations,
and concepts of mathematical logic to do this reasoning.  Having
abstract specifications, for both the component being implemented and
the components its implementation uses, seems to support this approach
directly.  Reasoning about the relationships among concrete
implementations of components would seem, by comparison, to be more
likely to cause problems when issues of soundness, relative
completeness, etc., are considered.  Again, I'm not claiming that it
would be impossible to do it that way, just that the abstract approach
seems more promising from here because it "reuses" what mathematicians
have already done.

	-Bruce