Re: Contracted exceptions for Ada

Stefan Lucks <lucks@xxxxxxxxxxxxxxxxxxxxxxxxxxxxx> writes:

no need for a handler. Unfortunately, there's no Non_Zero subtype.

I am afraid, a non-zero subtype would move the problem around, rather
than solve it. The exception not raised by X/Y might then be raised
before, when you compute Y:=A-B.

On a second look, this might actually be useful better diagnostics. The
exception is raised closer to the point where the faulty value (the zero
Y) is created, rather than, perhaps, much later.

Exactly. Pushing the check to the caller makes it more likely that you
can prove it's true statically.

E.g. suppose you read a number from the keyboard, and pass it around,
store it in a data structure, retrieve it from the data structure, and
then divide by it. The "read" part should do input validation, or else
there's a bug. If all the subtypes of those parameters and data
structures had a "cannot equal zero" invariant, then the bug is isolated
to the "read" part. And if that part says "if Value /= 0 ..." then
it's easy to prove that the bug is not there.

- Bob