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!news.eternal-september.org!.POSTED!not-for-mail From: "G.B." Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Wed, 14 Dec 2016 19:14:09 +0100 Organization: A noiseless patient Spider Message-ID: References: <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com> Reply-To: nonlegitur@notmyhomepage.de Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Wed, 14 Dec 2016 18:12:46 -0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="d7777aaea4e05f5460ede15b9236d665"; logging-data="6028"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX18oOgQOtDHbwsd3BVUDTgmVxDqP2DUrA/o=" User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 In-Reply-To: Cancel-Lock: sha1:EI5shlV4hWIO2FHOnkMb+W6dLmw= Xref: news.eternal-september.org comp.lang.ada:32825 Date: 2016-12-14T19:14:09+01:00 List-Id: On 14/12/2016 17:52, Dmitry A. Kazakov wrote: > On 2016-12-14 17:31, G.B. wrote: >> On 14/12/2016 13:52, Dmitry A. Kazakov wrote: >>> On 14/12/2016 13:44, G.B. wrote: >>>> On 14/12/2016 12:25, Dmitry A. Kazakov wrote: >>>> >>>>> That is the problem with implied contracts. Is this legal: >>>>> >>>>> begin >>>>> loop >>>>> X (Read (Stream)); >>>>> end loop; >>>>> exception >>>>> when Constraint_Error => >>>>> null; >>>>> end; >>>> >>>> "Assertions are not an input checking mechanism" >>>> "To avoid a common misunderstanding, make sure to note >>>> that each of the contracts discussed holds between a routine >>>> (the supplier) and another routine (its caller): we are concerned >>>> about software-to-software communication, not software-to-human >>>> or software-to-outside-world. (...) Here there is no substitute >>>> for the usual condition-checking constructs, include the venerable >>>> IF ... THEN ...; the exception handling mechanism ... may also be >>>> helpful ". [1] >>>> >>>> [1] Meyer, Bertrand: OOSC2, 2nd ed, ยง11.6 >>> >>> Is it legal or not? >> >> Like you have said, "It is about formal language-supported contracts >> and all sorts of other contracts". So, I think there is enough material >> there to conclude that this kind or that kind of contract should >> be legally dominating a particular program design decision. > > That is no answer. It is an answer, even with some "legality" coming out of nowhere, as if RM legality, I guess, were a sufficient condition for (a) correctness, and (b) justifying misuse of contracts (see below, and above), and the answer invalidates the premises of your proof: "There is no substitute ..." is universally quantified, and it suggests to not *ever* use aspects when checking input. See the first sentence of Meyer, which is a heading. "The exception handling mechanism ... may ... helpful", while politely suggesting existential qualification, is accompanied by a requirement of Eiffel style exception handling. > A program is either legal or not. The program is legal. The contract you implied is violated. Thus what you called contract is not a formal contract. q.e.d. It is interesting to learn that I must have implied all kinds of contracts (which ones? which kind?) when I speak in favor of expressly written aspects.