Re: GNAT packages in Linux distributions

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

On Sat, 15 May 2010 20:39:46 +0200, Georg Bauhaus wrote:

> On 5/15/10 11:30 AM, Dmitry A. Kazakov wrote:
> 
>> Compute should have the contract: if the sequence A,B is sorted then ...
>> else Constraint_Error propagated. And of course, A, B is just an interval
>> [B, A], and should be declared as such:
>>
>>     function Compute (X : Interval) return Number
>>        with Precondition =>  True;
> 
> OK, I guess we'd have a To_Interval (A, B) function raising
> constraint_error in case the programmer improperly passes A < B.
> Which he has learned not to do from some comment that states
> contractual obligations of client wishing to call To_Interval?

He learned that from the semantics of intervals, when he uses intervals he
supposed to know what they are.

When you write a precondition you use some premises. Consider primitive
operations of the type T. You cannot describe T in terms of T. I.e. +
cannot refer to +. So interval must be known to the programmer.

>> There is a reason why they aren't static.
> 
> Practically, yes, there is a reason why normal programming
> cannot hope to rely on static analysis.

If it could, you would not need program anything.  E.g. the result would be
obtained statically.

>>>>> IOW, no redundant checks.
>>>>
>>>> No, it would be *inconsistent* checks. No program can check itself.
>>>
>>> DbC checks are not part of the (intended) program.  Monitoring can be
>>> turned off and this should have no effect on program correctness.
>>
>> and thus on program execution. q.e.d.
> 
> The programs (with or without monitoring) are not too different
> and hence will lead to a useful program construction process.

How do you measure the difference?

>>> (a) there is nothing the programmer knows about valid Index_80
>>> values (viz. the odd ones)
>>
>> They are *all* valid, that is the contract of Careful.
> 
> I guess we disagree here:  I think that a "programming into
> exceptions" style leads to the universally applicable precondition
> True, but otherwise keeps the programmer in the dark about
> how to not make a subprogram raise.

This is what programming in Ada all about. Since the rest of the language
is by large safe, the main problem is debugging exceptions. I would like
Ada having contracted exceptions rather than run-time assertions producing
more exceptions than we already have.

>>> (b) there is no debugging hook that can be turned on
>>> or off (monitoring the precondition X rem 2 = 1).
>>
>> Debugging hooks do not belong to code.
> 
> I guess my wording was too unspecific.  Call it tracing
> automatism or whatever.

Nope, the key feature of tracing is that it does not change the program's
behavior. Assertions with handled exceptions do change it. It is a very
poor debugging tool.

I would prefer a decent debugger to run-time assertions. Make it remember
the break conditions between runs. That would be helpful and consistent.

>> You have to define "possible value":
> 
> In the sense of DbC:  values that client can pass without
> violating the DbC contract.

And contract is of course a predicate of that set of values? Nice circular
definitions.

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