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!gandalf.srv.welterde.de!news.jacob-sparre.dk!franka.jacob-sparre.dk!pnx.dk!.POSTED!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Tue, 20 Dec 2016 18:59:22 -0600 Organization: JSA Research & Innovation Message-ID: References: <1af458a8-cf5b-4dd7-824d-eed1ed5ffb21@googlegroups.com> NNTP-Posting-Host: rrsoftware.com X-Trace: franka.jacob-sparre.dk 1482281962 7441 24.196.82.226 (21 Dec 2016 00:59:22 GMT) X-Complaints-To: news@jacob-sparre.dk NNTP-Posting-Date: Wed, 21 Dec 2016 00:59:22 +0000 (UTC) X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2900.5931 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2900.6157 X-RFC2646: Format=Flowed; Response Xref: news.eternal-september.org comp.lang.ada:32931 Date: 2016-12-20T18:59:22-06:00 List-Id: "Dmitry A. Kazakov" wrote in message news:o3b316$153k$2@gioia.aioe.org... > On 2016-12-19 23:33, Randy Brukardt wrote: ... >> And I'm not sure why >> subtype Y is X range 1 .. 100; >> is OK and >> subtype Z is X with Static_Predicate => Z > 0; >> is not. They both have explicit declarations of the subtype, and the >> semantics is effectively the same. > > The former declares a continuous range from which the semantics of numeric > operations and attributes can be deduced. For the later, nobody has any > idea without looking at the expression = implementation. The expression is just a poor way of describing a set. I wanted to call these set constraints with appropriate set syntax, but I lost that argument. The semantics is the same either way. It's unlikely that a compiler would execute this expression as-is when making a check; it's most likely going to be making a set check. > "Effectively same" is meaningless on its own. The generated object code is > "effectively same" too. I said "effectively the same" because there are subtle wording differences which only matter in a few cases. Had we had first-class set constraints, we'd have had the same rules (as we didn't want to support discontigous arrays). So far as the set of operations and reasoning goes, there's no difference between reasoning for a set and for a single range (which is just a subset of a set anyway). > As I said, it is low-level and useless from SW design POV. You must be > able to answer questions like if you used Z in an algorithm of X, would it > work? If not, how, when, where etc. A range allows answering such > questions, an arbitrary constraint does not. A static_predicate is not an *arbitrary* constraint. It's restricted to expressions that can easily be represented as a set with a small number of ranges. One certainly can reason about it. (A dynamic_predicate is just an assertion that gets automatically placed at type conversions, quite a different thing. [There's a reason the names are different!] But my understanding is that provers are quite happy to use assertions in their proofs. Even so, I specifically was not talking about them.) Randy.