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!newsfeed.fsmpi.rwth-aachen.de!newsfeed.straub-nv.de!news-1.dfn.de!news.dfn.de!news.uni-weimar.de!medsec1.medien.uni-weimar.de!lucks From: Stefan.Lucks@uni-weimar.de Newsgroups: comp.lang.ada Subject: Re: Ada 2012 Constraints (WRT an Ada IR) Date: Fri, 16 Dec 2016 13:56:20 +0100 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <999c67b0-4478-4d2b-8108-32ac48fe6316@googlegroups.com> NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: multipart/mixed; BOUNDARY="8323329-205291469-1481890144=:29766" X-Trace: pinkpiglet.scc.uni-weimar.de 1481892983 1051 141.54.178.228 (16 Dec 2016 12:56:23 GMT) X-Complaints-To: news@pinkpiglet.scc.uni-weimar.de NNTP-Posting-Date: Fri, 16 Dec 2016 12:56:23 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: User-Agent: Alpine 2.20 (DEB 67 2015-01-07) Content-ID: Xref: news.eternal-september.org comp.lang.ada:32880 Date: 2016-12-16T13:56:20+01:00 List-Id: --8323329-205291469-1481890144=:29766 Content-Type: text/plain; CHARSET=ISO-8859-15; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE Content-ID: On Fri, 16 Dec 2016, G.B. wrote: > ... a design choice: establishing the precondition is work > to be done be the programmer who writes the call. There may be > Make'Pre as a guide. If there isn't, the implementers of > Make and writers of Make'Post have not done their homework. Make'Pre isn't just a guide, it is a contract. ;-) > But this is puzzling: > Suppose the compiler can't prove that calling Make is safe in the > Pre/Post sense. Then, how did the programmer of Make determine > which parameters will lead to safe return? And be silent about it? Technically, the programmer is responsible for *never* violating the=20 precondition, ever. That is the whole point of a *precondition*. So First <=3D Second is a proper precondition, telling the customer to=20 never, ever call Make with First > Second: function Make (First, Second: POT) return Immutable_Ordered_Pair with Pre =3D> First <=3D Second, Post =3D> ... In contrast, the notation with "or else Exception" is technically not a=20 precondition, any more. It tells the reader/client: "You don't need to=20 bother with the order of First and Second. If you call Make with First >=20 Second, I will raise a specific exception that you may handle, then.": function Make (First, Second: POT) return Immutable_Ordered_Pair with Pre =3D> First <=3D Second or else Raise_Constaint_Error, Post =3D> ... While Ada writes this conveniently as a precondition, it actually is a=20 postcondition. Dmitry is right at that point. Now, I am not as dogmatic as Dmitry sometimes is. Sure, the "or else=20 Exception" notation is a minor abuse of the "Pre" aspect, and the "Post"=20 aspect would have fitted better. But this is just a marginal syntactic=20 issue, and having the option to specify the specific exception is great! > Again, I think that an important purpose of the Pre aspect is to > inform the programmer about when *not* to call. Well, that is the purpose of a precondition, but we have to live with the= =20 fact that the "Pre" aspect is also used for certain postconditions. Else=20 something like Pre =3D> First <=3D Second or else Raise_Constaint_Error, would not make any sense at all! If you never call the subprogram with First > Second, it will not raise=20 the exception. And if the exception is not raised, anyway, then why, on=20 earth, whould you care which exception is not raised? A related but different point: Some people go even further and claim that Pre =3D> First <=3D Second, is not a proper precondition, because this is, de facto, the shorthand for Pre =3D> First <=3D Second or else Assertion_Error. I am afraid, that argument leads eventually into madness. If the compiler= =20 cannot prove that a certain call does not violate the contract, and if the= =20 programmer actually violates the contract, it makes sense to write some=20 diagnostic information to somewhere and then shut down. Of course,=20 handling Assertion_Error and then continuing, instead of shutting down,=20 may be express route into madness. ;-) -------- I love the taste of Cryptanalysis in the morning! -------= - www.uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-luck= s ----Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universit=E4t Weimar, Germany-= --- --8323329-205291469-1481890144=:29766--