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: Sat, 17 Dec 2016 10:13:17 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <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=windows-1252; 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-Mozilla-News-Host: news://news.aioe.org X-Notice: Filtered by postfilter v. 0.8.2 Xref: news.eternal-september.org comp.lang.ada:32899 Date: 2016-12-17T10:13:17+01:00 List-Id: On 2016-12-16 20:51, Randy Brukardt wrote: > "Dmitry A. Kazakov" wrote in message > news:o3095a$1f4q$1@gioia.aioe.org... >> On 15/12/2016 23:19, Randy Brukardt wrote: >>> "Dmitry A. Kazakov" wrote in message >>> news:o2tl62$1aro$1@gioia.aioe.org... >>>> On 14/12/2016 23:53, Randy Brukardt wrote: >>>>> "Dmitry A. Kazakov" wrote in message >>>>> news:o2r1ca$184u$1@gioia.aioe.org... >>>>> ... >>>>>> Others tried to argue that such bodies are not bodies but magically >>>>>> "preconditions". No, they are still bodies, just misplaced ones. >>>>> >>>>> Body /= implementation!! (Using "implementation" here in your sense as >>>>> the >>>>> entire execution of a subprogram.) A body is just the hidden part of >>>>> the >>>>> implementation; the part that is exposed to callers includes >>>>> constraint, >>>>> null exclusion, and predicate checks, and the precondition. The caller >>>>> has a need to know about part of the implementation, and hopefully not >>>>> about >>>>> the rest. Exactly where the split between the specification and the >>>>> body goes >>>>> clearly depends on a need to know basis, and it has nothing to do with >>>>> whether it is static or dynamic or provable. >>>> >>>> This pretty good summarizes why I consider it such a bad idea. >>> >>> The only alternative is to get rid of the separation of specifications and >>> bodies (many languages do exactly that). Then you don't need any kind of >>> contract. >> >> Exactly the opposite. Body /= implementation stance is getting rid of the >> separation. And Ada is well along that path since Ada 05. > > The path was that set by Ada 83 with the idea of constraints. By your model, > constraint checks belong to the implementation, and those have always been > exposed in the specification. Not explicitly. It is like the implementation of "+" when an integer type declared. The implementation is assumed but not specified. > Later versions of Ada have just built on this > already existing (and very successful) idea, extending it to further cases. I meant explicit code snippets in declarations, which includes "is null", checks, etc. It is very different from having type operations producing new [sub]types like subtype Y is X range 1..100; or type T is array (I) of E; They declare and implement operations implicitly. >>> Contracts that are too weak don't help; if a prover (or programmer!) has >>> to look into the implementation (and that would necessarily be the case in >>> your model), then there is no real separation. >> >> Surely they help. Moreover it is very important not to have to strong >> contracts. The contract strength is how much the contract determines the >> implementation. Too strong contracts prevent substitutability and thus >> code reuse. Since any modification of a type breaks something somewhere. >> Which is why contracts are relaxed in order to allow a range of >> implementations, e.g. raising and handling exceptions etc. >> Overspecification is a bad as underspecification. > > True enough. But irrelevant unless you're arguing for weak typing (and I > know you're not doing that). Typing is an example of usefulness of weak contracts. You just match types and ignore the rest. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de