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 14:44:57 PST Path: archiver1.google.com!news1.google.com!sn-xit-02!supernews.com!isdnet!newsfeed.cwix.com!newsfeed1.cidera.com!Cidera!cyclone.socal.rr.com!cyclone3.kc.rr.com!news3.kc.rr.com!typhoon.san.rr.com!not-for-mail Message-ID: <3C40BC71.F3009405@san.rr.com> From: Darren New X-Mailer: Mozilla 4.77 [en] (Windows NT 5.0; U) X-Accept-Language: en MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Assertions in the Next Ada Standard References: <3C3E8438.E780D942@adaworks.com> <3C3F45EE.7030808@look.ca> <3C3FE630.BDB27416@adaworks.com> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Date: Sat, 12 Jan 2002 22:45:46 GMT NNTP-Posting-Host: 66.75.151.160 X-Complaints-To: abuse@rr.com X-Trace: typhoon.san.rr.com 1010875546 66.75.151.160 (Sat, 12 Jan 2002 14:45:46 PST) NNTP-Posting-Date: Sat, 12 Jan 2002 14:45:46 PST Organization: Road Runner Xref: archiver1.google.com comp.lang.ada:18838 Date: 2002-01-12T22:45:46+00:00 List-Id: Richard Riehle wrote: > For a type, an invariant declaration simply adds some additional rules > for that type. For example, one cannot declare a discontinous range > for a numeric type, but an invariant might state that a value of that > numeric type cannot ever be zero. This would be stated (asserted) > in the package specfication. For other types, boolean expressions > could be declared that would further constrain a type with a more > rigorous invariant. Actually, if you wanted to follow the Eiffel model for this, the invariant would be that the values of the type have to obey the invariants unless you're running the body of a primitive operation of that type. That is, if you had something like type x is new integer; invariant x /= 0; -- Or whatever syntax procedure increment(value : in out x) is begin value := value + 1; if value = 0 then value = 1; end if; end increment; then it would be legal to call increment with a value of -1, and the first line of increment would not cause an exception. > Pre-conditions and post-conditions would be part of the declaration of > each subprogram. Post-conditions are particularly worthwhile because > there is, for access to composite type parameters, potential for > side-effects > that might be unknown to the client of a specification. A post-condition > can guarantee there are no unchecked side-effects. It's really, really difficult to rule out side-effects with post-conditions. Indeed, some of the hardest post-conditions are those of side-effects. For example, you do a Put on a file, and the postcondition is very unlikely to be able to express what that actually does in terms of future Gets. > Pre-conditions might be less useful given many of the controls already > in place for parameter lists in subprograms. However, one might declare > a pre-condition that prevents a subprogram from executing if some > combination of parameters is invalid. That's generally what they're good for, yes. Like, don't pop empty stacks, don't real closed files, and stuff like that. Most any subprogram that raises an exception specific to the package would be using preconditions instead. > Now to the problems. First, there is the danger that one might be able to > construct a self-cancelling boolean expresssion as an assertion. Not sure what a "self-cancelling" boolean expression is. You mean a tautology? Or a negation of a tautology? > We > are not very sophisticated in the automated theorem proving in the > world of computer science, even though there is some progress. Actually, "we" are. It's just a very difficult problem, with lots of NP stuff involved. > The > person who constructs an assertion might be tempted to rely on it > to the exclusion of more careful inspection. Indeed. That's part of the point of doing it, at least for preconditions. If your precondition is "don't pop an empty stack", then you don't have to implement pop to handle the case of an empty stack. This is actually a good thing. Well, not that the person won't "inspect", but that the implementation will be more straightforward. > Second, in an inheritance > scheme, what do we do about either inheriting or overriding a assertion. > This problem is non-trivial. I am not sure I have the answer, and that > is why there is a need for more people thinking about this than we have > so far. This is pretty well considered in Eiffel, actually. Indeed, the strength of Eiffel's "DbC" assertions over those of just inlining boolean checks is that they *do* get inherited in the "right way". -- Darren New San Diego, CA, USA (PST). Cryptokeys on demand. The opposite of always is sometimes. The opposite of never is sometimes.