Re: Structured exception information

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

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