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-24 02:55:19 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!feed.news.nacamar.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: Mon, 24 Mar 2003 10:56:48 +0000 Message-ID: <3E7EE470.5030807@praxis-cs.co.uk> References: 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 1048503315 78382495 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:35647 Date: 2003-03-24T10:56:48+00:00 List-Id: Volkert wrote: > Some time ago in c.l.a. was a discussion on > adding Assertions (preconditions, postconditions > and invatiants) to Ada 95. > > - what is the current status? > - who is working on this topic > - who is interested in Dbc for Ada > > Volkert To keept this thread under some sort of control, I suggest we agree a clear distinction between contracts enforced at run time (by the evaluation of checks and, typically, the raising of exceptions if the contract is vilated) and contracts enforced statically, prior to execuation (typically using proof technology). As Lutz has pointed out in an earlier reply, SPARK certainly provides the latter and has done for some years. There have been some proposals for run-time assertions in Ada 0Y although many participants in the review process have found them wanting. The big problem here is that the really interesting contractual claims may involve items not visible at the point where the contract is being checked (unless the code is rewritten with reduced abstraction to make them visible). Peter