Re: {Pre,Post}conditions and side effects

[Jacob Sparre Andersen <jacob@jacob-sparre.dk>]

Robert A Duff <bobduff@shell01.TheWorld.com> writes:
> Peter Chapin <PChapin@vtc.vsc.edu> writes:

>> ... Thus putting anything resembling essential program logic in an
>> assertion is, of course, just wrong.
>
> Yes.

But when are you putting "essential program logic" in an assertion?

1) subtype Non_Negative_Matrix is Ada.Numerics.Real_Arrays.Real_Matrix
     with Dynamic_Predicate
            => (Non_Negative_Matrix'First (1) = 1) and
               (Non_Negative_Matrix'First (2) = 1) and
               (for all E of Non_Negative_Matrix => E >= 0.0);

2) procedure New_Line (File : in File_Type)
     with Pre => Is_Open (File) and then
                 Mode (File) in (Out_File | Append_File);

3) function Binary_Search (Source : in List;
                           Key    : in Keys) return Values
     with Pre => Sort (Source); --  Sorts Source if it isn't already sorted.

I consider examples (1) and (2) fine, but example (3) a very bad idea.

At the same time, I know that my application may fail silently if the
assertion in example (1) isn't true.

When it comes to example (2), I expect that the operating system (if
nothing else) will make sure that my application doesn't fail silently
if the assertion isn't true.

But I dislike banning "essential program logic" in assertions, as any
assertion is program logic.  And if it isn't essential, why should it be
there?

One problem I have with assertion aspects is that I get the same
exception no matter which mistake I have made.  If I put the check
inside a subprogram instead of in its profile, I can get more clear
information about which kinds of mistakes I make.

Greetings,

Jacob
-- 
"Any politician with a live opposition does not understand
 how to make proper use of the true instruments of politics."