From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable autolearn_force=no version=3.4.4 Path: eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail From: Bob Duff Newsgroups: comp.lang.ada Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io Date: Wed, 28 Oct 2015 16:07:55 -0400 Organization: A noiseless patient Spider Message-ID: <87h9la3gf8.fsf@theworld.com> References: <87twpd2qlo.fsf@theworld.com> <1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net> <87pp0030c1.fsf@theworld.com> <135hiczk56x02.1xixcme8btbl4.dlg@40tude.net> Mime-Version: 1.0 Content-Type: text/plain Injection-Info: mx02.eternal-september.org; posting-host="9e4a124ceb0e8a60134d2d30eac9ea6f"; logging-data="31779"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX19FdVBEW6GZYkFbmcIyL1q9" User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.3 (gnu/linux) Cancel-Lock: sha1:/wBXCsHjaZdUU6YNOb+zHA3aYy4= sha1:M2IT8LTZ/REttbOyy1m/hjsv9xo= Xref: news.eternal-september.org comp.lang.ada:28097 Date: 2015-10-28T16:07:55-04:00 List-Id: "Dmitry A. Kazakov" writes: > On Tue, 27 Oct 2015 09:30:54 -0400, Bob Duff wrote: > >> "Dmitry A. Kazakov" 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." > 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; 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. I'd say that's the main point of contracts -- to allow localized reasoning about programs. - Bob