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.4 required=5.0 tests=BAYES_00,FORGED_MUA_MOZILLA autolearn=no autolearn_force=no version=3.4.4 X-Google-Thread: 103376,b78c363353551702 X-Google-NewGroupId: yes X-Google-Attributes: gida07f3367d7,domainid0,public,usenet X-Google-Language: ENGLISH,ASCII-7-bit Received: by 10.68.223.40 with SMTP id qr8mr3205387pbc.0.1340366057397; Fri, 22 Jun 2012 04:54:17 -0700 (PDT) Path: l9ni6731pbj.0!nntp.google.com!news2.google.com!news3.google.com!feeder1.cambriumusenet.nl!feed.tweaknews.nl!80.86.168.138.MISMATCH!news-feed.eu.lambdanet.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool1.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Fri, 22 Jun 2012 13:54:16 +0200 From: Georg Bauhaus User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.7; rv:13.0) Gecko/20120614 Thunderbird/13.0.1 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: about the new Ada 2012 pre/post conditions References: <1hgo6aks03zy.by4pq4xbjsgf$.dlg@40tude.net> <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> In-Reply-To: <1jvy3elqtnd1j.1sjbk32evhp1f$.dlg@40tude.net> Message-ID: <4fe45ce8$0$9508$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 22 Jun 2012 13:54:16 CEST NNTP-Posting-Host: f297ccf1.newsspool1.arcor-online.net X-Trace: DXC=i7aQZKH1@7;;]cDoEWD6A4ic==]BZ:af>4Fo<]lROoR1nkgeX?EC@@0JkkRih[6:Lh>_cHTX3j=G4?TMZkHMZ< X-Complaints-To: usenet-abuse@arcor.de Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Date: 2012-06-22T13:54:16+02:00 List-Id: On 22.06.12 09:23, Dmitry A. Kazakov wrote: > Neither #1 nor #2 is defendable. Maybe dynamic checking is not defendable when the attack is based on some biased, and, frankly, narrow set of assumptions. Which is probably OK in some narrow field. But from a workshop point of view, I'd throw in that Pre/Post gives us vastly better error messages, as follows. A clause of the contract, involving exceptions, looks like this: If you, client, do not obey the constract *Pre*, then I, supplier, may fail to produce in accord with the contract *Post*. I will throw something at you. Exceptions will happen in any case. The Pre/Post aspects show that this is the case. However, exceptions will point to somewhere *inside* the supplier's package if Pre/Post checking is off, or Pre = True. Whereas, if Pre/Post checking is on as intended, exceptions can pinpoint a *contract* violation by the client. This behavior requires that pre/post conditions are properly reflected in the supplier's implementation. (I have indicated alternative possibilities (just on Pop), as the specific contract of this example is probably one among a number of choices. For the sake of simplicity, this is a single stack package; the contractual behavior shouldn't change much with a stack type declared instead.) Compare raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from stk.ada:20 instantiated at stk.ada:79 vs raised CONSTRAINT_ERROR : stk.ada:60 range check failed Note that the first message mentions a specific precondition from the spec. The second message points to the body. This body may not be available for inspection! That is, if you want to spend time finding your own error by understanding the supplier's implementation first! generic package Stk is pragma Elaborate_Body (Stk); Capacity : constant := 10; -- or use a constrained subtype type T is interface; type Stackable is access constant T'Class; function Length return Natural; -- Number of items currently on the stack. procedure Push (Item : Stackable) with Pre => Length < Capacity, Post => Top = Item and Length = Length'Old + 1; -- Item becomes topmost if there is room procedure Pop with Pre => Length > 0, Post => Length = Length'Old - 1; -- Drops the topmost item, if any. -- [ALTERNATIVELY, -- Pre => True, -- Post => Length = Natural'Max (0, Length'Old - 1)] function Top return Stackable with Pre => Length > 0; -- A copy of the topmost item. -- [ALTERNATIVELY ...] end Stk; package body Stk is Ptr : Natural range 0 .. Capacity; Data : array (Natural range 1 .. Capacity) of Stackable; -- -- Strategy: there is a 1:1 correspondence between -- Ptr being in range and the pre/post conditions -- function Length return Natural is begin return Ptr; end Length; procedure Push (Item : Stackable) is begin -- cannot produce Post if the stack is full, may raise C_E Data (Ptr + 1) := Item; -- Ptr not increased in case of failure Ptr := Ptr + 1; end Push; procedure Pop is begin Ptr := Ptr - 1; -- if Ptr = 0, then C_E end Pop; function Top return Stackable is begin -- if Ptr not in 1 .. Capacity, then C_E return Data (Ptr); end Top; begin Ptr := 0; end Stk;