Re: {Pre,Post}conditions and side effects

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Thu, 7 May 2015 12:06:29 +0200, Stefan.Lucks@uni-weimar.de wrote:

> On Wed, 6 May 2015, Randy Brukardt wrote:
> 
>> I don't believe that checks in Ada (of any kind) should ever be turned off.
> 
> Here, I heavily disagree. Often, checking relevant properties is much to 
> expensive to perform the checks them in production code.

Merely a confusion of checks with code. There is no such thing as runtime
correctness check, there is only run time code. You can neither remove
functional code nor spoil your program with non-functional code, especially
with one that would break the behavior.

> A simple example is binary search over a sorted array. The precondition 
> requires the array to be sorted.

And what does it mean for the behavior? If unsorted input is *valid* and
*must* raise exception (contracted behavior) then you cannot remove code
*implementing* this behavior.

Consider this client program:

declare
   X : Element;
begin
   X := Search (Data, Key);
   begin
       null;
   exception
       when Not_Sorted_Error =>
          X := Search (Sort (Data), Key);
   end;
end;

Is this code correct?

> Actually, one thing I am missing from Ada 2012 is a convenient and 
> fine-grained way to tell the compiler which pre- and postconditions and 
> invariants are to be checked, and which checks are to be skipped.

There shall be no dynamic predicates at all. They are inherently
inconsistent. No program shall evaluate correctness of its own. No
executable code shall be put into declarations.

> Most urgently, I would expect an option to skip checking ordinary pre- and 
> postconditions, without skipping those that explicitly raise some 
> exceptions. The point is, these two forms of precondition are semantically 
> totally different:
> 
> The semantic of a plain precondition is essentially:
> 
>    * If I a True, the postcondition will hold.
>      Never call the subprogram if I am false!!!
>      Otherwise, the subprogram might do anything.
> 
> This is a precondition in the "Design by Contract" sense.

This is just a precondition in any sense. It reads: the program P is
correct only if pre(P). Nothing else.
 
> The semantic of a precondition with something like "else raise 
> This_Exception" is
> 
>    * If I am True, the postcondition will hold
>      when the subprogram terminates.
>      If I am False, the subprogram will not do anything,
>      except for raising This_Exception.

This is not a precondition this is a contracted behavior that mandates
certain kind of output (exception) for certain kind of input (unsorted
array).
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de