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: Thu, 29 Oct 2015 15:00:25 +0100 Organization: cbb software GmbH Message-ID: <19ihs115mzocg$.20s63jo0q2gf.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> <190shqocxd87d$.1d68ghgqgbvfs$.dlg@40tude.net> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: TWQ9mg4k1m/sph/eQ+zHLA.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:28115 Date: 2015-10-29T15:00:25+01:00 List-Id: On Thu, 29 Oct 2015 12:47:48 +0100, G.B. wrote: > On 28.10.15 19:20, Dmitry A. Kazakov wrote: >>> >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? > > You mean, contract code needs to add value to *executables* > other than run-time tests? I mean that something unknown is, well, unknown. > I think the biggest misunderstanding here is in asking for > contracts to be considered just expressions, and then analyzing > them like they were *meant* to be ordinary expressions. Yes. Contracts may have no effect on program execution. Consider this: program describes execution contract describes program(s) documentation describes anything > Even so, I think that an implementation of Ada could "outsource" > assertion checking to some read-only copy of the program that > is running on a twin processor, suitably connected, so as to > reduce run-time effects of assertion checking. We discussed that earlier. You can have program A asserting program B. You never can do this in a single program. That is inconsistent. Any execution effects of A are not of B. Thus, as before, assertion has no run-time effect on B. Nothing changed. When you put A into B, that is automatically broken. >> If you force it, it generates garbage, which the semantics of dynamic >> predicates is, a garbage. > > No, the compiler will be effecting the computation of a result > that does not need to be computed because we know it is true. Either the program raises exception or it does not. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de