Re: {Pre,Post}conditions and side effects

[Bob Duff <bobduff@theworld.com>]

Jacob Sparre Andersen <jacob@jacob-sparre.dk> writes:

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

I think what Peter meant by "essential program logic" is code that,
if deleted from the program, would cause the program to malfunction.

> 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);

The assertions in (1) and (2) are not "essential program logic"; if you
delete them, the program will still work properly.  That's fine -- you
should write assertions so that deleting them from a correct program
will have no effect.

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

That's illegal.  (I assume Sort is a procedure with an 'in out'
parameter that sorts in place.  Passing Source (an 'in') parameter is
illegal.)  I suppose you could make Source 'in out', but as you say
below that's a very bad idea.

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

Agreed.  (3) is trying to put "essential program logic" in an assertion,
which is a 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?

Same reason we put comments in the code.  Comments are not "essential
program logic" in the sense defined above -- if you delete all the
comments, the program will still work.  But we still want comments.
Likewise, one should normally write assertions (like Pre and Predicate)
so the program still works if they are deleted.

Assertions are like comments, except we have a higher confidence
that they are actually true.

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

You can say:

    Pre => X = Y or else raise X_Not_Equal_To_Y;

- Bob