Re: rant (Re: Ada featured in Doctor Dobb's Journal )

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

On Sat, 17 May 2008 11:56:33 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
>> On Sat, 17 May 2008 10:28:06 +0200, Ludovic Brenta wrote:
>> 
>>> I strongly prefer compile-time checks over run-time checks,
>> 
>> Yes, actually contract checks have to be strictly static.
> 
> I think there is a HALTing problem here.

You mean that checking is undecidable? Yes, this is BTW independent on when
you check. But self-correctness checks are worse that undecidable, they are
inconsistent. Consider

require True;
function X return Boolean is
begin
   if Correct (X) then
      return False;
   else
      return True;
   end if;
end X;
ensure
   (return = False and Correct (X))
or
   (return = True and not Correct (X));

So

   Correct (X) =
= (require => ensure)
= ensure

But these are not equal, let result = True

   Correct (X) = not Correct (X)

So it is better to check what is possible either at compile time, or maybe
by another program at run-time. In either case, there is no way to continue
if a check fails. You continue either the source editor, or the supervising
program.

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