Re: {Pre,Post}conditions and side effects

["Randy Brukardt" <randy@rrsoftware.com>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 3783 bytes --]

<sbelmont700@gmail.com> 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.