Re: {Pre,Post}conditions and side effects

[sbelmont700@gmail.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 and only functions labelled with this pragma would be allowed in pre/post conditions.  Such functions would not be able to modify global variables and would be restricted to invoking only functions/procedures marked with this aspect.   This is somewhat akin with the restrictions for packages marked with elaboration pragmas or with pragmas realated to distributed system annex. In both a package may only with a "lower or equal" package.
> 

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);
begin
   return True;
exception
   when others => Some_Task.Blocking_Rendezous;
end P;

Now you've got a function that doesn't access any global variables, but not only randomly exhaust the heap, but also permanently blocks the thread, so you are right back where you started.  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).

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:

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.

-sb