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: border1.nntp.dca1.giganews.com!nntp.giganews.com!goblin3!goblin.stu.neva.ru!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: {Pre,Post}conditions and side effects Date: Thu, 7 May 2015 20:00:54 +0200 Organization: Bauhaus-Universitaet Weimar Message-ID: References: <2430252d-52a1-4609-acef-684864e6ca0c@googlegroups.com> <0a718b39-ebd3-4ab5-912e-f1229679dacc@googlegroups.com> <9ee5e186-5aaa-4d07-9490-0f9fdbb5ca18@googlegroups.com> <87tww5296f.fsf@adaheads.sparre-andersen.dk> <871tj9dp5b.fsf@theworld.com> <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net> NNTP-Posting-Host: medsec1.medien.uni-weimar.de Mime-Version: 1.0 Content-Type: MULTIPART/MIXED; BOUNDARY="8323329-1486639336-1431021655=:16448" X-Trace: pinkpiglet.scc.uni-weimar.de 1431022047 20577 141.54.178.228 (7 May 2015 18:07:27 GMT) X-Complaints-To: news@pinkpiglet.scc.uni-weimar.de NNTP-Posting-Date: Thu, 7 May 2015 18:07:27 +0000 (UTC) X-X-Sender: lucks@debian In-Reply-To: <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net> User-Agent: Alpine 2.11 (DEB 23 2013-08-11) Xref: number.nntp.giganews.com comp.lang.ada:193066 Date: 2015-05-07T20:00:54+02:00 List-Id: This message is in MIME format. The first part should be readable text, while the remaining parts are likely unreadable without MIME-aware tools. --8323329-1486639336-1431021655=:16448 Content-Type: TEXT/PLAIN; charset=ISO-8859-15; format=flowed Content-Transfer-Encoding: QUOTED-PRINTABLE On Thu, 7 May 2015, Dmitry A. Kazakov wrote: >> Here, I heavily disagree. Often, checking relevant properties is much to >> expensive to perform the checks them in production code. > > Merely a confusion of checks with code. There is no such thing as runtime > correctness check, Agreed! At best, a run time check is some sort of a testing harness. It is useless= =20 to show the correctness of a program, but it can help to discover bugs. >> A simple example is binary search over a sorted array. The precondition >> requires the array to be sorted. > > And what does it mean for the behavior? If unsorted input is *valid* and > *must* raise exception (contracted behavior) then you cannot remove code > *implementing* this behavior. > > Consider this client program: [...] I'll slightly rewrite your client program -- I believe, the=20 exception handler was at the wrong place. declare X : Extended_Index_Type; begin X :=3D Search (Data, Key); exception when Not_Sorted_Error | Assertion_Error =3D> X :=3D Search (Sort (Data), Key); end; > Is this code correct? It depends on the specification of "Sort". Specification 1: function Search(Data: Array_Type; Key: Value_Type) return Extended_Index_Type with pre =3D> Sorted(Data), post =3D> (if Data(Search'Result) in Data'Range then Data(Search'Result)=3DValue else Search'Result =3D No_Index and then (for all I in Data'Range =3D> Data(I) /=3D Key)); The expression "Sorted(Data)" is a precondition. Every client which can=20 possibly violate the precondition is buggy. Thus, the above code is buggy.= =20 (Or otherwise, the exception handler is dead code.) One property of a proper precondition (or postcondition or ...) is that=20 disabling the check does not change the functional behaviour of correct=20 programs. Specification 2: function Search(Data: Array_Type; Key: Value_Type) return Extended_Index_Type with pre =3D> (Sorted(Data) or else raise Not_Sorted_Error), post =3D> (if Data(Search'Result) in A'Range then Data(Search'Result)=3DValue else Search'Result =3D No_Index and then (for all I in Data'Range =3D> Data(I) /=3D Key)); The expression following "pre" is "contracted behaviour" as you put it.=20 The code above is correct, and disabling the check must be prohibited,=20 because it would break correct programs. Which is why I wrote the following= : >> Most urgently, I would expect an option to skip checking ordinary pre- a= nd >> postconditions, without skipping those that explicitly raise some >> exceptions. In other words, I want to be able to switch of proper preconditions (and=20 postconditions, whatever) without affecting contracted behaviour. I depreciate the usage of the word "precondition" for the expression=20 following "pre" in spec 2. But I will not fight about names. Furthermore, I am quite happy with Ada allowing to specify contracted=20 behaviour, even I would have prefered use an aspect of its own for=20 contraced behaviour. The "pre" aspect should better be have been reserved= =20 for proper preconditions. But this appears too late now. On the other=20 hand, it would not be too late to support disabling proper preconditions=20 without changing contracted behaviour. Stefan ------ I love the taste of Cryptanalysis in the morning! ------ uni-weimar.de/de/medien/professuren/mediensicherheit/people/stefan-lucks --Stefan.Lucks (at) uni-weimar.de, Bauhaus-Universit=E4t Weimar, Germany-- --8323329-1486639336-1431021655=:16448--