Re: {Pre,Post}conditions and side effects

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 12.05.15 03:03, Randy Brukardt wrote:
> No, I'd still argue your code is broken. If*you*  know that some object is
> always sorted, then*you*  should tell the compiler that with an appropriate
> predicate:
>
>      subtype Sorted_Array is Some_Array
>          with Dynamic_Predicate => Is_Sorted (Sorted_Array);
>
>     My_Array : Sorted_Array := ...;

There is no formal specification of what Is_Sorted should be.
But there should be one, somewhere (other than a comment), even
when the formal specification involves quite a bit.

How is a client of Sorted_Array to know what Is_Sorted should be?

And if the contract has that information hidden in RM style commentary,
how would the cost of keeping Some_Array sorted plus having it checked
be so different from the supplier side cost of checking that assumption?

This sounds like shifting responsibility for commercial reasons, again.