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 09:40:57 PST Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!postnews1.google.com!not-for-mail From: volkert@nivoba.de (Volkert) Newsgroups: comp.lang.ada Subject: Re: Ada and Design By Contract Date: 24 Mar 2003 09:40:57 -0800 Organization: http://groups.google.com/ Message-ID: References: <3E7EE470.5030807@praxis-cs.co.uk> NNTP-Posting-Host: 195.186.221.173 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-Trace: posting.google.com 1048527657 8946 127.0.0.1 (24 Mar 2003 17:40:57 GMT) X-Complaints-To: groups-abuse@google.com NNTP-Posting-Date: 24 Mar 2003 17:40:57 GMT Xref: archiver1.google.com comp.lang.ada:35654 Date: 2003-03-24T17:40:57+00:00 List-Id: > 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). I know Spark and i like it, but my question is more in the direction of Eiffel-like Assertion mechanisms (runtime monitoring/checking). > There have been some proposals for run-time assertions in Ada 0Y > although many participants in the review process have found them > wanting. Can you/someone give me a pointer to it ...i found only a paper from Ehud Lamm from the last Ada-Europe Meeting. > 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). I see not the problem. Can you give a short example. Volkert