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!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: function Is_Open (File : File_Type) return Boolean; :Text_io
Date: Thu, 29 Oct 2015 12:47:48 +0100
Organization: A noiseless patient Spider
Message-ID: <n0t0t1$56e$1@dont-email.me>
References: <f30bbb5d-ebfd-427b-8c16-88aeb8a61318@googlegroups.com>
 <87twpd2qlo.fsf@theworld.com> <1pj15r7pul7f1.15qgdyrc8k133$.dlg@40tude.net>
 <87pp0030c1.fsf@theworld.com> <135hiczk56x02.1xixcme8btbl4.dlg@40tude.net>
 <n0o9fb$3pq$2@dont-email.me> <1dzlgoh4u2j7t$.1un3dfy0oeigd$.dlg@40tude.net>
 <n0qa3q$th8$1@dont-email.me> <190shqocxd87d$.1d68ghgqgbvfs$.dlg@40tude.net>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Thu, 29 Oct 2015 11:45:37 +0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="5326"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+QolWCJxhJ1mSORVpGefqsvSZmN/SKr/0="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0)
 Gecko/20100101 Thunderbird/38.3.0
In-Reply-To: <190shqocxd87d$.1d68ghgqgbvfs$.dlg@40tude.net>
Cancel-Lock: sha1:luqCL0/Q7lR/3CnstfJWPD5LvPs=
Xref: news.eternal-september.org comp.lang.ada:28111
Date: 2015-10-29T12:47:48+01:00
List-Id: <comp.lang.ada>

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

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.

> 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.
However, we wish to say that we know what the compiler does not
know, because a conjecture is being used as an assumption
when designing our subprogram, say.  If this assertion might
be checked at run-time due to some Assertion_Policy, then we
have to add a contraption,

     Some_Assertion =>
         Conjecture_X_To_Be_Assumed or else Conjecture_X (...);

So, if an algorithm is based on a conjecture, and we wish
to communicate what it is, precisely, a Boolean expression
allows us to do so. It documents our assumptions precisely.