Re: {Pre,Post}conditions and side effects

["Randy Brukardt" <randy@rrsoftware.com>]

"Peter Chapin" <PChapin@vtc.vsc.edu> wrote in message 
news:alpine.CYG.2.11.1504241811360.5268@WIL414CHAPIN.vtc.vsc.edu...
...
> In a correct program all assertions should always be true.

Sure, but that applies to lots of other things, too. For instance, in a 
correct program, Constraint_Error or Program_Error should not be raised. But 
it still happens.

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

I disagree with this (see below).

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

I definitely disagree here. This example is essentially similar to the one 
given in the upcoming Corrigendum (3.2.4(41-51/4). In a case like this, the 
precondition (or predicates as in the example) *replace* the checks required 
by English text in the RM. There would no internal checks of correctness.

You are of course correct that no caller should call New_Line with a closed 
file, but that's irrelevant because it can happen anyway (there is no static 
way to prevent it). There has to be code somewhere to handle it. So, in such 
a case, a precondition serves two purposes: (1) to signal to the client what 
conditions are expected, and (2) to determine what happens if those 
conditions aren't met. (2) certainly is "essential program logic", at so far 
as one cannot meet the published specification of New_Line without it.

Ada prior to Ada 2012 has a problem in that the reasons an exception can be 
raised conflate the programmer mistakes with conditions that are impossible 
for the programmer to know (consider the difference between whether a file 
object is open vs. whether a file exists on the disk). Preconditions and 
predicates provide a way to separately specify the first kind of situation 
vs. the second kind. (Ultimately, one hopes, compilers will be able to 
eliminate much of the runtime checking associated with preconditions and 
predicates, which is not possible in the pre-Ada 2012 world.)

                                   Randy.