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=-1.9 required=5.0 tests=BAYES_00 autolearn=unavailable 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!feeder.eternal-september.org!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Tue, 13 Dec 2016 22:11:54 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <47366b42-c0a3-41bf-a44a-5241c109d60f@googlegroups.com> <1af458a8-cf5b-4dd7-824d-eed1ed5ffb21@googlegroups.com> NNTP-Posting-Host: s3c6wwRqkurrfTZpuYYZ+w.user.gioia.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 X-Mozilla-News-Host: news://news.aioe.org Xref: news.eternal-september.org comp.lang.ada:32787 Date: 2016-12-13T22:11:54+01:00 List-Id: On 2016-12-13 19:25, Shark8 wrote: > On Tuesday, December 13, 2016 at 4:19:17 AM UTC-7, Dmitry A. Kazakov wrote: >> On 13/12/2016 11:39, G.B. wrote: >>> >>> 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. > > By that logic we shouldn't have something like: > type Item is null record; -- Stub > type Pointer is access Item; -- Access type > subtype Handle is not null Pointer; -- Subtype excluding null > > Procedure Something(Object : Handle); -- Object can't be null. > because we could instead say: > Procedure Something(Object : Pointer) is > begin > if Object = Null then --... > end; > > Or, really, any subtype. No. Type/subtype declarations are expressions involving type-algebraic operations [some operands are types, results are types]. You cannot use them in the bodies. They implicitly define operations of the resulting type and the corresponding bodies. This has nothing to do with the bodies defined explicitly in the declarative region by the programmer. You could point at: overriding procedure Foo (X : Bar) is null; That would be right, and I would wholeheartedly agree that this is against the principle of implementation separation. >>>> 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. > > But this works against your whole anti-pre, anti-post, anti-aspect > argument... those *ARE* [generally] Ada Boolean expressions. They are not, what was meant would be a predicate, spelled fully: forall a > b, a in T, b in T exist n in N a = b * n + a rem b It is not a Boolean expression and it cannot be written or evaluated in Ada. Though it is possible to write a program in Ada that would perform calculus on such expressions, e.g. SPARK. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de