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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no 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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io Date: Wed, 28 Oct 2015 19:20:51 +0100 Organization: cbb software GmbH Message-ID: <190shqocxd87d$.1d68ghgqgbvfs$.dlg@40tude.net> References: <87twpd2qlo.fsf@theworld.com> <1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net> <87pp0030c1.fsf@theworld.com> <135hiczk56x02.1xixcme8btbl4.dlg@40tude.net> <1dzlgoh4u2j7t$.1un3dfy0oeigd$.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: j6IQVb9uobzjXrpQLDU2rQ.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:28093 Date: 2015-10-28T19:20:51+01:00 List-Id: On Wed, 28 Oct 2015 12:06:33 +0100, Georg Bauhaus wrote: > On 27.10.15 21:04, Dmitry A. Kazakov wrote: >> The point can be summarized this way. If an exception is a part of the >> contract then Status_Error is much better than Constraint_Error > > "Better than Assertion_Error?" I understand we are going to get > > subtype Open_File is File with Predicate => > Is_Open(Open_File) or else raise Status_Error with "..."; Fine, but it is already this way. Operations of Text_IO propagate Status_Error when the file was not opened. There is no need to check that twice and that is no "assertion," anyway. >> If the contract is not to raise, then, firstly, there is no >> way to enforce it, > > Enforcing it appears possible in the above case, at least for each > single program involving file objects, IIUC. How are you going to get a constrained object? File_Type is limited. [ It is mere wrong design. If you wanted file objects that refer to only open files, that is no constraint, but a property ensured upon object creation. ] >> and, secondly, if there were a way, proving no >> Status_Error would be no harder than no Constraint_Error. Ergo, no use. > > Whenever one defines "use" to have the same meaning as "proof", "Use" in this context has the meaning "added value." > However, another use of predicates is to document assumptions. Documenting *shall* have *no* run-time effects. > If the assumptions are correct, but the compiler cannot determine > their truth, should we hide the assumptions? As hide from the compiler? Certainly so! If as you said the compiler has no idea what your assumption is supposed to mean, how can it generate a useful code? If you force it, it generates garbage, which the semantics of dynamic predicates is, a garbage. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de