Re: GNAT packages in Linux distributions

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

On Thu, 13 May 2010 04:03:38 +0200, Georg Bauhaus wrote:

> All of these features of C have merits besides what else
> they may have.  But they sure don't warrant dismissing DbC?

No. The point was about lack of substance in DbC as promoted by Eiffel.

>    Ada seems better here.  But before the arrival of preconditions
> etc. Ada didn't have that much to offer to programmers wanting
> to state sets of permissible values, for example for subprogram
> parameters.

Ada has strong types. "A set of permissible values" does not look like
that.

> Ada subtypes, e.g. scalars, are poorly equipped for this style of
> value set specification, AFAICS.  They do establish two implicit
> preconditions (>= S'First and <= S'Last).

These are not preconditions, but invariants.

> A Qi style type system could do more via types but is not to be in Ada
> any time soon, is it?

I don't know. If Ada designers will keep on driving Ada into a dynamically
typed language, then probably never.

> package P is
> 
>    type Number is range 1 .. 10;
>    function Compute (A, B: Number) return Number
>      with Precondition => A >= B;

I don't understand this notation.

> (Such specifications, if they were to be being static, would exclude
> a test of A in relation to B at run time,

You need not to specify anything you cannot check... As somebody said, do
not check for bugs you aren't going to fix. (:-))

> A distinguishing property of DbC visible here is
> that a programmer will *see* the contract (or part thereof).

I do not accept "preconditions" in the operations, which are not statically
true:

   function "/" (X, Y : Number) return Number   -- Wrong!
      pre : Y /= 0.0;

   function "/" (X, Y : Number) return Number   -- Right!
      post : result = X/Y or else Constraint_Error;

>>> Which set of "specifications" has only static things in it?
>>> Why exclude conditionals whose results cannot reasonably
>>> be computed by the compiler but
>>>
>>> (a) can be computed for every single case occuring in the
>>> executing program
>>
>> If they can for *every* case, they are statically checkable, per
>> definition.
> 
> "Every case" cannot "reasonably be computed by the compiler".

Either they can or cannot. You said they can, but then added "unreasonably
can",  or "reasonably cannot", whatever. Sound like Eiffel's contracts, x
is even, not really even, we wanted it be even... (:-))

>>> (b) can guide the author of a client of a DbC component?
>>
>> I don't know what does it mean technically.
> 
> Contractually, it means "do as the preconditions say."

Like "do as comments say"? Note, since your "preconditions" are not static,
how can you know *what* they say, in order to do as they do? Eiffel masters
with easily. Its DbC is "do as you want, we'll see later." But I think that
the honor of inventing this design principle by right belongs to C...

>   "Under no circumstances shall the body of a routine ever
>    test for the routine's precondition." -- OOCS2, p.343
> 
> IOW, no redundant checks.

No, it would be *inconsistent* checks. No program can check itself. Eiffel
pre- and postconditions fall into this category.

Of course, I can imagine a compiler which would use a separate CPU core to
check pre- and ponstconditions at tun-time. but that is beyond the point.

>>> For example, assume that Is_Prime(N) is a precondition of sub P.
>>> Furthermore, TIME(Is_Prime(N))>>  PERMISSIBLE_TIME.
>>> Then, still, PRE: Is_Prime (N) expresses an obligation,
>>> part of a contract:  Don't call P unless N is prime,
>>> no matter whether or not assertion checking is in effect.
>>
>> char X [80];  // Don't use X[80], X[81], no matter etc.
> 
> Yes, and don't use X[-200]. But you can. OTOH:
> 
>    function Access_Element (S: String_80; X: Index_80);
> 
>    function Careful (S: String_80; X: Index_80)
>      with Precondition => X rem 2 = 1;
> 
>   How would you write a statically checked version?

Trivially:

   function Careful (S: String_80; X: Index_80)
      with Precondition True;
      with Postcondition <whatever> or Constraint_Error

>>> (A DbC principle is that assertions are *not* a replacement
>>> for checking input (at the client side).)
>>
>> Exactly. Assertion is not a check. You said this.
> 
> What check means, exactly, is important.

Error_Check (P) => P is incorrect

other things you mentioned are control flow control statements. It is
really simply: an error/correctness check is a statement about the program
behavior. If-statement/exception etc is the program behavior.

>>>>> What is "breach of contract" in your world?
>>>>
>>>> A case for the court.
>>>
>>> What's the court (speaking of programs)?
>>
>> A code revision.
> 
> How do you become aware of a broken contract?
> Statically? Dynamically?

Me? I am not a part of the system. These terms do not apply to me. Before
going any further, you should define the system under consideration. Note
that your "DbC mindset" includes the programmer(s) into the system,
delivered and deployed. Isn't that indicatory? (:-))

>>> I'm a programmer.  If I "design" anything, it is a program whose
>>> parts need to interact in a way that meets some almost entirely
>>> non-mathematical specification.
>>
>> Mathematics has nothing to do with this. It is about a clear distinction
>> between a contract and a condition, how undesirable it could be but
>> nevertheless it is a condition, which you, as a programmer are obliged to
>> consider as *possible*. Eiffel gives you an illusion of safety.
> 
> No.  Eiffel marketing claims that a fully proven DbC program
> is 100% bug free.

I can imagine Microsoft marketing doing same, if they didn't already...

>> Simply consider
>> the following rule: my program shall handle each exception I introduce.
>> Objections?
> 
> No objection.
> 
>> Then consider exceptions from assertions.
> 
> That is what Eiffel's rescue mechanism is about.

And how do you rescue from:

   function "-" (X : Positive) return Positive;

Note, if you handle an exception then it is same as if-statement. (I agree
that if-statements could be better arranged, have nicer syntax etc. Is that
the essence of Eiffel's DbC?)

>>>>> How would you specify
>>>>>
>>>>>     subtype Even is ...; ?
>>>>
>>>> Ada's syntax is:
>>>>
>>>>     subtype<name>  is<name>  <constraint>;
>>>
>>> What will static<name>  and static<constraint>  be for subtype Even?
>>
>> No, in Ada<constraint>  is not required to be static. Example:
>>
>> procedure F (A : String) is
>>      subtype Span is Integer range A'Range;
> 
> Is the constraint, not to be static, then part of the contractual
> specification of subtype Even?

The specification of includes all possible values of the constraint. When
you assign -1 to Positive, it is not an error, it is a valid, well-defined
program, which behavior is required to be Constraint_Error propagation.
When you assign -1.0 to Positive, it is an error and the program is
invalid. Where and how you are using these two mechanisms is up to you. A
FORTRAN program can be written in Ada, of course...

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