Path: utzoo!utgpu!news-server.csri.toronto.edu!rutgers!mcnc!duke!romeo!crm
From: crm@romeo.cs.duke.edu (Charlie Martin)
Newsgroups: comp.software-eng
Subject: Re: Reuse and Abstraction (was: reu
Message-ID: <19848@duke.cs.duke.edu>
Date: 28 May 90 16:40:22 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> <80903@tut.cis.ohio-state.edu>
Sender: news@duke.cs.duke.edu
Reply-To: crm@romeo.UUCP (Charlie Martin)
Organization: Duke University CS Dept.; Durham, NC
Lines: 124

Bruce Weide writes...

In article <19820@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes:
.
.>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.

Right, I'll buy that, at least provisionally.

.
.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.


I think you're more or less wrong here, or at least somewhat idealistic
about what modern computer langauges really are.  (Most) programming
languages don't fulfill your definition of formality, because they don't
generally have completely well-understood semantics.  C is an example;
there are all the usual puzzles, like 

	int a ;
	a = a++ ;

where we can't say exactly what the result would be without reference to
a particular compiler and operating system.  (Even then, on siome
systems the behavior is not defined except that a remains a valid int
value.)

Further, C has a number of special cases which are at the least not well
documented, such as when *(a+i) IS NOT equivalent to a[i].

You're right about my use of "we" above; in fact, I'd be suspicious that
most people who are working programmers are not really used to using
mathematics in any but a cookbook sense.  But I suspect that the only
exposure most people have to fully formal and well-founded languages is
when they take Euclidean geometry in high school.

.
.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.

It is afulyy hard sometimes to educate people to write a specification
that doesn't express their idea of how the software is to be designed.
I agree with you: computer scientists should educate themselves.


.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?
.

I think when I write a Gypsy spec, I'm doing what you call a
fully-formal specification; as an "engineer" my resistance to it is that
it seems to take a lot of effort to not get very far.  Part of the
reason for it is that you have to consider a lot of foundational issues
every time, I think.

.
.>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.

I guess the canonical academic way of handling this problem is to start
a journal; to make it "competetive" in the tenure-credit sense, I
imagine it would have to reduce publications to minimum publishable
units, (this may be a little cynical) so that pubklication-count is
high.

I dunno -- does anyone else have any idea hw to make software
publication compete with theory publication?


Charlie Martin (...!mcnc!duke!crm, crm@summanulla.mc.duke.edu)
O: NBSR/One University Place/Suite 250/Durham, NC  27707/919-490-1966
H: 13 Gorham Place/Durham, NC 27705/919-383-2256