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!news2.google.com!news4.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!wns14feed!worldnet.att.net!attbi_s21.POSTED!53ab2750!not-for-mail From: Jeffrey Carter User-Agent: Mozilla/5.0 (Windows; U; Windows NT 5.0; en-US; rv:1.8.0.1) Gecko/20060130 SeaMonkey/1.0 MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Structured exception information 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> In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Message-ID: <%xErh.228837$aJ.94458@attbi_s21> NNTP-Posting-Host: 12.201.97.213 X-Complaints-To: abuse@mchsi.com X-Trace: attbi_s21 1169102075 12.201.97.213 (Thu, 18 Jan 2007 06:34:35 GMT) NNTP-Posting-Date: Thu, 18 Jan 2007 06:34:35 GMT Organization: AT&T ASP.att.net Date: Thu, 18 Jan 2007 06:34:35 GMT Xref: g2news2.google.com comp.lang.ada:8243 Date: 2007-01-18T06:34:35+00:00 List-Id: Randy Brukardt wrote: > > 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. Preconditions are pretty straightforward, in my experience: I can almost always express them as a Boolean expression (not X.Empty). Couple a Boolean expression with an exception and I'll be happy. Where that fails is mostly "for all" and "there exists" conditions, and I can live without that. Postconditions are a different matter. I often want to write things like (using SPARK notation) Size (X) = Size (X~) + 1 [would that be X~.Size in Object.Operation notation?] where X is an in out parameter of a limited type. In the most general case this involves storing the in value of X, which you're not supposed to be able to do. Maybe you could arrange to store Size (X) on input, as well as the values of all the other functions on in out parameters mentioned in the postcondition(s). They're still useful for documenting the behavior of an operation.