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 14:24:50 +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:32882 Date: 2016-12-16T14:24:50+01:00 List-Id: On 16/12/2016 12:48, G.B. wrote: >> The key difference is > > ... a design choice: establishing the precondition is work > to be done be the programmer who writes the call. Yep, a burden one could easily avoid had the designer cared to do his job properly. > But this is puzzling: > Suppose the compiler can't prove that calling Make is safe in the > Pre/Post sense. Then the program must be illegal, > Then, how did the programmer of Make determine > which parameters will lead to safe return? And be silent about it? This presumes the programmer has absolutely no idea why he is calling the subprogram. This is certainly not the way of work Ada should promote. Furthermore, the compiler does not prove if Make call is safe. The compiler proves if the code calling Make is correct. E.g.: 1. the code was contracted not to raise Constraint_Error 2. a call to Make possibly propagates Constraint_Error 3. Constraint_Error is not handled --------- Incorrect This is a sufficiently different approach to software design from what you seemingly have in mind. If Make has a precondition it would become: 1. precondition is true -------- Cannot prove First <= Second, incorrect The former is a lot easier to deal with, which is why the design rule orders to weaken preconditions. > Again, I think that an important purpose of the Pre aspect is to > inform the programmer about when *not* to call. Not at all. The sole purpose of a precondition is to state the contract. Information as to why Make is called and what Make is supposed to do is a problem space concept, not a correctness concept. -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de