weide@elephant.cis.ohio-state.edu (Bruce Weide) (05/25/90)
Thanks to Charlie Martin for his interesting posting about formal specification. Among other things, he writes: >My suspicion (today, ask me again in a couple weeks, because I may >change my mind again) is that one of the major advantages of Z and VDM >is that they are *not* tied to an implementation language, and are not >intended to be compiled. Because of this, one can invent terminology >and new notation on the fly, one can leave out essentially uninteresting >parts of the specification (like restating over and over again that a >particular operation works within the bounds of the type's >architecture-specific values), and in general one can play to the >audience instead of needing to satisfy a finicky proof-checker. One of the primary reasons for formal specification is the inherent ambiguity of natural language and other informal methods. It's hard to see how having a "formal" notation that can be augmented "on the fly" -- whenever the specifier feels a need to say something that the language wasn't designed for -- can be much better than an informal specification in this sense. Maybe a little better, but hardly the ultimate formal specification language. I think it is a reasonable academic exercise to explore the constructs and concepts needed to develop a more complete (in this sense) specification language than those offered to date. Eventually, a better language might even get used in practice. Charlie also argues: >Actually, it's pretty hard to show a library of reusable components that >are generally agreed to be reusable, and non-trivial. Maybe InterViews. >But I think we may be instanciating "easy" differently: what I mean is >"there are no technical difficulties (that I can see), so it should just >be a matter of applying some time and effort to doing so." It s an >interesting sort of task, but it's one that academic types are not >attracted to because a formal specification of a basically uninteresting >library isn't going to make a good publication, and one which industrial >types aren't likely to try unless soemone comes up with the money. Actually, there are some academic types (e.g., me) who don't think the exercise is so trivial, and who don't believe that there are "no technical difficulties" in developing a well-designed library of reusable components. Even things like stacks, lists, associate search structures, graphs, etc., ar NOT designed properly for reuse as they appear in the CS textbooks or in existing component libraries. In fact, though, judging from personal experience, Charlie is right if he is suggesting it is hard to convince many people of this. People don't really want to know WHY it's hard to "get it right", nor do they want to consider alternative designs even if they come with (so far, at least) an irrefutable rationale. This means it IS difficult to publish new designs for things people believe they already understand, and almost as difficult to find industrial funding. We hope, however, it does not turn out to be impossible :-). -Bruce
crm@romeo.cs.duke.edu (Charlie Martin) (05/26/90)
In article <80884@tut.cis.ohio-state.edu> Bruce Weide <weide@cis.ohio-state.edu> writes: > >Thanks to Charlie Martin for his interesting posting about formal >specification. Among other things, he writes: > Be careful -- it's hard enough for people who *don't* like what I'm saying to shut me up.... >>.... is that one of the major advantages of Z and VDM >>is that they are *not* tied to an implementation language, and are not >>intended to be compiled. Because of this, one can invent terminology >>and new notation on the fly, one can leave out essentially uninteresting >>parts of the specification .... > >One of the primary reasons for formal specification is the inherent >ambiguity of natural language and other informal methods. It's hard >to see how having a "formal" notation that can be augmented "on the >fly" -- whenever the specifier feels a need to say something that the >language wasn't designed for -- can be much better than an informal >specification in this sense. Maybe a little better, but hardly the >ultimate formal specification language. .... 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. 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. One hardly ever is forced back to considering foundational things (Peano axioms, cardinality of the reals) in doing day to day engineering mathematics. In fact, engineering mathematics often ignores things on a much higher level than these, like whether or not a function is continuous: we just know that most functions in, say, mechanical engineering are continuous. Thus an argument for an engineer will not state certain things that are part of the culture. And engineering math will sometimes use manipulations that are "good enough" but which will not hold if the implicit assumptions are violated. Of course, sometimes this bites a mechanical engineer or an architectural engineer as well. (One could argue that this kind of mistake was what brought done the Kansas City Flyway: on one side, the designer didn't know that it was hard to put a thread and nut in the MIDDLE of a long unthreaded rod; on the other, the people building it didn't realize that resolving this by making the one rod into two rods with a shear between them wouldn't be structurally sound.) > >Charlie also argues: > >>Actually, it's pretty hard to show a library of reusable components that >>are generally agreed to be reusable, and non-trivial. Maybe InterViews. >>But I think we may be instanciating "easy" differently: what I mean is >>"there are no technical difficulties (that I can see), so it should just >>be a matter of applying some time and effort to doing so." It s an >>interesting sort of task, but it's one that academic types are not >>attracted to because a formal specification of a basically uninteresting >>library isn't going to make a good publication, and one which industrial >>types aren't likely to try unless soemone comes up with the money. > >Actually, there are some academic types (e.g., me) who don't think the >exercise is so trivial, and who don't believe that there are "no >technical difficulties" in developing a well-designed library of >reusable components. Even things like stacks, lists, associate search >structures, graphs, etc., ar NOT designed properly for reuse as they >appear in the CS textbooks or in existing component libraries. I think I was clumsily trying to get at the same point: there are not many examples because it's hard to come up with a good library of reusable components. However, I think that if you can propose the collection of operations etc that go with such a library, then "rigorous" specification (avoiding the nasty word again) of the operations is not so big a problem. But there is a more significant, essentially political, problem (at least in my opinion), and another significant technical problem that I'm actually running into in my dissertation (so any suggestions will be welcome, BEELIEVE YOU ME!) 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? My view is a little parochial, since the only department I've ever been closely associated with is Duke's. But I can tell you that from here it looks like academics are rewarded for theorems, not for programs; theorems can be made into publications very quickly, and therer are many many journals that like to see them. Programs, even with good specifications, take a long time to implement and try out after you've had the idea and worked it out. Then papers on them are acceptable at (it seems to me) many fewer places. The result is that at Duke, it is very much harder for systems people to get tenure. What I hear suggests that this is true elsewhere, perhaps nearly everywhere. I'd love to hear that it is different; I'd even more like to see good evidence that it is different, as someday *I* will be trying to get tenure, I hope. on to the Technical Problem: once you have a library of components that you claim are reusable, how can you demonstrate scientifically that they are more reusable or better for reuse than anyone else's components? What is your measure of "reusability"? > we hope, however, that >it does not turn out to be impossible :-). I'm with you there, brother. 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
weide@elephant.cis.ohio-state.edu (Bruce Weide) (05/26/90)
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
cox@stpstn.UUCP (Brad Cox) (05/27/90)
In article <80884@tut.cis.ohio-state.edu> Bruce Weide <weide@cis.ohio-state.edu> writes: >One of the primary reasons for formal specification is the inherent >ambiguity of natural language and other informal methods. My own notions of specification/testing are based on the premise that, when non-ambiguity really *matters* (such as during a commercial transaction), mankind goes through a stereotypical, common-sense, and in principle automatable process whose effect is to remove the ambiguity of natural language. For example, in the commercial transaction signified by the requirement, "I want to buy a pound of ten-penny nails", or "I want to buy a Set class", ambiguity of terms like "pound", "ten-penny", "nail", "Set", and "class" are eliminated by developing a *common vocabulary* of *tests* that both parties, producer and consumer, can agree on as determining the meaning of these terms. For example, "pound" is defined by a test procedure involving a scale, and "ten-penny" by a test procedure involving shape recognition by the natural senses. Since test procedures based on scales and shape recognition fail to help with intangible concepts like "Set", we must become ultra-diligent in developing and *publishing* test procedures to detect each of the terms involved in specifying software components, to create the very *basis* for non-ambiguous producer/consumer dialog. Then, with a sufficiently large, robust, and widely-accepted library of such test procedures, we can take the next step of building a specification/testing *language* that can compose meaningful sentences, i.e. *specifications* from these primitive terms, and then compile these sentences to build go/nogo gauges that can determine whether a putative implementation is in fact an actual implementation of that specification. >Charlie also argues: >>Actually, it's pretty hard to show a library of reusable components that >>are generally agreed to be reusable, and non-trivial. The Smalltalk environment is one; the Objective-C System-building Environment is another. >> It s an >>interesting sort of task, but it's one that academic types are not >>attracted to because a formal specification of a basically uninteresting >>library isn't going to make a good publication, and one which industrial >>types aren't likely to try unless soemone comes up with the money. Re: academic types, please see Ralph London's formal specification (in Z, as I recall) of the Smalltalk Set class. Re: industrial types, please note my previous transmissions about Stepstone's use of specification/testing for all of our Software-IC products. We do not view this as an academic matter, but a matter right at the heart of our business. How will a robust commercial marketplace in fine-granularity software components even be *thinkable* unless producers and consumers can develop a way of agreeing on what is to be bought and sold? >Actually, there are some academic types (e.g., me) who don't think the >exercise is so trivial, and who don't believe that there are "no >technical difficulties" in developing a well-designed library of >reusable components. Even things like stacks, lists, associate search >structures, graphs, etc., ar NOT designed properly for reuse as they >appear in the CS textbooks or in existing component libraries. In >fact, though, judging from personal experience, Charlie is right if he >is suggesting it is hard to convince many people of this. People >don't really want to know WHY it's hard to "get it right", nor do they >want to consider alternative designs even if they come with (so far, >at least) an irrefutable rationale. This means it IS difficult to >publish new designs for things people believe they already understand, >and almost as difficult to find industrial funding. We hope, however, >it does not turn out to be impossible :-). To be somewhat more controversial here, the academic priesthood is highly unlikely to make great contributions precisely *because* they're conditioned to believe that only technical problems are significant. They focus on the *weapons* (i.e. OO technology), and neglect the *war* (software industrial revolution). Please take it from one who *knows*, the costs of building commercially robust components are *not* in getting the code running. There is at least a ten-fold greater cost in getting them tested and documented, and another ten-fold increment in sales/marketing. Both of these latter steps (100 fold) are unrelated to *implementation*, and closely related to *specification*. -- Brad Cox; cox@stepstone.com; CI$ 71230,647; 203 426 1875 The Stepstone Corporation; 75 Glen Road; Sandy Hook CT 06482
cox@stpstn.UUCP (Brad Cox) (05/27/90)
In article <80903@tut.cis.ohio-state.edu> Bruce Weide <weide@cis.ohio-state.edu> writes: >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. Thomas Kuhn's 'The Structure of Scientific Revolutions' should answer your question. The academic priesthood is deeply vested in the cottage industry approach. What you're proposing is a paradigm shift (Kuhn's term) or a software industrial revolution (mine). Although revolutionaries may (or may not) win in the end, the priesthood will hardly make it easy for you to gore their sacred cows. Re: concrete suggestions for how to publish such stuff, may I suggest that commercial enterprises like Stepstone, ParcPlace Systems, and Digitalk are in fact vehicles for publishing reusable code. Of course, the 'only' benefits we'd offer would be hard, cold cash, not academic benedictions like tenure. -- Brad Cox; cox@stepstone.com; CI$ 71230,647; 203 426 1875 The Stepstone Corporation; 75 Glen Road; Sandy Hook CT 06482
crm@romeo.cs.duke.edu (Charlie Martin) (05/28/90)
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-2256crm@romeo.cs.duke.edu (Charlie Martin) (05/29/90)
In article <5122@stpstn.UUCP cox@stpstn.UUCP (Brad Cox) writes:
ambiguity [is eliminated]...
by developing a *common vocabulary* of *tests* that both parties,
producer and consumer, can agree on as determining the meaning of these
terms. For example, "pound" is defined by a test procedure involving a scale,
and "ten-penny" by a test procedure involving shape recognition by the
natural senses.
I rather like this idea, in general. It also fits in with the problems
of describing "formally" what meeting a requirement means. But I've got
some questions about its application....
Since test procedures based on scales and shape recognition fail to help
with intangible concepts like "Set", we must become ultra-diligent in
developing and *publishing* test procedures to detect each of the terms
involved in specifying software components, to create the very *basis*
for non-ambiguous producer/consumer dialog.
Then, with a sufficiently large, robust, and widely-accepted library of
such test procedures, we can take the next step of building a
specification/testing *language* that can compose meaningful sentences,
i.e. *specifications* from these primitive terms, and then compile these
sentences to build go/nogo gauges that can determine whether a putative
implementation is in fact an actual implementation of that specification.
Charlie also argues:
Actually, it's pretty hard to show a library of reusable components that
are generally agreed to be reusable, and non-trivial.
The Smalltalk environment is one; the Objective-C System-building Environment
is another.
No question that these are more reusable than many other possibilities,
but both of these (and most others, certainly all others of which I'm
aware) make a further implicit constraint on the systems that can be
built with them: they require that the systems be realized with only
components from a particular "catalogue". This is a problem that occurs
over and over again with reuse by composition from a collection of spare
parts: you can't merge parts from two catalogues. Thus if one company's
catalogue doesn't have what is needed, you have no other options.
This isn't necessarily a bad thing from a commercial standpoint, and it
certainly isn't part of the usual company's reward structure to build
stuff that makes it easy to include competitors products. But it does
mean that one buys into a raft of new problems as soon as one gets into
reuse of commercial components.
Also, my experience with both Smalltalk and Objective-C (admittedly
limited) has been that to use the libraries of classes available, one
had to buy into a lot of architectural assumptions that might or moght
not fit what was needed, e.g., garbage-collection or interpretive codes.
(At a little higher level, things like model-view-controller.) To use
any other architectural assumption meant backing up and rebuilding the
universe from primitives.
It s an
interesting sort of task, but it's one that academic types are not
attracted to because a formal specification of a basically uninteresting
library isn't going to make a good publication, and one which industrial
types aren't likely to try unless soemone comes up with the money.
Re: academic types, please see Ralph London's formal specification (in Z,
as I recall) of the Smalltalk Set class.
The Oxford people are an interesting case, because (for reasons I don't
completely understand) you apparently get some sort of rewards for doing
things that wouldn't be considered quite "research" over here. Perhaps
because if Tony Hoare and Robin Milner say it's good enough, no one
would dare to object. Or perhaps it has to do with the Oxford name on
the box.
In any case, this is good stuff. There ought to be more of it. Why
isn't there? Noting that there is one example doesn't make much of a
case for it being a hot research area.
Re: industrial types, please note my previous transmissions about Stepstone's
use of specification/testing for all of our Software-IC products. We do not
view this as an academic matter, but a matter right at the heart of our
business. How will a robust commercial marketplace in fine-granularity
software components even be *thinkable* unless producers and consumers
can develop a way of agreeing on what is to be bought and sold?
I'm with you here, and I'm looking forward to seeing the paper you've
mentioned. Another part of this is the apparent insensitivity of the
marketplace to issues of quality: you can't sell more correct, but you
can sell faster or earlier availability. (Even Stepstone is selling
rapid prototyping not correct codes.)
Actually, there are some academic types (e.g., me) who don't think the
exercise is so trivial, and who don't believe that there are "no
technical difficulties" in developing a well-designed library of
reusable components. Even things like stacks, lists, associate search
structures, graphs, etc., ar NOT designed properly for reuse as they
appear in the CS textbooks or in existing component libraries. In
fact, though, judging from personal experience, Charlie is right if he
is suggesting it is hard to convince many people of this. People
don't really want to know WHY it's hard to "get it right", nor do they
want to consider alternative designs even if they come with (so far,
at least) an irrefutable rationale. This means it IS difficult to
publish new designs for things people believe they already understand,
and almost as difficult to find industrial funding. We hope, however,
it does not turn out to be impossible :-).
To be somewhat more controversial here, the academic priesthood is highly
unlikely to make great contributions precisely *because* they're conditioned
to believe that only technical problems are significant. They focus on the
*weapons* (i.e. OO technology), and neglect the *war* (software industrial
revolution).
Please take it from one who *knows*, the costs of building commercially
robust components are *not* in getting the code running. There is at
least a ten-fold greater cost in getting them tested and documented, and
another ten-fold increment in sales/marketing. Both of these latter steps
(100 fold) are unrelated to *implementation*, and closely related to
*specification*.
Since I'm at an academic site, I think I need to throw in the obligatory
complaint about the implication that we at academic sites don't *know*.
Don't fall for that, lots of us at .edu sites have done substantial
real-world work.
But let's continue the war analogy a little further. Outside of a few
special cases (the British vs the Zulu, say) neither the weapons nor the
desirability of the goal has really affected the way the war came out.
What does seem to make a difference is the right tactics.
So far, we seem to be agreeing that the right tactics are more "formal"
or rigorous in some sense. What I wish we could do is measure the
effect of those tactics.
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-2256djs@minster.york.ac.uk (05/29/90)
In article <80884@tut.cis.ohio-state.edu> Bruce Weide <weide@cis.ohio-state.edu> writes: > >> ... Because of this, one can invent terminology >>and new notation on the fly, one can leave out essentially uninteresting >>parts of the specification (like restating over and over again that a >>particular operation works within the bounds of the type's >>architecture-specific values), and in general one can play to the >>audience instead of needing to satisfy a finicky proof-checker. > >One of the primary reasons for formal specification is the inherent >ambiguity of natural language and other informal methods. It's hard >to see how having a "formal" notation that can be augmented "on the >fly" -- whenever the specifier feels a need to say something that the >language wasn't designed for -- can be much better than an informal >specification in this sense. Augmenting formal specification languages `on the fly' is not necessarily incorrect. As long as the extensions are understood, and the effect on the supporting theory are not inconsistent, then augmentations provide a mechanism for tailoring the language to your own development environment. No single formal specification language is going to be expressive enough to ensure applicability to current problems and future ones as well. It could be argued that providing an easily extensible language is the only solution to the `learn-language - evolving-problem - learn new language' cycle. I believe that a RISC approach to specification languages is the way forward. A core of powerful primitive concepts embedded in a flexible syntax is much more useful than a `fat' specification language that tries to freeze all possible solutions in a single complex syntax. Certainly `on the fly' is an emotive phrase (hacking springs to mind..), `extensible theory' seems more appropriate. Dave Scholefield UUCP ..!mcsun!ukc!minster!djs Computer Science Dept. Internet djs%minster.york.ac.uk@nfsnet-relay.ac.uk University Of York York. YO1 5DD UK.
cox@stpstn.UUCP (Brad Cox) (05/31/90)
In article <19855@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes: > The Smalltalk environment is one; the Objective-C System-building Environment > is another. >... These >require that the systems be realized with only >components from a particular "catalogue". This is a problem that occurs >over and over again with reuse by composition from a collection of spare >parts: you can't merge parts from two catalogues. Thus if one company's >catalogue doesn't have what is needed, you have no other options. The IEEE article argues that we should begin thinking of object-oriented (and older) technologies, not as fancier ways of building things from scratch, but modularity/binding technologies. And just as other domains have become quite adept at deploying diverse modularity/binding technologies in common (i.e. sheep herding, shearing, spinning, weaving, sewing, zippers/buttons/bows can all be viewed as modularity/binding technologies at different, but thoroughly compatible levels), we need to stop viewing each technology as a panacea (i.e. Ada vs Smalltalk, or Objective-C vs C++), but as a tool relevant to a specific level of the software producer/consumer hierarchy, and usually irrelevant at others. For example, the fact that C++ provides outstanding gate/block-level integration facilities is relevant to those whose work demands a better C, and irrelevant to those whose work demands a chip-level (Software-IC) modularity/binding technology. In other words, think of Objective-C, not as a *language*, but an environment that supports a modularity/binding technology analogous to socketed pluggable hardware ICs. There are many ways of building chips that can plug into these sockets, and many vendors who are doing so (many of whose work has been bought repackaged, and is now being distributed by Stepstone). But as long as the components abide by the socket standard, they do not need not be built via Objective-C. They can be built in plain C, or C++, or even Cobol, and Objective-C components can be used via any of these. Its only a matter of abiding by the low-level socket standard...which brings me right back to where we started, the need for specification/testing languages capable of describing, and then verifying compliance to, these standards. >Also, my experience with both Smalltalk and Objective-C (admittedly >limited) has been that to use the libraries of classes available, one >had to buy into a lot of architectural assumptions that might or moght >not fit what was needed, e.g., garbage-collection or interpretive codes. >(At a little higher level, things like model-view-controller.) To use >any other architectural assumption meant backing up and rebuilding the >universe from primitives. Software's abstract/concrete hybrid nature is simultaneously our curse, and our blessing (in that it guarantees us higher salaries than those who work in more concrete domains, like flipping burgers). But apart from this fundamental difference, I'd argue that other domains experience exactly the same kind of complications, but have grown thoroughly adept at mastering them. For example, you might want to take advantage of a hardware store's new inventory in copper plumbing pipes, but in a house with existing iron pipes, you'd face corrosion problems; a preexisting architectural decision. But somehow mature industries like plumbing always seem to provide a way of getting around incompatible architectures; i.e. by selling an suitable adaptor. I grant you, we're far more immature an industry than plumbers, and off-the-shelf adaptors are still rare and raise cultural objections, such as thinking of such adaptors as kludges. > Re: academic types, please see Ralph London's formal specification (in Z, > as I recall) of the Smalltalk Set class. > >The Oxford people are an interesting case, because (for reasons I don't >completely understand) you apparently get some sort of rewards for doing >things that wouldn't be considered quite "research" over here. Perhaps >because if Tony Hoare and Robin Milner say it's good enough, no one >would dare to object. Or perhaps it has to do with the Oxford name on >the box. I get your point re: Oxford, but Ralph London is an American thru and thru. Works at Tektronix Labs, I think in Beaverton. Wish I had a reference to his article to give you, but it was beautiful work, and insightful into the difficulty of applying a mathematical approach to well-understood piece of concrete engineering effort. >In any case, this is good stuff. There ought to be more of it. Why >isn't there? Noting that there is one example doesn't make much of a >case for it being a hot research area. Because during any major paradigm shift, the conservatives *radically* outnumber the revolutionaries. That is why the market for a better C is so much larger than the market for off-the-shelf software components. That's why the market for traditional academic topics is so much larger than the market for what we're discussing. In choosing sides for yourself, be sure to keep priorities straight...believe me, the revolutionary life is not all that it's cracked up to be. >I'm with you here, and I'm looking forward to seeing the paper you've >mentioned. Another part of this is the apparent insensitivity of the >marketplace to issues of quality: you can't sell more correct, but you >can sell faster or earlier availability. (Even Stepstone is selling >rapid prototyping not correct codes.) Without disagreeing with you one bit that quality costs money that the market can be reluctant to pay, be aware that although Stepstone's code started out as rapid prototypes (like any other code), after seven years of improving it is considerably better than that. The same is true of Smalltalk, except they've been at it longer (twenty years or so). As to *correct*, we're back to the original topic...what can it even *mean* if I say Stepstone's *putative* Set is an *actual* implementation of some abstract definition of Set, other than to point to our a of gauges that at least does verify compliance within some stated tolerance. Since we *have* gone so far as to define what we mean by *correct*, I'd claim (sticking neck waaay out) that our code is not mere rapid prototype, but also *correct* within a defined sense of "correctness". I'd be surprised if we'll ever be truly able to exceed that level, based on the fact that other mature disciplines (bridge builders, plumbers, space shuttles, etc) have never managed to. > Please take it from one who *knows*... >Since I'm at an academic site, I think I need to throw in the obligatory >complaint about the implication that we at academic sites don't *know*. >Don't fall for that, lots of us at .edu sites have done substantial >real-world work. Point well taken. Was only trying to emphasize arrows in my own back; not to imply anything about yours. >But let's continue the war analogy a little further. Outside of a few >special cases (the British vs the Zulu, say) neither the weapons nor the >desirability of the goal has really affected the way the war came out. >What does seem to make a difference is the right tactics. Didn't catch your meaning of British vs Zulu...do you mean like American vs Vietnamese? Not only tactice...also strategies, and determination, and a whole bunch of other stuff. Weapons count too. >So far, we seem to be agreeing that the right tactics are more "formal" >or rigorous in some sense. What I wish we could do is measure the >effect of those tactics. At the risk of picking this to death, what I'm actually saying is a lot less crisp than that, which is best summed up with "Use the right tool for the job". Sometimes the right tool is "formal" or "rigorous", but more often it is not. I've been exploring non-rigorous avenues (OOT, software components marketplaces) for quite some time, and seem to have made some headway there. But rather than getting hung up on the accomplishments, tooting horns re: "the virtues of OOT", I've begun digging into where these approaches leave holes, and backup approaches to fill them. -- Brad Cox; cox@stepstone.com; CI$ 71230,647; 203 426 1875 The Stepstone Corporation; 75 Glen Road; Sandy Hook CT 06482
cox@stpstn.UUCP (Brad Cox) (05/31/90)
In article <19848@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes: >Bruce Weide writes... >.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. Couldn't it be that we're looking through the wrong end of the telescope with all this emphasis on mathematics? *Everybody* deals with with the distinctions between requirement, specification, and implementation, even common-sense individuals like plumbers, waiters, etc. And the common-sense meaning of these terms is precisely the meaning that I've been using. An implementation is *correct* if it complies to its *specification* within an acceptable tolerance. There's nothing mathematical about it. In fact, it is all so common sense that the primary intellectual challenge is trying to convince oneself that common sense really applies to software. But object-oriented technologies drive me precisely towards that conclusion, that is, assuming a software industrial revolution. For a wonderful treatise on this topic, read "Zen and the Art of Motorcycle Maintenance; An Inquiry into Values". It winds up being about a definition of *quality*, which is close to *correctness*. Won't repeat his arguments here...but really try to read this book! -- Brad Cox; cox@stepstone.com; CI$ 71230,647; 203 426 1875 The Stepstone Corporation; 75 Glen Road; Sandy Hook CT 06482
crm@romeo.cs.duke.edu (Charlie Martin) (05/31/90)
You know, I really love it when these net discussions get productive like this..... In article <5131@stpstn.UUCP> cox@stpstn.UUCP (Brad Cox) writes: > >The IEEE article argues that we should begin thinking of object-oriented >(and older) technologies, not as fancier ways of building things from >scratch, but modularity/binding technologies. And just as other domains >have become quite adept at deploying diverse modularity/binding technologies >in common (i.e. sheep herding, shearing, spinning, weaving, sewing, >zippers/buttons/bows can all be viewed as modularity/binding technologies >at different, but thoroughly compatible levels), we need to stop viewing each >technology as a panacea (i.e. Ada vs Smalltalk, or Objective-C vs C++), but >as a tool relevant to a specific level of the software producer/consumer >hierarchy, and usually irrelevant at others. For example, the fact that >C++ provides outstanding gate/block-level integration facilities is >relevant to those whose work demands a better C, and irrelevant to those >whose work demands a chip-level (Software-IC) modularity/binding technology. > I *think* I agree with you to a great extent, although I'm beginning to get a bit lost here. My inderstanding and responses: We shouldn't think of OOP and reuse as a way of building things from components. Instead they represent "modularity/binding technologies". These are different mechanisms for combining what you have into what you want depending on the level of abstraction implied by what you need. Different langauges and such are suited to different levels of abstraction. As an example, C++ is well-suited to binding at a low level (analogous to discete components) and other things are better suited to a higher level. You give Software-IC as an example, from which I presume you mean that Objective-C is such a higher-level mechanism. The level of abstraction point is a good one, and is why we've mostly stopped writing machine language programs. (There are only a few levels of abstraction where machine language is appropriate.) But every time I try to get my hands on the modularity/binding technologies point, it falls apart and seems to turn into "putting things together from components." If you have higher-level components it is easier, so long as the higher level componets are suited to what you are trying to do. I guess that sounds tautologous now. Can you expand on your point a little? On the gate-level vs higher-level point, I've used both Objective-C and C++ and I have to admit I didn't see much difference in the language per se. There is/was a bigger library of higher level components to draw on, but then this is the result of longer and better funded development of these components. I once had a small argument with Tom Love that came down to his saying: "Here's a big application. How many lines for you to write it from scratch, no fair copying in parts of vi or using dbm?" "50,000 lines." "I can write it in Objective-C in 200 lines." "How?" "Well, first I instantiate my editor and data base class libraries...." "Isn't that reuse?" "No, that's class inheritance." The point being that if you *define* the problem statement the right way, it's easy to get the right answer. So is your second point that Objective-C is that much higher level than C++, and if so, on what basis? Or is it that the bigger IC libraries gives OC the advantage. >In other words, think of Objective-C, not as a *language*, but an >environment that supports a modularity/binding technology analogous to >socketed pluggable hardware ICs. There are many ways of building >chips that can plug into these sockets, and many vendors who are doing >so (many of whose work has been bought repackaged, and is now being >distributed by Stepstone). But as long as the components abide by the >socket standard, they do not need not be built via Objective-C. They >can be built in plain C, or C++, or even Cobol, and Objective-C >components can be used via any of these. Its only a matter of abiding >by the low-level socket standard...which brings me right back to where >we started, the need for specification/testing languages capable of >describing, and then verifying compliance to, these standards. I still don't see that OC is particularly advantageous compared to C++, but maybe that's a side issue. In any case, it's your product and your idea, and you're entitiled to some pride of ownership: it really is a substantial thing. One problem with the "socket standard" -- and this is a practical problem, not an objection to your definition -- is that the number of reasonable degrees of freedom is so large in software. Unlike circuits, the bandwidth of our connections is very high. This leaves more room for variation, and it gets used. >>Also, my experience with both Smalltalk and Objective-C (admittedly >>limited) has been that to use the libraries of classes available, one >>had to buy into a lot of architectural assumptions that might or >>moght not fit what was needed, e.g., garbage-collection or >>interpretive codes. (At a little higher level, things like >>model-view-controller.) To use any other architectural assumption >>meant backing up and rebuilding the universe from primitives. >Software's abstract/concrete hybrid nature is simultaneously our curse, and >our blessing (in that it guarantees us higher salaries than those who work >in more concrete domains, like flipping burgers). But apart from this >fundamental difference, I'd argue that other domains experience exactly >the same kind of complications, but have grown thoroughly adept at mastering >them. For example, you might want to take advantage of a hardware store's >new inventory in copper plumbing pipes, but in a house with existing iron >pipes, you'd face corrosion problems; a preexisting architectural decision. >But somehow mature industries like plumbing always seem to provide a way >of getting around incompatible architectures; i.e. by selling an suitable >adaptor. I grant you, we're far more immature an industry than plumbers, >and off-the-shelf adaptors are still rare and raise cultural objections, >such as thinking of such adaptors as kludges. > >> Re: academic types, please see Ralph London's formal specification (in Z, >> as I recall) of the Smalltalk Set class. >> > >I get your point re: Oxford, but Ralph London is an American thru and >thru. Works at Tektronix Labs, I think in Beaverton. Wish I had a >reference to his article to give you, but it was beautiful work, and >insightful into the difficulty of applying a mathematical approach to >well-understood piece of concrete engineering effort. Sorry, I'd remembered the paper as having been published as an Oxford monograph. Can't find the reference right at hand. But this is still someone other than an academic.... >Without disagreeing with you one bit that quality costs money that the >market can be reluctant to pay, be aware that although Stepstone's code >started out as rapid prototypes (like any other code), after seven >years of improving it is considerably better than that. The same is >true of Smalltalk, except they've been at it longer (twenty years or >so). As to *correct*, we're back to the original topic...what can it >even *mean* if I say Stepstone's *putative* Set is an *actual* >implementation of some abstract definition of Set, other than to point >to our a of gauges that at least does verify compliance within some >stated tolerance. Since we *have* gone so far as to define what we mean >by *correct*, I'd claim (sticking neck waaay out) that our code is not >mere rapid prototype, but also *correct* within a defined sense of >"correctness". I'd be surprised if we'll ever be truly able to exceed >that level, based on the fact that other mature disciplines (bridge >builders, plumbers, space shuttles, etc) have never managed to. Sorry, I think I wasn't clear there: what I meant to say was that the *advantage* you-all sell is not greater code correctness -- which doesn't seem to sell well -- but the productivity advantages. Or am I mistaking your approach from the PPI days? On the Brits vs Zulu point, what I meant was that superiour weapons must be DAMNED superior before they are a telling point in warfare. The British defeated multiple thousands of Zulus with spears and shields by using Gatling guns and just a few hundred soldiers. It wasn't because the Zulus were unskilled or cowards (the opposite: they should have run like rabbits!) but in that case better technology. Your US in Viet Nam is a good analogy for the other side: given appropriate tactics, small similarly armed forces can whup bigger forces. And my point was that maybe it isn't the coding etc technology at all, but rather Something Else. I think rigor in reasoning about software MIGHT be that something else. 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
crm@romeo.cs.duke.edu (Charlie Martin) (06/01/90)
In article <19848@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes: > >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. Couldn't it be that we're looking through the wrong end of the telescope with all this emphasis on mathematics? *Everybody* deals with with the distinctions between requirement, specification, and implementation, even common-sense individuals like plumbers, waiters, etc. It certainly *could* be, but I don't think we *are*. The problem here is that we are often dealing with something other than common-sense objects when we deal with software. At the lowest level, we're dealing with an arbitrary instruction set; at higher levels, we are often dealing with abstractions that purport to be mathematical objects: integers. "real" numbers, Sets, OrderedSets.... The only meaningful specification for these is inherently mathematical. The behavior of a "float" in calculations often has nothing common-sensical about it whatsoever. They don't work as we expect from the arithmetic we learned in 3rd grade, and they screw up the rules we learned in 9th grade algebra -- sometimes. Higher level abstractions often get worse, not better. I admit that we can make up some kind of reasonable expectation about typing into a window on a screen, based on our knowledge of typing on paper (but even then, we don't actually build systems that work that way, although a few old text editors did) but there is no common-sense to appeal to about what happens when we double-click a mouse. [T]he common-sense meaning of these terms is precisely the meaning that I've been using. An implementation is *correct* if it complies to its *specification* within an acceptable tolerance. There's nothing mathematical about it. Come on Brad, you're contradicting yourself in-line, here. "...within an acceptable tolerance" is a mathematical statement, and it's interpreted as such in ANY form of engineering. If I design a gear and I want it milled to within one-one-thousandth of an inch, I am stating a measure, and stating a numerical value against which the measured gear can be compared by measuring. If I want to do QA on gears, I state a statistical distribution and acceptable variance. These are all mathematical statements. For a wonderful treatise on this topic, read "Zen and the Art of Motorcycle Maintenance; An Inquiry into Values". It winds up being about a definition of *quality*, which is close to *correctness*. Won't repeat his arguments here...but really try to read this book! If anyone is reading this who *hasn't* read Persig's book, then for Ghod's sake stop at the library on the way home. But, as much as I like and admire the book, its major premise is that Quality (Persig's way of denoting the special thing he is talking about) is something that can't be measured or quantified in any way -- that any attempt to do so is *maya*, illusion, part of the world of words, not the world of things. So this leads to the implication that Brad is saying that Correctness is also something that can't be measured or quantified in any way. I can see the argument, which is one reason that I wish the formal methods folks had chosen some other word -- say "compliance" -- for the concept of "meets the specification in all cases." (After all, it is not in some sense correct unless the user *likes* it; the only measure for this is if they then *pay* for it, and this can be a very indirect one.) However, attractive as it is philosophically, it's not a useful idea for engineering. It comes down to arguing that whether or not an implementation meets its specification is something that is not mathematical, not quantifiable or measurable in any way. (Notice that this excludes *testing* just as much as it does proof). If Correctness really *is* like Persig's Quality, then there is only the ability of a trained eye to directly perceive the wondrous Correctness of the result of one's engineering efforts. I don't think that is suitable in any kind of engineering: I certainly wouldn't want to drive across a bridge whose capacity couldn't be measured. The difficulty of a purely testing-based approach to "correctness" as Brad is apparently advocating, is that we CAN'T in all cases depend on the common-sense behavior of the system in question. To steal an example from your paper (which I got today, thanks!) a gunsmith can be satisfied with testing a gunbarrel by putting four times the charge into the barrel and then firing it BECAUSE he can depend that a barrel which doesn't explode with 1000 grains of powder is very very unlikely to explode with 995 grains of powder, or 250 grains of powder. But there are real bugs in real systems that manifest by the system working fine for values 1..236, failing for values 237, 559, and 623, then working perfectly on every other value on up to 1000. In this situation, assuming that all these values are equiprobable in use, then the probability of failure over all is 3 in 1000 -- but testing with a value of 1000 doesn't tell us that. Nor does testing with a value of 4000, even if it works. The advantage of formal methods in real use (it seems to me, either philosophically or as an engineer) is that it gives us an argument to raise our degree of certainty so that we *can* believe that a few tests really do lead to near certainty that our implementation is going to work for any specified input. 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
jon@cs.washington.edu (Jon Jacky) (06/01/90)
I can't resist responding to comments by Charlie Martin, Bruce Weide, Brad Cox and maybe others too (I can no longer untangle who said what): > it's pretty hard to show a library of reusable components that are generally > agreed to be reusable and non-trivial ... how can you demonstrate > scientifically that they are `reusable'? What about libraries of numerical routines for finding roots, solving linear systems, doing FFT's and all that traditional scientific and engineering work? Packages like IMSL, LINPACK, EISPACK, NAG and others have been around for ages and are very heavily used. You know, the kind of thing you find in ACM COLLECTED ALGORITHMS and the NUMERICAL RECIPES books. It may help that the kinds of objects they deal with, like matrices, are well understood outside computer science, in fact they predate computers. > Political problem: (how can a researcher get credit, publications, tenure, > by building) a really good reusable non-trivial library? By providing new, useful solutions to application problems that others are trying to solve. In addition to the numerical stuff mentioned above, there has been some activity in recent decades in libraries of routines for doing graphics and image processing. There are probably application-specific libraries I don't know about. In these application areas, you get the academic (or other) credit for solving the application problem, not for crafting the library as such. Application people think of things at a lot coarser level of granularity than those with a mostly computer science bent: they don't think, "What I really need is a good implementation of sets," they think, "I need an adaptive histogram equalization image contrast enhancer". As a result the application libraries do not get much attention as computer science artifacts. I believe William Howden did a systematic study of errors in the IMSL library quite a while ago and there may have been some similar European work on the NAG library, but that's about it. > A specification is "formal" if it ... can be used to verify the correctness > of ... an implementation ... Emphasis on verification of implementations excludes a lot of what formal specifications are about. Often you need to reason about the properties of some proposed system, and this is a prerequisite to deciding if you want to implement the specified behavior at all. Formal specifications may make it possible to reason about system behavior by applying rules of inference (as opposed to building an implementation and experimenting with it). For example, you might want to show that some proposed collection of operations cannot violate particular assertions about safety. This is an entirely separate issue from verification and is independent of any particular implementation. > (seeking Reference to paper by London et al on specification of sets) @inproceedings{softeng:london89, author="Ralph L. London and Kathleen R. Milsted", title="Specifying Reusable Components Using Z: Realistic Sets and Dictionaries", booktitle="Proceedings of the Fifth International Workshop on Software Specification and Design", year="1989", publisher="IEEE Computer Society Press", address="Washington, DC", pages="120--127"} - Jon Jacky, jon@gaffer.rad.washington.edu
zarnuk@caen.engin.umich.edu (Paul Steven Mccarthy) (06/01/90)
>(Brad Cox) writes: >Because during any major paradigm shift, the conservatives *radically* >outnumber the revolutionaries. That is why the market for a better C is so >much larger than the market for off-the-shelf software components. This is a chicken-and-the-egg problem. Not to impune the putative quality of Stepstone's products (I have never used any), but just to add my $.02 worth from practical experience: Every off-the-shelf package that I have used has burned me in the end. It is exactly an issue of quality and correctness. I always read all available documentation with careful scrutiny and design my systems "by the book" -- only to find thousands of wasted development dollars and hundreds of unrecoverable hours later that the package does not match the documentation or contains substantive bugs. (This does not even address the countless packages that are inadequately defined by their associated documentation). I am in unequivocal agreement with both you concerning the need for *better* (more/less formal--I don't care) means of establishing correctness. More formal systems should be easier to automate, but that doesn't mean that adequate manual systems can't be developed. The key concepts are CLARITY and COMPLETENESS. As far as off-the-shelf components go, I would be much more comfortable buying formally specified and tested components than the hit-or-miss choices that I'm currently facing. ---Paul...
weide@elephant.cis.ohio-state.edu (Bruce Weide) (06/02/90)
In article <12085@june.cs.washington.edu> jon@cs.washington.edu (Jon Jacky) writes: >----- >I can't resist responding to comments by Charlie Martin, Bruce Weide, >Brad Cox and maybe others too (I can no longer untangle who said what): >... > >> A specification is "formal" if it ... can be used to verify the correctness >> of ... an implementation ... > >Emphasis on verification of implementations excludes a lot of what formal >specifications are about. Often you need to reason about the properties of >some proposed system, and this is a prerequisite to deciding if you want to >implement the specified behavior at all. Formal specifications may make it >possible to reason about system behavior by applying rules of inference (as >opposed to building an implementation and experimenting with it). For example, >you might want to show that some proposed collection of operations cannot >violate particular assertions about safety. This is an entirely separate >issue from verification and is independent of any particular implementation. >----- FYI, I made the original statement about what I'd consider a "formal specification" as opposed to a "rigorous specification." I agree, of course, that one can use formal statements to "reason about the properties of some proposed system." In fact, the ability to do this before you implement the specified software was one of the three specific criteria I offered for deciding whether you had a "formal specification." It is not "an entirely separate issue from verification" because it is exactly at the heart of verifying that the CLIENT of the not-yet-implemented system will behave as expected. Therefore, I'm not sure how your point relates to the proposed definition of what should be called a "formal specification." If you're saying that we should call something a "formal specification" even if it doesn't COMPLETELY describe the intended behavior, then we agree there, too. It is possible for a formal specification to permit tremendous latitude in the implementation. For example, if you want to say that the following is a specification of the behavior of the effect of a "push" operation on a stack s: length(s) = length(original s) + 1 then you'd better be willing to accept lots of weird, non-stack-like implementations. The point is that just calling it a "stack" doesn't mean a thing. If you want intuitive stack-like behavior you have to ask for it in the specification. If all you want to do is reason about the lengths of stacks then your specification is fine, but again, don't blame me if I implement a FIFO queue or something. If your reasoning depends on me providing you with code that implements a stack (as you intuitive expect it to behave) you'll have to say so explicitly. And this seems to have nothing to do with the distinction between formalism and rigor, unless use of the word "stack" is somehow considered rigorous enough. This gets to Brad Cox's point about "common sense." I guess the above example helps illustrate where Brad and I might disagree (if I understand the argument he's making). Brad seems willing to describe the intended behavior of stacks by saying the implemented objects "act like stacks" and relying on my common sense to understand what he means. As I've pointed out before, though, even THIS seemingly rather precise statement means different things to different people. It's not that hard to say it rigorously, and (IMHO) no harder to say it formally than rigorously. I still don't understand the resistance to doing so. People keep implying or explicitly stating that formal specs are inherently such a pain, but why? -Bruce
zarnuk@caen.engin.umich.edu (Paul Steven Mccarthy) (06/02/90)
>(Bruce Weide) writes: > [discussion about informal/rigorous/formal specs]... It's >not that hard to say it rigorously, and (IMHO) no harder to say it >formally than rigorously. Bruce, I agree with you in principle: it is not much harder _conceptually_ to cast "rigorous" specifications into "formal" notation, but it does require more _work_. Worst of all, most of the additional effort is "busy-work" symbol manipulation or fitting square pegs into round holes to express a simple concept in a language that does not support the concept directly. (We Americans are just too impatient! :) As I see it, formal specifications cost more up front, but they pay off in the long run. They certainly take the guess-work out of trying to figure out if/how you can you use a component. ---Paul...
cox@stpstn.UUCP (Brad Cox) (06/02/90)
In article <19946@duke.cs.duke.edu> crm@romeo.UUCP (Charlie Martin) writes: >The level of abstraction point is a good one, and is why we've mostly >stopped writing machine language programs. (There are only a few levels >of abstraction where machine language is appropriate.) But every time I >try to get my hands on the modularity/binding technologies point, it >falls apart and seems to turn into "putting things together from >components." If you have higher-level components it is easier, so long >as the higher level componets are suited to what you are trying to do. > >I guess that sounds tautologous now. Can you expand on your point a >little? The distinction is between "building from first principles" (fabrication) and "building from components (assembly). Fabrication involves reuse of only raw materials, while assembly involves reuse of higher-level components. The first involves a flat organizational structure (programming language vendors as providers of low-level raw materials; i.e. int, float, strcmp()), whereas the second involves a deep organizational structure; a software components marketplace. Evolving from our present flat structure (cottage industry) to a deep structure is what the IEEE paper means by a "software industrial revolution". >On the gate-level vs higher-level point, I've used both Objective-C and >C++ and I have to admit I didn't see much difference in the language >per se. There is/was a bigger library of higher level components to >draw on, but then this is the result of longer and better funded >development of these components. That is *precisely* my point. Viewing them as competing *languages* misses the fact one is solely a language and the other an *environment* of off-the-shelf software components (Software-ICs). >So is your second point that Objective-C is that much higher level than >C++, and if so, on what basis? Or is it that the bigger IC libraries >gives OC the advantage. It is "higher-level" in the sense that a soldering iron (for assembling chips to make boards) is a higher-level tool than a photolithography machine (for assembling gates to make blocks, and blocks to make chips). Both are modularity/binding technologies, and both support reuse, but at radically different *levels*. But soldering irons and photolithography machines *do not compete*, but *support* each other. They provide *radically* different services to *radically* different audiences. Photolithography machines require far more skill to use than soldering irons (lower man-productivity) but deliver greater performance (higher machine-productivity). But it is the the pluggability of soldering irons that created the very possibility of today's marketplace in hardware components (by this I mean, it was the invention of the silicon chip and circuit boards that made the very notion of a hardware marketplace thinkable). So it is with Objective-C. >I still don't see that OC is particularly advantageous compared to C++, >but maybe that's a side issue. In any case, it's your product and >your idea, and you're entitiled to some pride of ownership: it really is >a substantial thing. Many people's difficulty here arises from comparing the technologies themselves, rather than their organizational implications. In other words photolithography machines are technologically impressive, rich functionality, need great skill to use well. Soldering irons are simple, and require much lower skill to use effectively. Compared as technologies, photolithography machines are clearly 'superior'. But viewed insofar as their organizational implications, soldering irons created the very possibility of a multi-level marketplace in reusable hardware components. A *lot* more people are capable of using soldering irons than photolithography machines. -- Brad Cox; cox@stepstone.com; CI$ 71230,647; 203 426 1875 The Stepstone Corporation; 75 Glen Road; Sandy Hook CT 06482
cox@stpstn.UUCP (Brad Cox) (06/02/90)
In article <19948@duke.cs.duke.edu> crm@romeo.cs.duke.edu (Charlie Martin) writes:
< [T]he common-sense meaning of these terms is precisely the meaning
< that I've been using. An implementation is *correct* if it complies
< to its *specification* within an acceptable tolerance. There's
< nothing mathematical about it.
<
<Come on Brad, you're contradicting yourself in-line, here. "...within
<an acceptable tolerance" is a mathematical statement, and it's
<interpreted as such in ANY form of engineering. If I design a gear and
<I want it milled to within one-one-thousandth of an inch, I am stating a
<measure, and stating a numerical value against which the measured gear
<can be compared by measuring. If I want to do QA on gears, I state a
<statistical distribution and acceptable variance. These are all
<mathematical statements.
Change the example slightly, say to hamburgers, and "tolerance" as to
what is "acceptable" becomes much less obviously mathematical.
I don't want to be pushed into an either/or situation here, because software
really *is* a swamp; a hybrid of land and sea; a nearly 50-50 hybrid between
the concrete domain of burger flipping and the abstract domain of mathematics.
<So this leads to the implication that Brad is saying that Correctness is
<also something that can't be measured or quantified in any way. I can
<see the argument, which is one reason that I wish the formal methods
<folks had chosen some other word -- say "compliance" -- for the concept
<of "meets the specification in all cases." (After all, it is not in
<some sense correct unless the user *likes* it; the only measure for this
<is if they then *pay* for it, and this can be a very indirect one.)
<However, attractive as it is philosophically, it's not a useful idea for
<engineering. It comes down to arguing that whether or not an
<implementation meets its specification is something that is not
<mathematical, not quantifiable or measurable in any way. (Notice that
<this excludes *testing* just as much as it does proof).
No, you're misstating me. My whole point about specification/testing languages
is that we *do* need to start getting as serious about specifying software as
McDonalds is about specifying burgers. Correctness (or quality) *can* be
measured, but its absolute measure is the satisfaction it brings to its users,
which of course can only be measured by its consumers. Its *producers*, however,
must be satisfied with less technologically appealing indirect measures, since
the absolute measure is technologically intractible (brain probes, anyone?)
<If Correctness really *is* like Persig's Quality, then there is only the
<ability of a trained eye to directly perceive the wondrous Correctness
<of the result of one's engineering efforts. I don't think that is
<suitable in any kind of engineering: I certainly wouldn't want to drive
<across a bridge whose capacity couldn't be measured.
<
<The difficulty of a purely testing-based approach to "correctness" as
<Brad is apparently advocating, is that we CAN'T in all cases depend on
<the common-sense behavior of the system in question.
Again, I'd never advocate any *pure* approach to anything as impure as swamp.
The point of the paper was that bridges and guns and plumbing systems would be
as problematic as software if we built them as we do software, by having each
plumber mine, refine, and manufacture their own components rather than by
distributing this effort over time and space via a marketplace. As you've
pointed out, marketplaces are not pure approaches. They involve some
mathematics here, some common sense there, some politics yonder, etc, etc.
--
Brad Cox; cox@stepstone.com; CI$ 71230,647; 203 426 1875
The Stepstone Corporation; 75 Glen Road; Sandy Hook CT 06482cox@stpstn.UUCP (Brad Cox) (06/03/90)
In article <81111@tut.cis.ohio-state.edu> Bruce Weide <weide@cis.ohio-state.edu> writes:
<This gets to Brad Cox's point about "common sense." I guess the above
<example helps illustrate where Brad and I might disagree (if I
<understand the argument he's making). Brad seems willing to describe
<the intended behavior of stacks by saying the implemented objects "act
<like stacks" and relying on my common sense to understand what he
<means. As I've pointed out before, though, even THIS seemingly rather
<precise statement means different things to different people. It's
<not that hard to say it rigorously, and (IMHO) no harder to say it
<formally than rigorously. I still don't understand the resistance to
<doing so. People keep implying or explicitly stating that formal
<specs are inherently such a pain, but why?
"Most" people (certainly not myself) aren't saying that they're a big pain
for stacks. A lot of them *are* saying that their usefulness is less obvious
than their costs for bigger objects like Sets (see Ralph London's article),
word processors, or hamburgers.
To restate what I'm saying once more, I'm interested in a paradigm shift,
a software industrial revolution. We'd start applyingw3 an organizational
principle called *division of labor* (or *reusability*). In the end
(which might take as much as fifty years, which seems to be the historical
time constant for such paradigm shifts) we'd have software components
marketplaces, in which building a word processor from trusted components
might be done with about as much effort as it is to build a stack from
raw software materials (ints, pointers, etc).
This path, while *clearly* not easy, might get us to the point where the
formal approaches you advocate for Stack might also apply to word processors.
--
Brad Cox; cox@stepstone.com; CI$ 71230,647; 203 426 1875
The Stepstone Corporation; 75 Glen Road; Sandy Hook CT 06482db@lfcs.ed.ac.uk (Dave Berry) (06/04/90)
In article <19948@duke.cs.duke.edu> crm@romeo.cs.duke.edu (Charlie Martin) writes: >The advantage of formal methods in real use (it seems to me, either >philosophically or as an engineer) is that it gives us an argument to >raise our degree of certainty so that we *can* believe that a few tests >really do lead to near certainty that our implementation is going to >work for any specified input. Another advantage is that they can be quicker than testing. Witness the use of formal methods by INMOS in the development of the floating point unit for the T800 transputer. Dave Berry, LFCS, Edinburgh Uni. db%lfcs.ed.ac.uk@nsfnet-relay.ac.uk "ML don't stand for nothing! ML *is* ML" -- Spike Lee.
weide@elephant.cis.ohio-state.edu (Bruce Weide) (06/04/90)
In article <5152@stpstn.UUCP> cox@stpstn.UUCP (Brad Cox) writes regarding whether formal specifications are a pain: >-------- > >"Most" people (certainly not myself) aren't saying that they're a big pain >for stacks. A lot of them *are* saying that their usefulness is less obvious >than their costs for bigger objects like Sets (see Ralph London's article), >word processors, or hamburgers. > >-------- We've written the formal spec for a set module, too, and it's awfully easy to write the spec once you have decided on a design of the intended abstract behavior. (This may sound trivial but it is not if reuse is an issue.) We've also written quite comprehensible formal specs for lots of other concepts, too, including partial functions (for associative searching), graphs, etc., and have been teaching them to undergraduates and to practicing software engineers in industry for several years. In fact, the spec for a set module has been a favorite exam question. So this notion that stacks are the only things people can specify formally (yet still comprehensibly) is just plain bogus. It is to be expected that a formal spec for a word processor is going to be rather formidable, even AFTER you have figured out what it is and how it is supposed to behave from an abstract viewpoint. But this difficulty can hardly be attributed to the desire to make the specification formal. Do you have something you'd call an acceptable "rigorous" specification of a word processor? I'd be surprised if it couldn't be stated formally with just about the same number of symbols, and if the formal spec wasn't just about as readable to someone who has learned to read a formal specification. Besides, I'll let you attach an informal and/or rigorous spec to the formal one if you think it will help people understand what's going on. A formal spec can include natural language comments. The comments just won't be machine-processable and won't participate in correctness proofs any more than comments in code participate in code generation. What I'm suggesting is that formality is not much more expensive than rigor. It may pay off big-time in the long run precisely because of reuse. Reuse of components demands that the client understand WHAT a reusable component is supposed to do, and that the client be confident that the implementation he/she is buying actually does it. Formality makes the first objective feasible if people can learn how to read formal specs; everyone doesn't have to be an expert in writing them. And if formally specified components are reused, the cost of formal verification of correctness of implementations can be amortized over many future uses. I'm not saying there's no place for informality in software, just that we should not overlook places where formality can help, nor the possibility of (re)using some of the work that mathematicians have been so kind to do for us. Let me not discuss the formal specification of a hamburger, because all I'm arguing for is formal specification of software components. I never claimed the technique would or should be applied to everything in the world... Although living in the home of Wendy's and a variety of other fast food chains, maybe I could tap into some local industrial support if I could adapt the method to burgers. Hmmm... -Bruce
crm@romeo.cs.duke.edu (Charlie Martin) (06/05/90)
In article <4467@castle.ed.ac.uk db@lfcs.ed.ac.uk (Dave Berry) writes: In article <19948@duke.cs.duke.edu crm@romeo.cs.duke.edu (Charlie Martin) writes: The advantage of formal methods in real use (it seems to me, either philosophically or as an engineer) is that it gives us an argument to raise our degree of certainty so that we *can* believe that a few tests really do lead to near certainty that our implementation is going to work for any specified input. Another advantage is that they can be quicker than testing. Witness the use of formal methods by INMOS in the development of the floating point unit for the T800 transputer. Oops, this is going to restart the Fetzer-dilemma argument: I assume you are asserting that you can *eliminate* testing through formal analysis. 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
sean@castle.ed.ac.uk (S Matthews) (06/05/90)
In article <81153@tut.cis.ohio-state.edu> Bruce Weide <weide@cis.ohio-state.edu> writes: >In article <5152@stpstn.UUCP> cox@stpstn.UUCP (Brad Cox) writes >regarding whether formal specifications are a pain: > >>-------- >> >>"Most" people (certainly not myself) aren't saying that they're a big pain >>for stacks. A lot of them *are* saying that their usefulness is less obvious >>than their costs for bigger objects like Sets (see Ralph London's article), >>word processors, or hamburgers. >> >>-------- > If you want to see a formal specification of a word processor look at Sufrin's spec in specification case studies by Ian Hayes. It is actually for a display oriented editor, rather than a full word processor and to be frank it is a crummy design, but then it was a piece of reverse engineering, so that is not a fair criticism of the quality of the specification *as a specification*. It is certainly not complex or a pain, and it is very readable, and highlights nicely some of the differences between a specification and a program because of the intention. It would be interesting to see how it would be extended into a full editor. Sean P.S. there is another (new---there is also an older, out of print, book by Bjorner and him) book in the same series that gives examples of VDM specifications as well, edited by Jones. Why don't some of you read them so that you know what formal specs of (semi) real systems look like. You would also be able to compare notes on the same specs!
geoffb@butcombe.inmos.co.uk (Geoff Barrett) (06/07/90)
In article <81153@tut.cis.ohio-state.edu> Bruce Weide <weide@cis.ohio-state.edu> writes: > Do you have something you'd call an acceptable >"rigorous" specification of a word processor? What about an acceptable "informal" specification of a word processor? vvv| |vvv------------------------------------- \ o o / \ / Wot! No Queen's Award logo? \_/