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-11 17:12:02 PST Path: archiver1.google.com!news1.google.com!sn-xit-02!supernews.com!newsfeed.direct.ca!look.ca!fu-berlin.de!uni-berlin.de!ppp-1-176.cvx1.telinco.NET!not-for-mail From: "Nick Roberts" Newsgroups: comp.lang.ada Subject: Re: Assertions in the Next Ada Standard Date: Fri, 11 Jan 2002 23:28:59 -0000 Message-ID: References: <3C3E8438.E780D942@adaworks.com> NNTP-Posting-Host: ppp-1-176.cvx1.telinco.net (212.1.136.176) X-Trace: fu-berlin.de 1010797919 29866095 212.1.136.176 (16 [25716]) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 5.50.4133.2400 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4133.2400 Xref: archiver1.google.com comp.lang.ada:18805 Date: 2002-01-11T23:28:59+00:00 List-Id: "Dale Stanbrough" wrote in message news:dstanbro-07F79B.20222311012002@mec2.bigpond.net.au... > Richard Riehle wrote: > > > I am hoping to see something like pre-conditions, post-conditions, > > and invariants in the next revision of Ada. I would be pleased if > > we simply adopted the wording already used in Eiffel: require, > > ensure, and invariant, but I am not intractable about the terminology. > > > > So, who is working on the proposal for this? > > > > Richard Riehle > > I think another valuable one would be "assume" which is an > assertion that allows the compiler to invoke any code > optimisation it can. A counter-argument to the addition of any of these facilities being added can be illustrated in the following procedure: subtype Must_Be_True is Boolean range True..True; procedure P (...) is ... [invar.]: constant ... := [i. expr.]; --D [a. name]: constant Must_Be_True := [assumption]; --D begin if [debug] and then not [pre-conditions] then raise [excep.]; end if; --D ... if [debug] and then not [post-conditions] then raise [excep.]; end if; --D if [debug] and then not [invar.] /= [i. expr.] then raise [excep.]; end if; --D end P; This procedure demonstrates how pre-conditions, post-conditions, invariants, and assumptions can all be programmed in existing Ada. For efficiency, certain assumptions may be made of the compiler, in terms of static evaluation and/or dead code removal (but these would effectively be required for the efficient implementation of the proposed pragmas). A procedure such as P could be made a 'wrapper' to another Q (which does the real work). P could then be replaced by Q when debugging is completed. Alternatively, a simple text modification tool could be used to remove all lines containing "--D". It may seem like an extreme form of Blimpism to argue against the suggested pragmas, but I have found in real code that I often wanted to code quite com plicated test routines into subprograms for debugging purposes. I can't believe I'm the only one who has found this. The proposed pragmas would be of little advantage in these cases (they can only take an expression). Sometimes, what sounds like a great idea turns out not to be so brilliant when you closely look at it. And sometimes, it turns out that a bigger idea subsumes it anyway. (Read on... ;-) One little thing that (I think there is wide agreement on) would be most welcome would be a 'raise ... when ...;' statement: procedure P (...) is ... [invar.]: constant ... := [i. expr.]; --D [a. name]: constant Must_Be_True := [assumption]; --D begin raise [excep.] when [debug] and then not [pre-conditions]; --D ... raise [excep.] when [debug] and then not [post-conditions]; --D raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; --D end P; However, a major new feature that I would like to see introduced at the next revision would be a provision for 'separation of concerns'. As a 'straw man', this might work something like as follows. Each declarative item which is or can contain a subprogram requires a completion in Ada 95. In the case of a subprogram, the completion (the body) is permitted to be the declaration also. My proposed facility would permit multiple completions for a subprogram (separately declared). The facility would always apply to a library unit: if the unit is a package, all the subprograms in the package would be permitted multiple completions. For example, the declaration of a library procedure P might be declared: procedure P ([parameters]); A new kind of library-level declaration would allow a set of different 'aspects' to be declared, together with a pattern for the way in which they are applied to subprograms. E.g.: procedure P ([parameters]) is separate (Debugging.Before, Main_Function, Debugging.After); This declares that P has three separate completions, named Debugging.Before, Main_Function, Debugging.After. There is also a fourth optional completion, Debugging, which is a kind of 'parent' to Debugging.Before and Debugging.After. Whenever P is called, all three declared completions will be called, in the order declared. The fourth completion, Debugging, will also be called, before those for Debugging.Before and Debugging.After. The completions would look similar to current Ada subunits: separate (Main_Function) procedure P ([parameters]) is ... begin ... end P; A completion for Debugging allows for shared declarations, and an initialisation: separate (Debugging) procedure P ([parameters]) is [invar.]: constant ... := [i. expr.]; [a. name]: constant Must_Be_True := [assumption]; begin null; end P; This body will be executed before those for Debugging.Before and Debugging.After (to provide a set of common declarations for them, and possibly an initialisation). Finally, we must separately complete the final two outstanding bodies: separate (Debugging.Before) procedure P ([parameters]) is begin raise [excep.] when [debug] and then not [pre-conditions]; end P; separate (Debugging.After) procedure P ([parameters]) is begin raise [excep.] when [debug] and then not [post-conditions]; raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; end P; Things get a little more complex with packages. Here we define a pattern that applies to all the subprograms the package contains implicitly. E.g.: package My_Stuff.Utilities is procedure P (...); procedure Q (...); ... end; package My_Stuff.Utilities is separate (Debugging.Before, Main_Function, Debugging.After); There are now three bodies required to fully complete this package, one for each of the three aspects. I have also chosen to make the package a child, to illustrate naming within hierarchies. Within each of the package bodies, the completions of the given aspect of each of the package's subprograms must be given. E.g.: separate (Main_Function) package My_Stuff.Utilities body is procedure P (...) is ... begin ... -- implementation of P's main functionality end; procedure Q (...) is separate; end; I have made the completion of Q a normal subunit, to illustrate the naming scheme: separate (My_Stuff.Utilities.Main_Function) procedure Q (...) is ... end Q; There would then be: separate (Debugging) package My_Stuff.Utilities is -- any declarations common to Debugging.Before and Debugging.After begin -- any initialisation code end; separate (Debugging.Before) package My_Stuff.Utilities is procedure P (...) is begin raise [excep.] when [debug] and then not [pre-conditions]; end P; procedure Q (...) is null; end; separate (Debugging.After) package My_Stuff.Utilities is procedure P (...) is begin raise [excep.] when [debug] and then not [post-conditions]; raise [excep.] when [debug] and then not [invar.] /= [i. expr.]; end P; procedure Q (...) is null; end; I have invented a new form of null procedure, which would probably be handy. (A bit analogous to the new form of null record declaration for types.) Finally, each completion would be permitted to be a completion by renaming, as normal. In many cases, this would greatly facilitate code re-use (if the design is good). Obviously there are a lot of details to fill in on this one. But hopefully it can be seen how it solves the problem of the separation of debugging code, as well as helping to solve the problems of code separation in a much wider way. -- Best wishes, Nick Roberts