Path: utzoo!attcan!uunet!snorkelwacker!tut.cis.ohio-state.edu!elephant.cis.ohio-state.edu!weide
From: weide@elephant.cis.ohio-state.edu (Bruce Weide)
Newsgroups: comp.software-eng
Subject: Re: Reuse and Abstraction (was: reu
Message-ID: <80903@tut.cis.ohio-state.edu>
Date: 25 May 90 21:09:39 GMT
References: <4979@stpstn.UUCP> <102100009@p.cs.uiuc.edu> <80449@tut.cis.ohio-state.edu> <19614@duke.cs.duke.edu> <80685@tut.cis.ohio-state.edu> <19760@duke.cs.duke.edu> <80884@tut.cis.ohio-state.edu> <19820@duke.cs.duke.edu>
Sender: news@tut.cis.ohio-state.edu
Reply-To: Bruce Weide <weide@cis.ohio-state.edu>
Organization: Ohio State University Computer and Information Science
Lines: 75

In article <19820@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes:

>One thing that might be worth a couple of beers and a bull-session
>sometime is to figure out what "formal" means.  I recently had the word
>"rigorous" suggested as an alternative; let's replace the word "formal"
>with "rigorous" for a few lines and see if it helps any.
>
>Then what I'm saying is that I think a rigorous notation can be used
>which presents many of the advantages of fully-formalized (machine
>processable, proof-checkable) specification languages.  Z and VDM seem
>like good approaches to this.

OK, here's an attempt at distinguishing "rigorous" from "formal" -- a
very useful distinction indeed, also suggested recently by Brad Cox.
First, a proposed definition of "verify": To prove by transformation
of symbols, with each step justified by a rule of logic or by explicit
assumption; the proof steps may or may not be generated mechanically,
but at least they must be subject to mechanical checking.

Now, a specification is "formal" if it:

(1) is written in a language with well-defined syntax and semantics;

(2) can be used to verify the correctness of a proposed implementation
of the specified component (i.e., a program in a formal programming
language); and

(3) can be used in a verification of the correctness of a proposed
client of the specified component.

A specification is "rigorous" if the proofs in (2) and (3) are not
verifications in the sense given above, but rather are arguments whose
correctness is subject to debate (and/or vote :-).


>One argument for these rigorous notations is that we are accustomed to
>rigorous but not fully formal notations in any case, because that is the
>way mathematics exposition is usually done...

I suppose Charlie is talking about "computer scientists" or "software
engineers" when he says "we."  In either case, I can't buy it.  On the
contrary, most of us are quite comfortable with fully formal
notations: programming languages.  What many computer scientists don't
seem to be comfortable with is mathematics.  Formal specifications
need be no more intimidating than programs.  It's just that they deal
with abstract mathematical concepts rather than bits and bytes.  And
given the general trend toward "high-level" programming languages in
which one is supposed to reason about computing with more "abstract"
things, this difference seems to be diminishing.

The other major difference between a specification and an
implementation, of course, is that the former says WHAT is computed,
while the latter says HOW it is computed.  Perhaps most computer
scientists (at present) are also a bit uncomfortable with things that
are not so procedural.  But I can't accept that this is an inherent
limitation of computer scientists.  Let's educate ourselves.
Furthermore, if this is the crux of the problem, formal specs can't be
substantially more difficult to deal with than informal (but rigorous)
ones.  In summary, then, what's the resistance to formal specification?


>Political problem:  Let's say I as a researcher determine that I want to
>build up a really good reusable non-trivial library.  I spend a year
>(maybe that little) developing the specs and implementing it.  Where do
>I publish?  How much tenure credit will I get for it?

Good point.  I wish I knew where to publish this stuff.  If you have
any suggestions let us know.  If I were so inclined and had a willing
venture capitalist lined up, I might be tempted to bypass the academic
routine and just start designing and implementing reusable components
and sell them.  But I don't think that's in the cards, so publishing
seems to be essential.

Cheers,
	-Bruce