🚀 go-pugleaf

Ralph Johnson's second reply to the question of the place of formal
specification was very interesting.

I'd like to add our group to his list of those who have written formal
specifications for "real" components.  Ralph, I'll send you a few
reports if you wish; just drop me a note.  I wish I could cite a bunch
of papers we've had published but few people seem to want to hear what
we're trying to say.  That's one of the reasons we think this
newsgroup is so important: at least the people here have not already
abandoned the idea that reusable software components might someday
become practical.  Nor are they convinced that they already know the
one-and-only way to do something.

That leads to Ralph's claim that one of the deficiencies in relating
formal specification, verification -- formal methods in general -- to
real programming is the difficulty of dealing with pointers.  How
true!!!  Again, all I can say is that we have done quite a bit of work
on this, but it generally falls on deaf ears.  Many people can't
imagine programming without pointers sticking out of everything, so
don't even bother suggesting that pointers spell trouble.  But this is
another important reason that formal specifications are important and
that you don't want to look at source code to try to understand a
component's behavior.  By making specifications abstract, one can
shield a client of a reusable component from all the pointer tricks
that often need to be played in the implementation in order to
implement it at all, and certainly to make it efficient.

I guess the bottom line is that Ralph might grant that, if certain
technical problems could be solved, there might be some hope for
substituting formal specifications for source code as descriptions of
component behavior.  Ralph, if I've misrepresented your position on
this, please advise.

	-Bruce