Re: function Is_Open (File : File_Type) return Boolean; :Text_io

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 28 Oct 2015 16:07:55 -0400, Bob Duff wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
> 
>> On Tue, 27 Oct 2015 09:30:54 -0400, Bob Duff wrote:
>>
>>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> writes:
>>> 
>>>> On Mon, 26 Oct 2015 18:48:51 -0400, Bob Duff wrote:
>>>>
>>>>> comicfanzine@gmail.com writes:
>>>>> 
>>>>>> Can someone please show my a code in which this function is used , i'm
>>>>>> lost , thanks .
>>>>> 
>>>>> Most code is written so that it is statically known whether a file is
>>>>> open, so Is_Open is close to useless.  Not entirely useless -- you might
>>>>> use it in an assertion, such as:
>>>>> 
>>>>>     subtype Open_File is File with Predicate => Is_Open(Open_File);
>>>>
>>>> In order to have the Constraint_Error exception instead of Status_Error?
>>> 
>>> No, in order to document the fact that a certain formal parameter must
>>> be open, and in order to prove things statically.  If a procedure takes
>>> "F: Open_File", then we can easily prove that writes to F within that
>>> procedure do not raise Status_Error.
>>
>> That does not make sense either. There is nothing in the procedure itself 
>> that would prevent raising Status_Error. Everything is on the caller's 
>> side. How do you know if some callers would not appreciate Status_Error as 
>> a possible outcome? Looks like poor design to me.
> 
> I don't understand what you're getting at.  We can, of course, make the
> Predicate raise Status_Error if we want.  But the point is to prove
> statically that files are open when we want to write to them.  The
> example of the log file ("We want to write on the file if and only if it
> is open") is unusual.  The far more common case is:  "We want to write
> on the file.  No 'if's about it.  Therefore, the file had better be
> open."

No doubt about it. That does not help to understand how substituting one
exception for another changes anything. A caller still can pass a closed
file in both cases.

>> Anyway proving either of the conditions A) not raising Constraint_Error, B) 
>> not raising Status_Error look equally hard.
> 
> I think it is important that proofs be localized.  E.g. proving
> something about P should not require examining all call sites
> that call P.  Suppose we have:
> 
>     procedure P(F: in out Open_File) is
>     begin
>         ...
>         Put(F, ...);
>         ...
>     end P;

You cannot prove that P does not raise Constraint_Error, in fact it is the
opposite, it does raise, when F is not open.

You could only prove that *if* F is open then Constraint_Error is not
raised. Likewise you could prove that if F is open then Status_Error is not
raised, as locally as for another one. It is just same.

> At the call to Put, we can (informally) prove that F is open.
> (This requires knowing certain things, such as Is_Open not having
> side effects, and nobody is sneakily calling Close in the "..." parts.
> To automate such a proof, you'd need some way of expressing such
> things -- e.g. globals annotations as supported by SPARK 2014.)
> 
> The Predicate is pushing the responsibility of opening the file to the
> caller.  That's a good thing, because the caller likely knows:
> 
>     procedure Caller(Name: String) is
>         F: File_Type;
>     begin
>         Open(F, Name, ...);
>         P(F);
> 
> We know at "P(F)" that F is open because we just opened it.
> Both of these proofs are local and static.  There's no issue
> about Constraint_Error versus Assertion_Failure versus Status_Error,
> because we know that no exception is raised.
> 
> Without the Predicate (or an equivalent precondition), the proofs
> fall apart.

They don't because Text_IO procedures have contracts not to raise
Status_Error. This is fully equivalent. You cannot say that they don't have
contracts because your proof is necessarily based on these implied
contracts.

> I'd say that's the main point of contracts -- to allow localized
> reasoning about programs.

Yes, and these contracts exist as documented in ARM. The only problem is
that they are not explicit.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de