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: Tue, 13 Dec 2016 11:39:45 +0100 Organization: A noiseless patient Spider Message-ID: References: <47366b42-c0a3-41bf-a44a-5241c109d60f@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: Tue, 13 Dec 2016 10:38:22 -0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="eb28462d3cdfe36eb00d85b69972742c"; logging-data="18705"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/Tkame6FEkRBtn7+57+rHj7ki2gW80zqg=" 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:uDZEAMRxcOYW0wnxKTrJGS9Nl/M= Xref: news.eternal-september.org comp.lang.ada:32776 Date: 2016-12-13T11:39:45+01:00 List-Id: On 13/12/2016 09:27, Dmitry A. Kazakov wrote: >> No Ada in there. I was thinking of this posting. > > Ada is an object language here. Thus it can never be Ada. It could be a meta language of annotations for Ada, like SPARK. Pre doesn't have to be object language as has now been said and confirmed a number of times. >>> Implied contracts are outside the scope. >> >> My point. Why should contracts not be explicit, in particular >> when they had already been formal, albeit in a comment? > > Explicit contracts are only ones the framework can enforce, at all or pragmatically. Which role do programmers play in this? Are frameworks so much better at proving and enforcing than humans? They are man made frameworks after all, so whether they should necessarily limit the scope of man seems dubious. > It is an explicit contract. Can you make it a Boolean expression? > The contract gets violated when the Plus_Too does not return expected value due to consumption of the CPU by the black hole. So, what are expected values for various inputs of A and B passed to Plus_Too? Can this be stated? Partially? I do think so. >> (Actually, there is no variable in the predicate other than those >> implied in sub-expressions of Earth turning a black hole. > > Your fault. Formally no such predicate could even exist, merely due to Goedel incompleteness. Gödel's results do not apply to "+" in Standard.Integer, so nothing is due to them here. > There is an old programmer's saying: never check bugs you are not going fix... Which is reflected in the saying that a failed Pre check puts some bug directly under my nose, and that's by intent. No proof can show bugs' absence whenever there is no predicate describing expected values.