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.1 required=5.0 tests=BAYES_00, PP_MIME_FAKE_ASCII_TEXT autolearn=no autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!gegeweb.org!news.ecp.fr!news.jacob-sparre.dk!loke.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Mon, 22 Dec 2014 17:46:28 -0600 Organization: Jacob Sparre Andersen Research & Innovation Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> NNTP-Posting-Host: rrsoftware.com X-Trace: loke.gir.dk 1419291989 5961 24.196.82.226 (22 Dec 2014 23:46:29 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Mon, 22 Dec 2014 23:46:29 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-RFC2646: Format=Flowed; Original X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 Xref: news.eternal-september.org comp.lang.ada:24201 Date: 2014-12-22T17:46:28-06:00 List-Id: wrote in message news:c17f6550-1cc8-4ef7-8477-4512d16d294a@googlegroups.com... On Monday, December 22, 2014 11:22:29 AM UTC-5, Jean François Martinez wrote: >> Perhaps it would have been a good idea to have a No_Side_Effects aspect >> ... >It's more than just global variables, though. Your condition might be >thusly ludicrous: > >function P return Boolean is > x : Some_Ptr_Type := new Integer'(42); The storage pool of Some_Ptr_Type is a global variable. It would have to be mentioned in the Global aspect, else this allocator is illegal. >begin > return True; >exception > when others => Some_Task.Blocking_Rendezous; There's also an aspect "Potentially_Blocking" under development, to cover this case. >end P; >Now you've got a function that doesn't access any global variables, but not >only randomly >exhaust the heap, As noted, the heap is a global variable, so that couldn't happen with Global => null. >but also permanently blocks the thread, so you are right back where you >started. That's already a Bounded Error (see 11.4.2(23.1/3)). One presumes that if pragma Detect_Blocking is used, it will always raise Program_Error. Plus there would be the aspect noted above, for static checking. >You end up needing all the same rules and restrictions as pragma Pure, >which means >you might as well just be beholden to pragma Pure to begin with (or use >qualified >expressions). Actually, you need quite a bit more that Pure. Pure allows dereferences of access values, which can't be allowed willy-nilly (the pool is a global variable, after all). Plus Pure only applies to complete packages, which is way too unwieldy for assertions (typically an assertion depends on predicate functions defined with an ADT, we surely don't want to have to make the entire ADT Pure just to use assertions). >But more to the point, there is no escaping that disabling/enabling checks >will cause the >program to function differently; that is, after all, the entire point. >What constitutes >'correctness' is only in the eyes of the programmer. Ergo: You're right here, and I've always thought that is a problem. It's one reason that a package author can prevent some or all assertions from being disabled in the package. >procedure Some_Subprogram is null with Pre => false; > >procedure Insane is >begin > Some_Subprogram; > raise Program_Error; >exception > when others => Continue_Running; >end Insane; > >No globals, but it still "breaks" when checks are disabled. A much better example is an implementation that has implemented the containers using preconditions rather than explicit checks. For instance: procedure Replace_Element (Container : in out Vector; Position : in Cursor; New_Item : in Element_Type); with Pre'Class => (if Tampering_With_Elements_Prohibited (Container) then raise Program_Error) and then (if Position = No_Element then raise Constraint_Error) and then (if not Cursor_Belongs_To_Container (Container, Position) then raise Program_Error; If this is called with preconditions ignored, the required semantives of Replace_Element won't happen [because the checks for the various exceptions won't happen - no one is going to repeat the precondition checks in the body - if that was required, the precondition is worthless]. [Note: This precondition uses a couple of predicates that aren't defined in the Ada 2012 containers, but should have been. Most likely, the next version of Ada will rewrite the containers this way, it will get rid of a lot of text in the Standard.] Randy.