Re: {Pre,Post}conditions and side effects

[Stefan.Lucks@uni-weimar.de]

[-- Attachment #1: Type: TEXT/PLAIN, Size: 3647 bytes --]

On Thu, 7 May 2015, Dmitry A. Kazakov wrote:

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

Agreed!

At best, a run time check is some sort of a testing harness. It is useless 
to show the correctness of a program, but it can help to discover bugs.

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

[...] I'll slightly rewrite your client program -- I believe, the 
exception handler was at the wrong place.

   declare
     X : Extended_Index_Type;
   begin
     X := Search (Data, Key);
   exception
       when Not_Sorted_Error | Assertion_Error =>
          X := Search (Sort (Data), Key);
   end;

> Is this code correct?

It depends on the specification of "Sort".

Specification 1:

   function Search(Data: Array_Type; Key: Value_Type)
                      return Extended_Index_Type with
     pre  => Sorted(Data),
     post => (if Data(Search'Result) in Data'Range
              then Data(Search'Result)=Value
              else Search'Result = No_Index and then
                   (for all I in Data'Range => Data(I) /= Key));

The expression "Sorted(Data)" is a precondition. Every client which can 
possibly violate the precondition is buggy. Thus, the above code is buggy. 
(Or otherwise, the exception handler is dead code.)

One property of a proper precondition (or postcondition or ...) is that 
disabling the check does not change the functional behaviour of correct 
programs.

Specification 2:

   function Search(Data: Array_Type; Key: Value_Type)
                      return Extended_Index_Type with
     pre  => (Sorted(Data) or else raise Not_Sorted_Error),
     post => (if Data(Search'Result) in A'Range
              then Data(Search'Result)=Value
              else Search'Result = No_Index and then
                   (for all I in Data'Range => Data(I) /= Key));

The expression following "pre" is "contracted behaviour" as you put it. 
The code above is correct, and disabling the check must be prohibited, 
because it would break correct programs. Which is why I wrote the following:

>> Most urgently, I would expect an option to skip checking ordinary pre- and
>> postconditions, without skipping those that explicitly raise some
>> exceptions.

In other words, I want to be able to switch of proper preconditions (and 
postconditions, whatever) without affecting contracted behaviour.

I depreciate the usage of the word "precondition" for the expression 
following "pre" in spec 2. But I will not fight about names.

Furthermore, I am quite happy with Ada allowing to specify contracted 
behaviour, even I would have prefered use an aspect of its own for 
contraced behaviour. The "pre" aspect should better be have been reserved 
for proper preconditions. But this appears too late now. On the other 
hand, it would not be too late to support disabling proper preconditions 
without changing contracted behaviour.

Stefan


------  I  love  the  taste  of  Cryptanalysis  in  the morning!  ------
uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks
--Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universität Weimar, Germany--