From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: *
X-Spam-Status: No, score=1.3 required=5.0 tests=BAYES_00,INVALID_MSGID,
	MSGID_RANDY autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,bd40601768eaf8fd
X-Google-Attributes: gid103376,public
From: Robert Dewar <robert_dewar@my-deja.com>
Subject: Re: 'constant functions' and access constant params (was Re: Array of
 Variant Records Question...)
Date: 1999/09/28
Message-ID: <7sqbt6$1la$1@nnrp1.deja.com>#1/1
X-Deja-AN: 530086074
References: <7r5vh3$imu1@svlss.lmms.lmco.com> <37d6a45c@news1.prserv.net>
 <eExB3.6$ZR.1146@news.wenet.net> <37d6ccb6@news1.prserv.net>
 <7r77i8$i08$1@nnrp1.deja.com> <37d7c116@news1.prserv.net>
 <7r8t21$ov5$1@nnrp1.deja.com> <37d822a1@news1.prserv.net>
 <7reg02$t83@dfw-ixnews6.ix.netcom.com> <37DE8D09.C863CBC9@rational.com>
 <7roohh$s6r@dfw-ixnews7.ix.netcom.com> <37e01168@news1.prserv.net>
 <7rp86o$c6h@dfw-ixnews3.ix.netcom.com> <37E18CC6.C8D431B@rational.com>
 <7rs8bn$s6@dfw-ixnews4.ix.netcom.com> <37e2e58c@news1.prserv.net>
 <7s9nd0$cbe@dfw-ixnews17.ix.netcom.com> <37e8e067@news1.prserv.net>
 <7sas3p$bfa@dfw-ixnews3.ix.netcom.com> <7sc6b6$c6m$1@nnrp1.deja.com>
 <7socka$6u4@dfw-ixnews19.ix.netcom.com>
X-Http-Proxy: 1.0 x23.deja.com:80 (Squid/1.1.22) for client 205.232.38.14
Organization: Deja.com - Before you buy.
X-Article-Creation-Date: Tue Sep 28 12:22:06 1999 GMT
X-MyDeja-Info: XMYDJUIDrobert_dewar
Newsgroups: comp.lang.ada
X-Http-User-Agent: Mozilla/4.04 [en] (OS/2; I)
Date: 1999-09-28T00:00:00+00:00
List-Id: <comp.lang.ada>

In article <7socka$6u4@dfw-ixnews19.ix.netcom.com>,
  Richard D Riehle <laoXhai@ix.netcom.com> wrote:
> In article <7sc6b6$c6m$1@nnrp1.deja.com>,
> 	Robert Dewar <robert_dewar@my-deja.com> wrote:
>
> >The answer is that without comments, the caller has not the
> >foggiest idea. Specifications in Ada give only the bearest
> >structural details on how to call a subprogram, they do not
> >give any hint as to what the subprogram is supposed to do!
>
> Exactly, Robert.  In the absence of assertions that can be
> checked by the compiler, comments are the only recourse. And
> you and I both agree about the problems of compiler-checked
> assertions.  An assertion can be more wrong than the program
itself.

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

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




Sent via Deja.com http://www.deja.com/
Before you buy.