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: Fri, 16 Dec 2016 09:38:00 +0100 Organization: Aioe.org NNTP Server Message-ID: References: <1af458a8-cf5b-4dd7-824d-eed1ed5ffb21@googlegroups.com> NNTP-Posting-Host: vZYCW951TbFitc4GdEwQJg.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 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:32871 Date: 2016-12-16T09:38:00+01:00 List-Id: 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. > 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. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de