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=-0.3 required=5.0 tests=BAYES_00, REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4 Path: border2.nntp.dca1.giganews.com!nntp.giganews.com!newspeer1.nac.net!newsfeed1.swip.net!aioe.org!.POSTED!not-for-mail From: "Dmitry A. Kazakov" Newsgroups: comp.lang.ada Subject: Re: {Pre,Post}conditions and side effects Date: Thu, 7 May 2015 14:16:54 +0200 Organization: cbb software GmbH Message-ID: <121ytg16vbxsk$.18dxo1h7daxty.dlg@40tude.net> 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> Reply-To: mailbox@dmitry-kazakov.de NNTP-Posting-Host: enOx0b+nfqkc2k+TNpOejg.user.speranza.aioe.org Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit X-Complaints-To: abuse@aioe.org User-Agent: 40tude_Dialog/2.0.15.1 X-Notice: Filtered by postfilter v. 0.8.2 Xref: number.nntp.giganews.com comp.lang.ada:193061 Date: 2015-05-07T14:16:54+02:00 List-Id: On Thu, 7 May 2015 12:06:29 +0200, Stefan.Lucks@uni-weimar.de wrote: > On Wed, 6 May 2015, Randy Brukardt wrote: > >> I don't believe that checks in Ada (of any kind) should ever be turned off. > > 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, there is only run time code. You can neither remove functional code nor spoil your program with non-functional code, especially with one that would break the behavior. > 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: declare X : Element; begin X := Search (Data, Key); begin null; exception when Not_Sorted_Error => X := Search (Sort (Data), Key); end; end; Is this code correct? > Actually, one thing I am missing from Ada 2012 is a convenient and > fine-grained way to tell the compiler which pre- and postconditions and > invariants are to be checked, and which checks are to be skipped. There shall be no dynamic predicates at all. They are inherently inconsistent. No program shall evaluate correctness of its own. No executable code shall be put into declarations. > Most urgently, I would expect an option to skip checking ordinary pre- and > postconditions, without skipping those that explicitly raise some > exceptions. The point is, these two forms of precondition are semantically > totally different: > > The semantic of a plain precondition is essentially: > > * If I a True, the postcondition will hold. > Never call the subprogram if I am false!!! > Otherwise, the subprogram might do anything. > > This is a precondition in the "Design by Contract" sense. This is just a precondition in any sense. It reads: the program P is correct only if pre(P). Nothing else. > The semantic of a precondition with something like "else raise > This_Exception" is > > * If I am True, the postcondition will hold > when the subprogram terminates. > If I am False, the subprogram will not do anything, > except for raising This_Exception. This is not a precondition this is a contracted behavior that mandates certain kind of output (exception) for certain kind of input (unsorted array). -- Regards, Dmitry A. Kazakov http://www.dmitry-kazakov.de