Re: Structured exception information

["Randy Brukardt" <randy@rrsoftware.com>]

"Jeffrey Carter" <spam.jrcarter.not@spam.acm.not.org> 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.