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=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,67afd31696e08d55 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2003-03-26 01:36:27 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news-spur1.maxwell.syr.edu!news.maxwell.syr.edu!newsfeed.icl.net!newsfeed.fjserv.net!newsfeed.freenet.de!newsfeed.r-kom.de!fu-berlin.de!uni-berlin.de!213.155.153.242!not-for-mail From: Peter Amey Newsgroups: comp.lang.ada Subject: Re: Ada and Design By Contract Date: Wed, 26 Mar 2003 09:38:12 +0000 Message-ID: <3E817504.5040806@praxis-cs.co.uk> References: <3E7EE470.5030807@praxis-cs.co.uk> <3E801279.80905@praxis-cs.co.uk> NNTP-Posting-Host: 213.155.153.242 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Trace: fu-berlin.de 1048671385 81054954 213.155.153.242 (16 [69815]) User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.0.2) Gecko/20030208 Netscape/7.02 X-Accept-Language: en-us, en Xref: archiver1.google.com comp.lang.ada:35716 Date: 2003-03-26T09:38:12+00:00 List-Id: Volkert wrote: > Dear Peter, > > >>>Volkert >> >>A small (but probably not the best) example: >> >>package P is >> function IsFull return Boolean; >> -- we may only want this function for assertion checking, not as >> -- part of our normally executable code >> >> procedure Push ... >> --! pre not IsFull; -- run time assertion >> ... >>end P; > > IsFull is part of the contact between client/supplier. > The client needs access to IsFull. As a consequence > IsFull has to be part of the executible code. > > >>with P; >>package Q is >> procedure SomeOperation; >> -- Calls P.Push so we really need to propagate the precondition here >> --! pre not P.IsFull; >> ... >>end Q; > > The caller has to check that not(P.isFull) is true, else > he can possibly break the contract. It is clear, that the caller > must implement this check in its own body > > >>with Q; >>package R is >> procedure AnotherOperation; >> -- this calls Q.SomeOperation; >> -- It's execution will involve the check not P.IsFull but P is not >> -- visible here. >>end R; > > The check is made in the body of Q.SomeOperations. Why should > P.IsFull visible here? > Because it is too late to wait until Q.SomeOperation is executed in breach of contract. The real cause of the contract failure is AnotherOperation's attempt to call Q.SOmeOtherOperation in a way that will cause the stack to overflow. If we want to try and deal with the problem we need to know where the dangerous condition started. In our view this is better done by proof than by dynamic checks. Peter