Re: {Pre,Post}conditions and side effects

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

On Fri, 24 Apr 2015, Randy Brukardt wrote:

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

In this case it's not the internal checks I mean. Hoisting the internal 
checks into preconditions makes sense to me, at least in certain (many?) 
cases. In my comments above I'm talking about checks occurring before 
New_Line is called.

Somewhere the programmer tried to open a file. If the programmer attempts 
to call New_Line without first verifying that the file opened 
successfully, that's a logical error in the program. Checking that 
Is_Open(File) is true provides some protection against such an error... 
regardless of if the check is a precondition or done inside the body of 
New_Line. Either way, in a correct program that check should never fail. 
The beauty of doing it in a precondition is that the "unnecessary" check 
can be removed by changing the assertion policy.

In contrast imagine a procedure that takes file and does some processing 
on it. Suppose the procedure raises some exception if the file has the 
wrong format. The programmer might decide that it's not wrong to call the 
procedure with an incorrectly formatted file, and let that be a matter for 
the procedure to worry about. In that case, adding the check as a 
precondition doesn't seem right; a correct program might call the 
procedure with a badly formatted file.

On the other hand if the programmer decides it's illogical to call the 
procedure with an incorrectly formatted file because the file has 
(supposedly) been verified previously, using a precondition to check the 
format makes sense.

Same procedure, same check... the sensibility of making the check a 
precondition depends on the context in which the procedure is used. In the 
first case the caller relies on the procedure to do the check. In the 
second case the procedure relies on the caller to do it. Ultimately it 
ends up being a design decision.

Peter