Re: {Pre,Post}conditions and side effects

[Brad Moore <brad.moore@shaw.ca>]

On 14-12-22 12:38 PM, sbelmont700@gmail.com wrote:
> 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).

The value designated by X is a global variable though.

In the proposal for the Global aspect which appeared in a paper at the 
most recent HILT conference, you would not be allowed to specify

function P return Boolean
    with Global => null;

for this case, as the value designated by Some_Ptr_Type actually is a 
global variable.

You could however write;

   function P return Boolean
      with Global => (in out => Some_Ptr_Type);

However, this function now obviously has side effects


>
> 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.

I don't see anything being broken here. Some_Program still honours it's 
contract, and does what it says it will do. The contract of Some_Program 
doesn't impact the Insane procedure's contract. You haven't shown any 
contract for Insane, so for all we know, it has no contract, and do 
anything, including what you have here.


Brad

>
> -sb
>