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!news3.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: Fri, 19 Jan 2007 01:33:39 -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> <%xErh.228837$aJ.94458@attbi_s21> Subject: Re: Structured exception information Date: Fri, 19 Jan 2007 01:34:35 -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-y6jnu7I+fg31p18IhTyp0ZHdy2xVQZsHG4EaOQW8/AutNzPw0mk6Hev51jLujX/BMJZSa4WT4qrOLs9!PTXrhYVsUMiNvf61HBtvC1JsI1n/0bjR8xiIr3DwN0DdpLkxWtSCDUh4WAUUJpKeOaHVpwLxRm8c!m5xgmSDKeups+A== 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:8309 Date: 2007-01-19T01:34:35-06:00 List-Id: "Jeffrey Carter" wrote in message news:%xErh.228837$aJ.94458@attbi_s21... > Randy Brukardt wrote: ... > > 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. Right, but there still are the issues of what is and is not visible in the precondition. You're not inside the subprogram, yet you have access to the parameters. And what about side-effects? The other issue was what to do with preconditions for inherited routines. They ought to compose somehow, but that got ugly in a hurry. > 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). The proposal we were working on had a way to get the original value of a scalar parameter. Which meant they all had to copied on entrance - causing extra overhead. And the inheritance, visibility, and side-effect issues are still around. Randy.