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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,cd1591f986baca62 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-03-14 09:20:14 PST Path: supernews.google.com!sn-xit-03!supernews.com!freenix!sunqbc.risq.qc.ca!news.maxwell.syr.edu!news.mindspring.net!not-for-mail From: Lao Xiao Hai Newsgroups: comp.lang.ada Subject: Re: AdaYY; Assertions? Date: Wed, 14 Mar 2001 09:17:14 -0800 Organization: AdaWorks Software Engineering Message-ID: <3AAFA79A.66F86B99@ix.netcom.com> References: <3AAA9B7A.36B601F0@ix.netcom.com> Reply-To: richard@adaworks.com NNTP-Posting-Host: 3f.35.b5.5b Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Server-Date: 14 Mar 2001 17:16:27 GMT X-Mailer: Mozilla 4.7 [en] (Win98; I) X-Accept-Language: en Xref: supernews.google.com comp.lang.ada:5725 Date: 2001-03-14T17:16:27+00:00 List-Id: Stephen Leake wrote: > Lao Xiao Hai writes: > > So what is your proposal? At this point, my proposal is the addition of a pre-, post-, and invariant capability to the Ada language, similar to that found in Eiffel. I fully realize that it is easier to propose something than to figure out how to make it work. The general mechanism, as I see it. Pre-conditions These could be applied to a subprogram or a data type. Since data types already have the benefit of range constraints and other features of the type model, this might be superfluous. However, some properties are not as simple as range constraints. What happens when a pre-condition fails. Eiffel has two basic options: 1) handle and leave scope (as well as potentially propogating) 2) handle the exception and retry I personally have a problem with the retry semantics, but it seems to be effective with Eiffel. Not sure about all the implications for Ada. I do believe that run-time is the wrong place to find a pre-condition error. It is too late in the process. However, if the pre-condition error can be detected at run-time and corrective action other than an exception handler be taken, perhaps it has some virtue. Post-conditions Many of the same issues apply as for pre-conditions. However, what to do if a post-condition fails could be quite different, even problematic. Invariants These should apply to the type/class. Invariants should be inherited. Eiffel allows overriding of the invariant (they call it something else, but same general effect). Ada poses another problem. Should be have an invariant to applies to an entire package rather than just a type? This problem originates in the Ada model of enclosing a type declaration within a package. Other problems It is easy to craft a self-contradictory assertion. It would be too much overhead, and probably impossible, to include some kind of theorem prover in the compiler to detect such assertions. Can assertions contribute to safer code? That is debatable. Probably some assertions are inherently more safe. But to rely on assertions, for safety-critical software, might pose some serious considerations. I realize that Bertrand Meyer and others who espouse the Design By Contract philosophy have made a strong case for the value of assertions in constructing safer software, but I believe the jury is still out. Given my doubts, why do I still support the idea. It seems to me that a conservative approach to this issue, for Ada, can have some real benefits. If we adhere to some of the existing syntactic rules and some of the existing semantics of the language, pre-, post-, and invariant conditions can be subjected to some rigor during the compile process. Trivial example, complex boolean expressions in Ada require parentheses. I don't want to seem as if I believe this is a simple change to the language. Tucker seems to agree with the general proposition, and he is much smarter about this kind of thing than I. There is a need for more technical input, more ideas, more criticism, before deciding on this course. However, it is a serious enough issue that it deserves our attention. As I stated earlier, more and more textbooks are publishing algorithms, examples of classes, and other pseudocode fragments in which assertions are part of the code. Ada can benefit from being more compatible with those examples, I believe. Richard Riehle Lao Xiao Hai