Re: {Pre,Post}conditions and side effects

[Peter Chapin <PChapin@vtc.vsc.edu>]

On Fri, 24 Apr 2015, Jacob Sparre Andersen wrote:

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

I think a servicable rule is this: If the program works as required, with 
all necessary checks still present, with all assertions removed, then we 
can say the assertions contain no essential program logic.

In a correct program all assertions should always be true.

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

Although the Dynamic_Predicate asserts that the matrix elements are all 
non-negative, this does not remove the program's obligation to include 
checks that no negative elements are added to the matrix. The assertion 
only exists to catch mistakes in those checks. It does not exist to 
actually *be* those checks. In that respect the assertion is not 
"essential program logic."

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

Similarly here the program is still obligated to only pass File objects to 
New_Line that represent open files. If the program accidentally passes an 
unopened file to New_Line the assertion will catch the logical error. 
However, the assertion should not take the place of earlier checks. Again 
the assertion is not essential program logic.

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

Yes, definitely wrong. On the other hand using something like

     with Pre => Is_Sorted(Source);

could be reasonable.

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

I agree that (1) and (2) are fine, but that doesn't mean the program 
should rely on the assertions for its proper functioning. The assertions 
check correctness; they don't implement it. Even if the assertions are 
removed, the program should still execute properly.

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

Because we often make mistakes and it's nice to have our thinking double 
checked. Also, of course, the assertions make our intentions known to 
tools, such as SPARK, that can automatically verify our code implements 
the conditions we are asserting.

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

Putting the check inside the subprogram is quite a different thing. That 
is part of your implementation of correctness. Since assertions should 
never fail, using the same exception for all of them isn't terrible. That 
said, the upcoming feature that allows different exceptions to be used 
when an assertion fails is nice too.

Peter