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 17:59:42 +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 16:58:19 -0000 (UTC) Injection-Info: mx02.eternal-september.org; posting-host="eb28462d3cdfe36eb00d85b69972742c"; logging-data="11663"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/oFNL2qDChdCyqnuPC0zsqoW5WcbIwzFs=" 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:0JshaHSxXISpv0fQdO3R6yQw1Hg= Xref: news.eternal-september.org comp.lang.ada:32780 Date: 2016-12-13T17:59:42+01:00 List-Id: On 13/12/2016 12:19, Dmitry A. Kazakov wrote: > On 13/12/2016 11:39, G.B. wrote: >> 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. > > Being a part of the body it does not belong to declarations. Right, Pre aspects are *not* body! They have a right to be part of some sort of monitoring program that observes the first if they are to have an operational effect at all. They are assertions separate from the program itself. And they need *not* be exhaustive, even saying of what would be hard, if possible at all. I think that is agreement. Whatever GNAT happens to do now does not change all this. >>> It is an explicit contract. >> >> Can you make it a Boolean expression? > > That depends on the language in question. It is not an expression in Ada and cannot be made one. Please, it's simple, actually, for what I had suggested, a relation involving the two parameters A and B to be passed to Plus_Too, since Standard.Integer is finite. One lists inputs to Plus_Too as pairs that one specifies as not mathematically overflowing the sum in Integer, for a start. That's far from not expressible in Ada, it's not perfect either, and it is highly inconvenient. (A => Integer'Last, B => Integer'Last) will be a pair not listed, (A => -1, B => 42) meets the requirements, and is listed. >> So, what are expected values for various inputs of A and B >> passed to Plus_Too? Can this be stated? > > Yes it can and it is already done by the provided implementation of Plus_Too. It needs to be stated before the fact to be useful. Without an implementation yet, one cannot infer its precondition. But it is possible to write a predicate that is the specification of a set of values from which some implementation is to compute results. > You keep on confusing program behavior with statements about it. See above. >> Gödel's results do not apply to "+" in Standard.Integer, >> so nothing is due to them here. > > They apply to a framework capable to spell all preconditions of "+". No such thing can exist. Therefore some [most] contracts will remain implied forever. I only asked for a relation between A and B as inputs to Plus_Too. I cannot reasonably ask for an exhaustive Boolean expression that makes the silly attempt to describe the universe of possibilities in which Ada's "+" may have a number of effects.