From: "Mark Wonsil" <[log in to unmask]>


> Steve after Stan writes:
> >> Having code (at a single-point of termination) to close/cleanup
> >>things is good.
> >
> >As a blanket statement? We'll have to disagree on that one.
>
> Has anyone read "The Science of Programming" by David Gries
(Springer-Verlag
> 1981)?  IIRC, the point of the book was "Proving programs correct".  It
took
> a mathematical-proof approach to programming.  One would create functions
> that acted like an a assert() function.  The one I remember was wp
(weakest
> precondition).  Here one would check all inputs and outputs and
essentially
> place assert() calls to make sure all conditions were met to guarantee the
> program worked as advertised.  I don't know if it every caught on but this
> conversation reminded me of the topic.


The idea of "proving programs correct" has not proved to be practical.
Writing correct full specifications turns out to be as hard as writing
correct progams.  Gries gives examples such as square root, which are easy
to write specifications for, but these are the exception.

Some of the ideas have proved useful, even though they fall far short of a
proof of correctness.  Design by Contract is a methodology which supports
the use of preconditions, postconditions,  and invariants.  It's much easier
when you use a language that is designed with this in mind (Eiffel).

Many C programmers use assert statements as test and debugging aids.  See
Steve Maguire's "Writing Solid Code" for its use at Microsoft (circa 1992).

* To join/leave the list, search archives, change list settings, *
* etc., please visit http://raven.utc.edu/archives/hp3000-l.html *