Bryan O'Sullivan wrote:
b> Language like the "contract between the caller and callee" are
b> distinctively from Bertrand Meyer's writings.
Er, no. Such notions have been floating around since quite a long
time before Meyer popped up.
I guess I haven't been in the field long enough to know. The first I
heard of the "Contract" metaphor was in 1986, and OOSC was published in
1988.
I've read a lot of material on software engineering since then and PWT
was the first reference that I've read since then that liberally used
the contract metaphor in describing how to write correct code. I will
grant that "assert.h" has been around, but I'm talking about the
application of assertions and not the existence of them.
"Such notions" is pretty vague, can you elaborate or provide a reference
to an earlier use of the contract metaphor?
Anyway, PWT is pretty well written. It just gave me enough of a sense
of deja vue that I decided to leaf through the bibliography. The lack
of the OOSC reference surprised me.
Regards,
Mike Hancock
- Bart
--
Bart Smaalders Solaris Clustering SunSoft
ba...@cyber.eng.sun.com (415) 786-5335 MS UMPK17-301
http://playground.sun.com/~barts 2550 Garcia Ave
Mt View, CA 94043-1100
It would seem Meyer's is the original reference, considering the dates
listed in the site start from '92.
Thanks for the reference. Has the data cache coherence work made it into
Solaris. FreeBSD has a unified buffer cache now using vm objects.
Regards,
Mike Hancock
The concepts of preconditions and postconditions to form a contract
on a routine go back at least to Dijkstra and Hoare in the late 60's
and early 70's. In the late 70's and early 80's there were a couple
of experimental languages Alphard and Euclid that were designed to
support assertions. It's not clear to me how much they succeeded in
implementing these, however.
IMHO, Meyer made two major contributions in this area (along with
a host of lesser ones). :
1. Brought the world Eiffel, the first commercial language to support
Hoare's and Dijkstra's ideas.
2. Was the first to get the interaction of subtyping and assertions
exactly right _and_ implement it in a commercial language.
For some reason I don't fully understand, Pierre America is often credited
with #2.
>
>I've read a lot of material on software engineering since then and PWT
>was the first reference that I've read since then that liberally used
>the contract metaphor in describing how to write correct code. I will
>grant that "assert.h" has been around, but I'm talking about the
>application of assertions and not the existence of them.
>
>"Such notions" is pretty vague, can you elaborate or provide a reference
>to an earlier use of the contract metaphor?
>
>Anyway, PWT is pretty well written. It just gave me enough of a sense
>of deja vue that I decided to leaf through the bibliography. The lack
>of the OOSC reference surprised me.
I missed the beginning of this thread. What's PWT?
>
>Regards,
>
>Mike Hancock
>
Hope this helps,
-- Jim
--
*------------------------------------------------------------------------------*
Jim McKim (860)-548-2458 Teachers affect eternity. They can never tell
Internet: j...@hgc.edu where their influence stops.
The concepts of preconditions and postconditions to form a contract
on a routine go back at least to Dijkstra and Hoare in the late 60's
and early 70's. In the late 70's and early 80's there were a couple
of experimental languages Alphard and Euclid that were designed to
support assertions. It's not clear to me how much they succeeded in
implementing these, however.
IMHO, Meyer made two major contributions in this area (along with
a host of lesser ones). :
1. Brought the world Eiffel, the first commercial language to
support
Hoare's and Dijkstra's ideas.
2. Was the first to get the interaction of subtyping and
assertions
exactly right _and_ implement it in a commercial language.
Thanks for the info.
>Anyway, PWT is pretty well written. It just gave me enough of a
sense
>of deja vue that I decided to leaf through the bibliography. The
lack
>of the OOSC reference surprised me.
I missed the beginning of this thread. What's PWT?
"Programming with Threads", by Steve Kleiman, Devang Shah, and Bart
Smaalders. It covers primarily POSIX threads with some references to UI
threads.
They vigorously promote the use of invariants throughout the book. It
doesn't go as far as Eiffel, but it is unusual to see this much
attention paid to correctness in most texts I've seen.
Regards,
Mike Hancock
On the predecessors, the following should be quoted:
- Besides Dijkstra and Hoare, Bob Floyd's original paper
"Assigning meanings to programs" (1967) which was
the first to use assertions systematically for program
proving. (Hoare also cites an early mention by Turing himself,
but this was not fully developed.)
- Besides Alphard and Euclid, the CLU language. (One may
also mention Turing, but it is a contemporary rather than
a predecessor.)
- The formal languages Z by Abrial (especially the initial
version developed in France) and VDM by Jones and Bjorner.
- Work on abstract data types (Liskov & Zilles, Guttag
and Horning, as well as my own which, however, was not
widely circulated).
On the original aspects, apart from what James McKim mentions,
one should note:
- The importance of invariants, although the basic ideas come
from Hoare ("Proof of Correctness of Data Representations")
and VDM. Although both Alphard and CLU had a notion of
invariant, it is less developed than in Eiffel.
- The connection with exception handling. As far as I know
Eiffel's exception handling mechanism is original
(although influenced by earlier work, especially Randell's
and Cristian's); it applies the notion of Design by Contract
to the processing of abnormal cases. This is certainly one
of the most important aspects of the approach.
- The insistence on executability of assertions. (CLU assertions,
for example, are more like comments.) Actually I have the
impression that the idea of evaluating assertions would be
anathema to Dijkstra. (The precedent here is Algol W, followed
by C, but all they support is an "assert" instruction
rather than a full-fledged assertion mechanism.)
- The methododological consequences. Central to the theory of
Design by Contract is the idea that to obtain more reliable
software you should often have *fewer* checks (thanks to
assertions). I have never seen any precursor to that apparently
paradoxical idea - the rule that a routine
should never test for its precondition; if you know of an
earlier publication please tell me.
As far as I can tell it is not only original but in
fact runs contrary to the accepted ideas in software
engineering, as found in many textbooks
(e.g. in Liskov's and Guttag's otherwise excellent
"Abstraction and Specification..."). In my experience it
brings about a major change to software development, as important
as the rest of object technology. (I realize that people who
haven't yet tried Eiffel don't necessarily believe this, but
it's the truth nevertheless.)
- The notion of short form: taking advantage of the presence
of contracts to permit self-documenting software. Again this
is pretty much against everything I had read in the software
engineering literature when Eiffel was designed.
- The close connection with object-oriented structuring
(not just the connection with redefinition, i.e. precondition
weakening and postcondition strengthening, pointed out by
James McKim).
- Invariant accumulation in an inheritance hierarchy.
- Some of the theoretical perspective (in particular the
connection between object-oriented principles and the theory
of abstract data types - this is mostly in "Object-Oriented
Software Construction" second edition).
- The `old' construct. (Although it has equivalents
at least in Alphard and Z, these two languages are
not executable. Z is a specification language, and
for Alphard, as far as I was able to understand, there
never was a released compiler or a fixed specification.
Someone may correct me on this last point; my understanding
is based on what I heard at the time - late seventies -,
and on the Springer-Verlag book "Alphard: Form and Content"
edited by Mary Shaw.)
- The close integration of a full-fledged assertion mechanism
in a commercial programming language. (The assertion facility
of Algol W may be viewed as a precedent but, as noted, is of
limited scope. If we remove the qualifier "commercial" this
point is, however, less strong than the previous ones, as we
can bring up Euclid and Turing.)
--
Bertrand Meyer, President, ISE Inc., Santa Barbara (California)
805-685-1006, fax 805-685-6869, <bert...@eiffel.com> -
ftp://ftp.eiffel.com
Visit our Web page: http://www.eiffel.com
(including instructions to download Eiffel 4 for Windows)