Re: about the new Ada 2012 pre/post conditions

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

On Fri, 6 Jul 2012 19:43:08 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:13p2n1ve6lbrc.yr8d2a5ljm8$.dlg@40tude.net...
>> On Wed, 4 Jul 2012 21:18:24 -0500, Randy Brukardt wrote:

>>> Exactly. You claim that there cannot be such a thing as a dynamically
>>> enforced contract.
>>
>> Absolutely. How could you enforce a contract which has been *already*
>> violated? If a program reaches an illegal state, it is in that state.
>> Period.
> 
> Illegal /= Wrong. An illegal state cannot be reached because you can't 
> compile the program. An incorrect state can be reached simply by violating a 
> check or contract.

"violating the contract enforced by the contract check", you should have
said.

>>> But handling exceptions raised for contracts does not make the program 
>>> any less wrong;
>>
>> Really? What is the purpose of the exercise? Raising exception, rolling the
>> stack, finalizing stuff, and so on only to resign that the program is as
>> wrong as it was before? (Maybe it is even *more* wrong than it was? (:-))
> 
> Practicality -- it's not possible to find all program errors before a 
> program is fielded.

No practical reasons may do wrong right. I see no practical gain in calling
implementations contracts.

>>>>> The only kind of correctness checks that *can* exist in general are dynamic.
>>>>> Ada's entire reason to exist is to include checks like range checks and
>>>>> overflow checks to programs. Without them you get the buffer overflows
>>>>> and other errors that plague C code.
>>>>
>>>> Yes, but irrelevant. These checks are not contract checks, because,
>>>> otherwise you are in contradiction. No words can change that.
>>>
>>> Certainly not if you insist on using an unnecessarily limiting definition of
>>> "contract".
>>
>> Yes, the contract as opposed to the implementation limits the former not to
>> be the latter [POV #2]. But I am all open to accept that Eiffelesque/Ada
>> 2012 "contracts" are implementations [POV #1]. Do you?
> 
> No, because I use a very different definition of these terms.
> 
> Contract is roughly equivalent to (Ada) specification. Implementation is 
> roughly equivalent to (Ada) body.

That does not change anything. There are two kind entities involved A and
B. The check may be attributed to either A or B. It is not a question of
terminology.

>> The actual fallacy is in pretending that a bug can be handled. You can
>> handle/be in only anticipated states.
> 
> Really? That's certainly not true of my web server or many other programs.
> 
>    exception
>         when Err:others =>
>               Log_Error (Err);
>               Reset_to_Known_Good_State;
>
> The above is that the bottom of most of my tasks. I have no idea what state 
> the task is in when it gets to this handler;

But you have some ideas about the state of the log, about the meaning of
the object Err, about the overall state of your program, such that
Reset_to_Known_Good_State might work.

> I suppose you'll twist the terminology around in some bizarre way to claim 
> that an unanticipated state - which is the only way to reach this handler - 
> is somehow anticipated simply because I can write a handler for it.

Yes. Merely by the fact that the program continues.

Think about it from the angle of preconditions. In ANY state of the program
the preconditions of this state are met. You are going to do

   Log_Error (Err);
   Reset_to_Known_Good_State;

BECAUSE the precondition "some unhandled exception is propagating" is TRUE.
(Would you claim that precondition FALSE?)

>>> [As an aside, this means you do not want real exception contracts, since
>>> they cannot usefully be done without having it be implementation-defined
>>> when an exception is raised by a predefined check. The canonical semantics
>>> of Ada would require assuming that every line raises Storage_Error,
>>> Program_Error, and usually Constraint_Error -- that would make it virtually
>>> impossible to eliminate those exceptions from contracts.
>>
>> I don't see it as a big problem. There is a difference between an
>> obligation to raise exception and a possibility that an exception could be
>> raised.
> 
> No one cares about an "obligation to raise an exception";

Numeric errors, e.g. overflow and zero-divide must raise.

Another important example is when a constructing operation is implemented
like:

  function Create (...) return Boo is
  begin
      raise Use_Error; 
      return Boo;
  end Create;

>> The vendors could gradually reduce the number of cases where E may be
>> raised without making clients relying on weaker contracts illegal. The
>> second cannot be misused to prove that E is raised. It just does not 
>> follow from the second, and conversely.
> 
> I don't see this at all. Once you call a routine that has a contract that 
> says "E might be raised", you have to include "E might be raised" in your 
> contract as well.

No.

1. It is always "E might be raised AND Condition." It might be possible to
prove not Condition. E.g. x + y might raise Constraint_Error if sum is out
of range (or else yield the mathematically correct result). If you can
prove x + y in the range, you don't have Constraint_Error.

2. It you cannot prove not Condition, you still can handle E.

The main practical purpose of exception contracts is to ensure them
handled, rather than attempting to prevent exceptions from being raised.

> This "poisoning" is the major objection to exception 
> contracts in practice.

It cannot be otherwise. Any uncertainty about the condition when an
exception may appear is necessarily propagates to all clients. This cannot
be changed otherwise than by reducing uncertainty:

- at the client side, e.g. through 1 or 2.
- at the callee's side, e.g. strengthening the condition.

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