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.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,7a7040918881fd02 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2002-01-12 11:51:28 PST Path: archiver1.google.com!news1.google.com!sn-xit-02!supernews.com!newsfeed.direct.ca!look.ca!brick.direct.ca!brie.direct.ca.POSTED!not-for-mail Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset=us-ascii; format=flowed From: FGD MIME-Version: 1.0 Message-ID: <3C409568.4000102@look.ca> NNTP-Posting-Date: Sat, 12 Jan 2002 11:48:06 PST NNTP-Posting-Host: 209.148.71.184 Newsgroups: comp.lang.ada Organization: Look Communications - http://www.look.ca References: <3C3E8438.E780D942@adaworks.com> <3C3F45EE.7030808@look.ca> <3C3FE630.BDB27416@adaworks.com> Subject: Re: Assertions in the Next Ada Standard User-Agent: Mozilla/5.0 (Windows; U; WinNT4.0; en-US; rv:0.9.4) Gecko/20011128 Netscape6/6.2.1 X-Accept-Language: en-us X-Complaints-To: abuse@look.ca X-Trace: brie.direct.ca 1010864886 209.148.71.184 (Sat, 12 Jan 2002 11:48:06 PST) Date: Sat, 12 Jan 2002 14:58:32 -0500 Xref: archiver1.google.com comp.lang.ada:18833 Date: 2002-01-12T14:58:32-05:00 List-Id: Ah! I see now that your proposal is deeper than what I originally thought it was. I see also that it does addresses some very real issues of Ada. As you point out yourself, when it comes to incorporating them in the current Ada framework, invariants and pre-/post-conditions are quite different. Invariants are connected to types whereas conditions pertain to subprograms and their parameters. Consider dividing it in two related proposals to avoid opposition to one reject the other. Invariants constitute a "type improvement" as I would have said in my first reply. As such they are desirable, they provide a nice way of defining disconnected ranges and imposing constraints on type discriminants for example. Safety is an issue, but we know enough to work around it. The sublanguage of assertions should be constrained so that it cannot describe conditions which are not polytime---we know how to do that. More severe restrictions will probably be imposed, and very severe restrictions should apply if some kind of non-static assertions are to be allowed. Since the sublanguage of assertions should contain boolean variables and all propositional connectives, the problem of deciding whether or not a particular assertion is ever true is NP-complete. Thus one cannot reasonably expect compile time warnings for all such conditions. Some may object to that, but I consider this to be the programmer's problem. From my perspective, invariants have many merits. The most important is that it provides a uniform way of implementing all the type improvements I ever thought of in a uniform way. I'm still not sure about pre-/post-conditions. Right now, it seems to me that the associated complexities outnumber the benefits and I'm still curious about practical applications... -- Frank