Re: MI is sloppy

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

On Fri, 12 Dec 2008 18:08:12 -0600, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:43lprrmyik2q.1esp72deqcw6o.dlg@40tude.net...
>> On Fri, 12 Dec 2008 13:15:35 +0100, Georg Bauhaus wrote:
>>
>>> Dmitry A. Kazakov schrieb:
>>>
>>>>> If you have an ambitious compiler, it might reach out,
>>>>> at compile time, for objects whose behavior is then known
>>>>> to be constrained by membership in a then known specific
>>>>> subtype.
>>>>
>>>> ... and then inline raising Constraint_Error. Great!
> 
> For some reason, I didn't get the other messages to this thread.
> 
> But that's not what I'm suggesting. First of all, this is a contract 
> failure; it has it's own dedicated exception (maybe Assertion_Error).

Does it change anything?

> In 
> addition, I think compilers should be allowed to reject any program in which 
> that it can be determined statically that the contract exception will 
> unconditionally be raised.

If exceptions where *statically* contracted I would accept assertions (not
preconditions) raising them.

> What a programming language can't do is mandate 
> the cases in which that detection will occur.

Why? That looks simple:

procedure Foo raise Constraint_Error and not Assertion_Error;

declare
   raises not (Constraint_Error or Assertion_Error);
begin
   if False then
      Foo;
   end if;
end;  -- Compile error, the block may propagate
      -- Constraint_Error, because Foo can

The estimation is conservative, it ignores that Foo would eventually never
called.

> That will depend on the tools 
> you use; a really good tool should be able to detect just about everything 
> statically. (In addition, you could use an exception contract to force this, 
> or the program would also be illegal.)

Not an addition (to having nothing), but how things should work, IMO.

>>> Deriving another type, even if not sufficiently different
>>> from the original to warrant a type, is another formal
>>> way to trigger the same effect on the programmer, at compile
>>> time: "There is something odd about your program".
>>
>> No, the effect is fundamentally different. The effect is that the program
>> becomes illegal, it may not run.
> 
> That's exactly what is possible with the contracts that I'm suggesting. But 
> it cannot be mandated; we have to leave to the tools vendors to describe 
> what is possible to detect statically (after giving them the framework).

Leaving legality to vendor tools? Shudder...

>> 2. There is no minor differences in terms of correctness. An incorrect
>> program is incorrect.
> 
> You are definitely wrong about this, at least in a finite world. The cost to 
> fix some technically incorrect programs (in manpower, performance, 
> useability, etc.) is greater than the cost of the error occurring. Such 
> programs might be technically incorrect, but they're practically correct. 
> This the reason that we tolerate erroneousness in the language definition. 
> And it's the reason that we use exception handlers.

It is an empiric estimation which nobody can tell how close to reality it
is. You can declare any program correct if it will never be started. In
order to make such estimations any scientific, you have to enumerate all
program states, attach a cost of failure to each one and the probability
that the program traverses the state. Basically, what certification process
does. Now, because this is technically (and economically) impossible, you
usually estimate the program behaviour, based on the assumption that it was
implemented more or less correctly. Now the vicious circle is closed.

This is a psychotherapy, no more. I don't argue that it does not work. It
does. This is why you mailer cannot see all messages in this group... (:-))

>> There is no *any* way to predict the effect of incorrectness.
> 
> That is surely not true. An Ada bounded error occurs in a program that is 
> incorrect, but the effect of that incorrectness is strictly bounded.

No. Bounded error defines the effect for the program execution. It does not
define the semantics of. If I wrote I := I + 2 instead of I := I + 1, that
would not be an error at all. Yet the program would be incorrect and nobody
could tell anything about the effect without knowing what the program does
and where it is deployed.

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