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-Thread: 103376,699cc914522aa7c4 X-Google-Attributes: gid103376,public X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news4.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local01.nntp.dca.giganews.com!nntp.megapath.net!news.megapath.net.POSTED!not-for-mail NNTP-Posting-Date: Wed, 17 Jan 2007 17:17:59 -0600 From: "Randy Brukardt" Newsgroups: comp.lang.ada References: <1168885771.30643.20.camel@localhost> <1168891576.30643.39.camel@localhost> <5NKdnTv2UZfVZTbYnZ2dnUVZ_vipnZ2d@megapath.net> <38z8yk9z1uxn$.1r6qpevwu2i7c.dlg@40tude.net> <1lpy2h06scx34.1i2k4dlbg0nfy.dlg@40tude.net> Subject: Re: Structured exception information Date: Wed, 17 Jan 2007 17:18:55 -0600 X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 6.00.2800.1807 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1807 Message-ID: NNTP-Posting-Host: 64.32.209.38 X-Trace: sv3-vkze4sO/aDR5ggt7NIXmGQ6H2FK6ujbgu9LQ3Hz/Zi/KNxaM0JSVGNXFikVuuZp8qAuXd+XGpDNtzWw!Lnt2USPrfv+TkZIZMCToPs7ztFxS5SrzO52PJ2o/o/F6WqCOg50Izr28SLqYJo3lha5VqL6now5Z!iv+KApDaH4+CHQ== X-Complaints-To: abuse@megapath.net X-DMCA-Complaints-To: abuse@megapath.net X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint properly X-Postfilter: 1.3.32 Xref: g2news2.google.com comp.lang.ada:8237 Date: 2007-01-17T17:18:55-06:00 List-Id: "Jeffrey Carter" wrote in message news:x2urh.309672$FQ1.158886@attbi_s71... > Dmitry A. Kazakov wrote: > > > > I doubt that others could or should be called preconditions. > > > The point is that violated preconditions are non-states and cannot be > > handled at all. Provided, that one understands precondition as a method of > > proving program correctness. Otherwise, it is something else. > > It's clear that you're locked into the concept of a precondition as part > of correctness proofs. In that context, yes, you statically prove that > preconditions are met, and do not need to dynamically test them. This is > the case with SPARK, for example. Right. The problem is that you can't write much of anything interesting that is statically provable for the full Ada language. (If your willing to work only in a subset of Ada, that's of course different.) Thus, I tend to think mainly about dynamic preconditions, tested either as explicit tests or as assertions. Those raise an exception if they fail. And part of the contract of the operation is that an exception will be raised if the (dynamic) preconditions fail. ... > Ideally, you'd use the same syntax for both uses of preconditions. Then > SW that's written for general use could be used in SW that does > correctness proofs without changes; without correctness proofs the > compiler would automatically generate the tests, and with proofs, the > tests would not be generated. When we looked at this during the Amendment work, the static analysis people thought that the requirements for static preconditions and dynamic ones were too different to use the same syntax/semantics for both. While I'm not sure I believe that, it's never a good idea to dispute people who have more experience in an area than you do. Anyway, preconditions and postconditions start getting messy once you try to figure out how they inherit, how to access previous values, and the like. And there's ugly visibility issues if you want to write them on the specification. So, eventually we gave up in part because there wasn't much existing practice for dynamic preconditions/postconditions, so we couldn't be sure what we were doing was even useful. Randy.