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: Thu, 15 Dec 2016 14:17:07 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.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 6.1; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.5.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32846 Date: 2016-12-15T14:17:07+01:00 List-Id: On 15/12/2016 11:31, G.B. wrote: > On 15/12/2016 09:41, Dmitry A. Kazakov wrote: >> In Ada type declarations must be there, so it is not a tool, but an >> integral part of the language. This is why "pre"-aspects is a >> non-starter even ignoring their semantic consistency issues. You can >> do things with or without them. Psychologically it won't work. > > Problem statement: > Devise a type that represents an ordered pair of linearly > ordered numbers, such that programmers can create objects that > have the two elements in proper order. It is a good illustration of what is wrong with ideas you promote. You are thinking in terms of implementations. Ada, at least Ada 83 was focused on ADT and designed to be language that supporting software design in terms of ADTs as opposed to loose data structures. An Ada programmer would rather design an integer interval type than data structure you described. Whether he would choose a pair of interval bounds to represent it, or the lower bound and length, or whatever else he would not expose it in the declarations. Neither there is any reason to derive an interval type from a pair and put a constraint on the pair as you seem suggest. That is an implementation. Semantically pairs and intervals are not related types. Then lower<=higher is not a constraint, it is an invariant, if any. Furthermore from the correctness proofs standpoint the post-conditions of interval arithmetic trivially ensure the invariant. E.g. [a,b] + [c,d] = [min(a,b), max(c,b)] So there is no need to spell the invariant. And finally, invariant is an implementation detail not to expose anyway. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de