Re: Structured exception information

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Wed, 17 Jan 2007 18:38:21 GMT, Jeffrey Carter wrote:

> 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.

I think that stress on compile-time checks is to some extent misleading. In
my view, the issue is not "when", but "who" performs the checks.
Correctness checks cannot be performed by the same program. In the case of
static checks, it is just so that the compiler program P2 checks my program
P1. If I wished to check my program at run-time, I should have a run-time
checker P3. For that matter, it could well be a part of Ada run-time
library, provided it were good insulated from my P1. But in all cases, when
P2 or P3 detects that P1 is incorrect (not Ada), then P1 cannot be
continued. The checker is free to start some third (Ada) program, though.

For this reason exception propagation in P1 were fundamentally flawed. We
cannot pretend that P1 has any scope which wasn't spoiled by the bug.

> In general, though, preconditions are a useful tool for documenting SW, 
> especially SW that will be used by people other than the developer. It's 
> a useful way of communicating to the client what he needs to ensure in 
> order for the SW to function normally (this condition must be true), and 
> the consequences of failing to do so (this exception is raised).

To me this is a contract: x/y yields a mathematically correct result or
else it propagates an exception when, for example, y=0. I.e. it is legal to
write 1/0 and the precondition is True.

If the precondition were y/=0, then 1/0 would be illegal and nothing could
be done about it.

> Ideally, you'd use the same syntax for both uses of preconditions. 

I think is a difficult question. The languages of P1 (my program) and of P2
(a checker of) could be sufficiently different, by necessity. On the other
hand, Ada compilers are written in Ada... In any case there should be a
clear visual distinction between the contracts and the things checking the
contracts. The latter are optional (=have the semantics outside P1) the
former are not (=have the semantics of P1). 

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de