From: Richard D Riehle <laoXhai@ix.netcom.com>
Subject: Re: 'constant functions' and access constant params (was Re: Array of Variant Records Question...)
Date: 1999/09/28
Date: 1999-09-28T14:56:05-05:00 [thread overview]
Message-ID: <7sr6gl$soc@dfw-ixnews19.ix.netcom.com> (raw)
In-Reply-To: 7sqbt6$1la$1@nnrp1.deja.com
In article <7sqbt6$1la$1@nnrp1.deja.com>,
Robert Dewar <robert_dewar@my-deja.com> wrote:
>Assertions written at the level of the language itself only
>fix a very small part of this problem. And if you talk
>about compiler-checked assertions, then you are reducing the
>level of the assertions to a trivial level that definitely
>does not begin to approach full specification (remember we
>are FAR from being able to mechanically check that a full
>formal specification matches an implementation in a language
>at the semantic level of Ada, such checks require a large amount
>of human intervention at the implementation level, e.g. adding
>proof assertions).
I agree with most of your observations here. Even Bertrand Meyer,
advocate of "design by contract" through assertions, agrees that
we have not yet reached a point in software design where we can
rely on a compiler to "prove" the validity of an assertion. Of
greater concern is that one can construct an assertion so complex
that no current theorem-proving software can guarantee its correctness.
As much as I agree with Parnas, Gries, Dijkstra, and Knuth about the
desirability of assertions, I continue to be skeptical of their
usefulness in large-scale software systems.
>Furthermore, full formal specifications are often neither
>desirable (too opaque) nor practical (problem too complex),
>nor conceptually possible (try to formalize the idea of
>"nice error messages").
Once again, I mostly agree. On the other hand, I have been
encountering some really interesting work in formal specifications
coming from the European computing community. I don't understand
all of what I see, but what I do understand is impressive. It is
that kind of work that makes me optimistic about the potential for
formal specifications in the future.
The people who follow us in creating the equivalent of software a
hundred years from now will look back on what we are doing today
with the same regard we give mathematicians in the time of Charlemagne.
Richard Riehle
http://www.adaworks.com
>
>
>
>Sent via Deja.com http://www.deja.com/
>Before you buy.
next prev parent reply other threads:[~1999-09-28 0:00 UTC|newest]
Thread overview: 69+ messages / expand[flat|nested] mbox.gz Atom feed top
1999-09-08 0:00 Array of Variant Records Question Bruce Detter
1999-09-08 0:00 ` Matthew Heaney
1999-09-08 0:00 ` Mike Silva
1999-09-08 0:00 ` Matthew Heaney
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Matthew Heaney
1999-09-09 0:00 ` Matthew Heaney
1999-09-09 0:00 ` Mark Lundquist
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Brian Rogoff
1999-09-13 0:00 ` Matthew Heaney
1999-09-13 0:00 ` Robert A Duff
1999-09-13 0:00 ` Matthew Heaney
1999-09-13 0:00 ` Brian Rogoff
1999-09-14 0:00 ` Robert Dewar
1999-09-14 0:00 ` Brian Rogoff
1999-09-14 0:00 ` Robert Dewar
1999-09-09 0:00 ` Matthew Heaney
1999-09-10 0:00 ` Mark Lundquist
1999-09-10 0:00 ` Matthew Heaney
1999-09-11 0:00 ` Robert Dewar
1999-09-10 0:00 ` Robert Dewar
1999-09-10 0:00 ` Mark Lundquist
1999-09-10 0:00 ` Matthew Heaney
1999-09-11 0:00 ` Jean-Pierre Rosen
1999-09-14 0:00 ` "cast away const" (was Re: Array of Variant Records Question...) Mark Lundquist
[not found] ` <wccd7viiv59.fsf@world.std.com>
1999-09-22 0:00 ` Array of Variant Records Question Robert I. Eachus
[not found] ` <7rrmqd$l89@drn.newsguy.com>
[not found] ` <wcciu59n2uf.fsf@world.std.com>
1999-09-22 0:00 ` Robert I. Eachus
1999-09-23 0:00 ` Robert Dewar
1999-09-23 0:00 ` Robert I. Eachus
1999-09-11 0:00 ` Richard D Riehle
1999-09-13 0:00 ` Hyman Rosen
1999-09-14 0:00 ` Mark Lundquist
[not found] ` <7roohh$s6r@dfw-ixnews7.ix.netcom.com>
[not found] ` <37e01168@news1.prserv.net>
[not found] ` <7rp86o$c6h@dfw-ixnews3.ix.netcom.com>
[not found] ` <37E18CC6.C8D431B@rational.com>
[not found] ` <7rs8bn$s6@dfw-ixnews4.ix.netcom.com>
[not found] ` <wccemfxn15s.fsf@world.std.com>
1999-09-22 0:00 ` 'constant functions' and access constant params (was Re: Array of Variant Records Question...) Richard D Riehle
[not found] ` <37e2e58c@news1.prserv.net>
1999-09-22 0:00 ` Richard D Riehle
1999-09-22 0:00 ` Matthew Heaney
1999-09-22 0:00 ` Richard D Riehle
1999-09-22 0:00 ` Matthew Heaney
1999-09-23 0:00 ` Vincent Marciante
1999-09-23 0:00 ` Matthew Heaney
1999-09-24 0:00 ` Robert A Duff
1999-09-25 0:00 ` Matthew Heaney
1999-09-27 0:00 ` Richard D Riehle
1999-09-27 0:00 ` Richard D Riehle
1999-09-27 0:00 ` David Kristola
1999-09-22 0:00 ` Matthew Heaney
1999-09-23 0:00 ` Robert Dewar
1999-09-27 0:00 ` Richard D Riehle
1999-09-28 0:00 ` Robert Dewar
1999-09-28 0:00 ` "Competence" (was: 'constant functions' and access constant params) Ted Dennison
1999-09-28 0:00 ` Robert Dewar
1999-09-28 0:00 ` 'constant functions' and access constant params (was Re: Array of Variant Records Question...) Robert Dewar
1999-09-28 0:00 ` Richard D Riehle [this message]
1999-09-29 0:00 ` Robert A Duff
1999-09-29 0:00 ` Robert Dewar
1999-09-22 0:00 ` Mark Lundquist
1999-09-22 0:00 ` Mark Lundquist
1999-09-10 0:00 ` Proposed Ada features " Mark Lundquist
1999-09-10 0:00 ` Matthew Heaney
1999-09-10 0:00 ` tmoran
1999-09-09 0:00 ` Array of Variant Records Question Nick Roberts
1999-09-09 0:00 ` Robert Dewar
1999-09-09 0:00 ` Tucker Taft
1999-09-10 0:00 ` Nick Roberts
1999-09-08 0:00 ` Ted Dennison
1999-09-08 0:00 ` Thank you Bruce Detter
1999-09-08 0:00 ` Martin C. Carlisle
1999-09-08 0:00 ` Array of Variant Records Question Martin C. Carlisle
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox