Re: {Pre,Post}conditions and side effects

["G.B." <bauhaus@futureapps.invalid>]

On 13.05.15 11:35, Dmitry A. Kazakov wrote:
> The
> proper design is a composite type Sorted_Array with an*invariant*  that
> ensures the array sorted.

This shifts responsibility.

Also, why does the array need to be sorted during
its entire life time? How do you know that?

A contract for Binary_Search could require that

(a) input data is any plain old array of numbers
(b) in sorted order, by "<="

Why require some fancy abstraction imposed on client code
because the supplier feels it to be the proper design,
reflecting his particular idea of design for his particular
idea of what the job really is, even though it is not his job?

What is the difference between

-  the use of a sorted array (by precondition)
    in one place and

-  the use of a sorted array (by invariant)
    in the very same place,

when there is only this place?

   Binary_Search (It : Num; Data : Ary)
     with Pre => Is_Sorted (Ary);

vs

   type Sorted_Array is private
      with Type_Invariant => Is_Sorted (Sorted_Array);

   Binary_Search (It : Num; Data : Sorted_Ary);

Does every single, isolated algorithm on data warrant
a corresponding type?

There is no context here. So, there is nothing that says
that keeping some array-like private composite in sorted
order would improve the client's design.

If customers should be told how to structure their data
so that the contract matches the supplier's design ideas
why not require that the client keep an index
for the array? Then, the supplier could create his
Binary_Search as Search, based on the properties of customer
built index... Which, then would get a suitable contract ...

I hope the shift in responsibility becomes apparent.

Every contract has to start from some reality. How could
a design be compared to another without knowing the exact
problem?