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 11:00:19 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news.isc.org!sjc70.webusenet.com!c03.atl99!news.webusenet.com!news.maxwell.syr.edu!sn-xit-03!sn-xit-01!sn-post-01!supernews.com!corp.supernews.com!not-for-mail From: "Randy Brukardt" Newsgroups: comp.lang.ada Subject: Re: Ada and Design By Contract Date: Wed, 26 Mar 2003 13:00:41 -0600 Organization: Posted via Supernews, http://www.supernews.com Message-ID: References: <3E7EE470.5030807@praxis-cs.co.uk> <3E801279.80905@praxis-cs.co.uk> <3E817504.5040806@praxis-cs.co.uk> MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Newsreader: Microsoft Outlook Express 4.72.3612.1700 X-MimeOLE: Produced By Microsoft MimeOLE V4.72.3719.2500 X-Complaints-To: abuse@supernews.com Xref: archiver1.google.com comp.lang.ada:35738 Date: 2003-03-26T13:00:41-06:00 List-Id: Peter Amey wrote in message <3E817504.5040806@praxis-cs.co.uk>... >> 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. Which is why Janus/Ada was always included a call walkback with every unhandled exception, and includes this information in Exception_Information. It's often the case that the location of an exception being raised (assertion failure) isn't enough information. But, usually (probably more than 90% of the time), knowing the caller(s) allow tracing/fixing the bug without having to add additional code (or even run the program again). Proof has its place, of course, but I don't think that most systems can justify the extra work to develop that way. A few carefully placed run-time assertions (combined with good compiler suppprt - it's not surprising that Gnat added a walkback feature) are sufficient for non-critical systems. Randy.