Re: GNAT packages in Linux distributions

[Georg Bauhaus <rm-host.bauhaus@maps.futureapps.de>]

On 5/12/10 11:57 PM, Dmitry A. Kazakov wrote:
> On Wed, 12 May 2010 20:53:45 +0200, Georg Bauhaus wrote:
>
>> On 12.05.10 20:33, Dmitry A. Kazakov wrote:
>>
>>>> Being better is precisely the point (of DbC).
>>>> DbC talks about proof obligations, not about provability.
>>>
>>> Who is obliged to whom in what?
>>
>> By being a programmer subscribing to the principles of DbC,
>> you are obliged to show that the components of your system
>> obey the components' contracts.  The compiler and run-time
>> try to help you achieving this goal.
>
> A C programmer would tell you same story about merits of pointers, casts
> and preprocessor.

All of these features of C have merits besides what else
they may have.  But they sure don't warrant dismissing DbC?
A C programmer is "right" when he tells an *analogous*
story that competent C programmers will avoid typical mistakes
by correct use of C features. ... whenever a competent C programmer
is defined to be one who avoids these mistakes...

A C programmer's tool set is difficult to use
for correct, portable programs.  For example,
ADTs are mostly emulated via style and conventions, by
programmers working correctly; there is little direct language
support for ADTs in C.
   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.  Or wanting to state relations required to hold
between parameters.

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).  And these little things
seem to do miracles already, judging by the model train study
of McCormick.
A Qi style type system could do more via types but is not to be in Ada
any time soon, is it?  Let alone a statically verifiable one.

Hence my insistence on a worked out example of a subtype Even
with a static specification of the intended value set, one
that can be written by a single programmer.

Alternatively, as is,

package P is

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

   type Number_Too is range 0 .. 10_000_000;
   function Compute_Too (A, B: Number_Too) return Number_Too
     with Precondition (A + B = 5_000_000);

   -- etc., with Precondition's predicate in O(P(N));

end;

(Such specifications, if they were to be being static, would exclude
a test of A in relation to B at run time, for example to reverse
their order in a recursive call as needed. It would also exclude
a simple test at run time that A + B = 5_000_000.)

A distinguishing property of DbC visible here is
that a programmer will *see* the contract (or part thereof).
Whatever implementation of Compute will later be provided,
he does not need to infer arguments in proper calls of Compute
from looking at the code of the body (or its object code).  Surely code
review can provide results insofar as there will be no
doubt about what (current!) preconditions can be inferred from
the code. The code of the current implementation!
Code review, meant as an alternative to giving preconditions,
just seems impractical in the general case. Unlike DbC.


>> 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".
Continuing the examples above.  (This argument is also somewhere
in OOSC2.)

>> (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."
And the preconditions say more than an Ada type can ever say!
A subprogram is perfect if there is little else to say than
"of this subtype", but that isn't always possible.
A responsible programmer will then write calls ensuring
that an argument is even.
Or that the first argument is greater than the second. The
client programmer can arrange for these conditions only because
he has clear, formal instructions written as preconditions.
The contract guides him, it tells what to do.

Why not have a computer language help us express these
preconditions? Some can even be checked when we develop our
software.

A paradoxical consequence of this style of invitation (to
please write your client code properly) is this:

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

IOW, no redundant checks.
Note that this is true with assertion checking on or off.
And yes, the author does say something about defensive
programming at the microscopic (routine) level: it should be
avoided in DbC systems in favor of correct software.
Have DbC help you write correct software instead.
(There is more to say here, e.g. about the "magic" that is
needed to program a correct defence...)


>> 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?


>> (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.

DbC assertion checking or monitoring can turn assertions
into run-time checks; these checks turned can be on or off,
like pragma Assert in Ada.
Input checking is something completely different.
Input to a routine comes from a programmer's call.
It is the programmer's obligation to make sure input is valid.
It is not the called routine's obligation.

Another input is I/O, which by the rules is checked
for validity, too.


>>>> 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?

Typically, I think, you notice a malfunctioning program or
an exception occurrence; same with DbC.
But DbC is also about specifying what you want before you have
an issue and before you have a result of code review.
In this sense, DbC extends an Ada spec. I guess you can
even use DbC assertions in code review comparing results
with your contracts.



>> 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't imagine that compiler makers will
claim that such a program is guaranteed to automatically
produce correct results for each input and presume that every
input can be successfully tested for validity.  They know
about SPARK and TTBOMK they won't claim DbC to effect more than
SPARK does.


> 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.
Failed assertions are one exception case (defined in $12.1 of OOSC2).
BTW, there is a rule in DbC about the correctness of
exception handlers of primitive operations.
The rule starts from a call of a primitive operation that fails
(to terminate its execution in a state satisfying the primitive
operation's contract {post(x) and INV}. The primitive operation's
exception handler is correct if it establishes its type's INV
before propagating the exception to its caller.

I am mentioning this to draw attention to the fact that DbC
is not just a thin, fluffy wrapper for "raise when" or
pragma Assert.  If it were the latter, then it would be
a bit like C style roll-your-own.


>>>> 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?