Re: GNAT packages in Linux distributions

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

On 5/13/10 10:39 AM, Dmitry A. Kazakov wrote:

>>     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's strong types are not really strong enough to express
a supplier library's ADT expectations in the sense of DbC.
Subtypes (or the type system) would need to by more specific for that.

One OOSC2 example is easily handled by Ada's subtypes,
though.

It also shows that DbC does *not* assume contracts should
necessarily become a meaningful part of your executing program,
i.e. have the program do assertion monitoring. On the contrary.

    function sqrt(x: REAL) return REAL;
    pragma Precondition (X >= 0.0);
    --  and something like pragma
    --- Postcondition (sqrt'Result * sqrt'Result = x);

    function Sqrt(x: REAL) return REAL is
    begin
       ...
    end Sqrt;

(The requirement that X >= 0.0 on entry will actually be part of
a translated *Ada* program if REAL above is defined as a
subtype of some type that includes values below 0.0.
The check is not necessarily part of a corresponding Eiffel
program that has require X >= 0.0.)
Anyway, wherever the Ada compiler sees that a value passed to Sqrt
is < 0.0, it can warn at least.

The following would *not* be a DbC style Sqrt:

    function Sqrt_Not_DbC (X: REAL) return REAL is
    begin
       if X < 0.0 then
	 -- "Handle the error, somehow"
       else
	 -- "Proceed with normal square root computation"
       end if;
    end Sqrt_Not_DbC;   -- cf. OOSC2, p.343

Instead, supplier is supposed to write the program Sqrt as if
X >= 0.0 on entry.  Only if X >= 0.0 can client legitimately expect
supplier's Sqrt to terminate in a state that satisfies the postcondition
and INV.  (INV is probably just True here.)


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

'First and 'Last are invariants of the type and they express
preconditions when reinterpreted in the normal DbC way.
Again, can you produce a statically checked invariant for
subtype Even?


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

It says that the client of Compute would have to provide
A, B such that A >= B if client expects Compute to produce
its postcondition; otherwise, the expectation is unjustified
and Compute is not bound by the contract, i.e. may fail and
produce whatever, including an exception.

The contract here is this:
I, client, give you, Compute, numbers A and B that are as
you told me.
I, Compute, will produce my Postcondition if you give me
numbers A and B as I told you.



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

That's your choice then, but not DbC's, which is more
inclusive (again, statically checked subtype Even vs. X rem 2 = 0).


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

The second "/" is a DbC one.  There is a big warning sign in OOSC2 that
says,

/                \
   NO PRECONDITION
      TOO BIG
    OR TOO SMALL
\                /

While a matter of choice, there is one strict rule: "It is _never_
acceptable to deal with a correctness condition on both the client
and supplier sides."



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

When I mentioned "not reasonably be computed by the compiler" early on,
I meant that DbC should be a possible system that helps programmers.
I did not want to theorize program analysis systems that are impossible
to produce.

I can think of a DbC program with assertion monitoring turned on
and see it as a stepwise attempt at working out the correctness
properties of the program.  For example, I can see the program
crash when a new change set makes some variable have a different
value.  This value no longer meets the stated requirements of
some subprogram.  That is shown then by the run-time and I can
think again.  Preferrably think about possible mistakes in my
attempts at corectness lemmata, since otherwise this procedure
will degrade into debugging things into some state.

But DbC here yields more than dealing with exceptions and erroneous
execution in some random fashion can possibly achieve!


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

Yes. Only, a DbC system can be quite helpful in checking
my understanding of more formal "comments".


> Note, since your "preconditions" are not static,
> how can you know *what* they say, in order to do as they do?

I can write my client code such that the preconditions are
true. I know what a procondition says if I do not need to
solve hard problems to know the meaning of a predicate.
Note that DbC includes requirements that are stated in
natural language.  Of course, not even trying to write
predicates defeats the purpose of contracting between
client and supplier, assisted by the DbC system.

E.g., I read a number from input, and another number
from input.  I know that subprogram P wants one number to be odd
and the other number to be even.  (Otherwise, it does not guarantee
that it produces its postcondition.)  These are easily
tested conditions.  I know what I have to test and I know
how to test what.


>> 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.
The proof obligation rests on us, the programmers.


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

This is legitimate I'd say, but is also is a destructive omission of
what the precondition above does specify.  Yours (True) does not tell
the client programmer the conditions that by DbC will guarantee
Postcondition.  Without hardware failure or other occurrences
that cannot be expected to be handled by the Careful algorithm,
Careful must produce Postcondition provided odd Index_80 numbers
are passed for X.  But in your version,

(a) there is nothing the programmer knows about valid Index_80
values (viz. the odd ones)

(b) there is no debugging hook that can be turned on
or off (monitoring the precondition X rem 2 = 1).


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

Normal If-statements and exceptions cannot be turned off.


 > Note
> that your "DbC mindset" includes the programmer(s) into the system,
> delivered and deployed. Isn't that indicatory? (:-))

The programmer is the one ingredient that matters most in DbC,
since programming is a human activity, and contracts are between
clients and suppliers of software components (classes).


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

I'm assuming this is not an input-sanitizing function.

You don't handle the exception as part of the algorithm:

        minus: INTEGER
            require Current > 1

            do
                Current := Current - 1
            end

            ensure Current + 1 = old Current

Where Ada requires "ifs" for bounds checking and raising an
exception accordingly, DbC/Eiffel requires that you express the
correctness properties of subprograms *and* that you choose
whether or not you want the "if", and which ones.


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

This specifies that assigning -1 to a positive will raise an exception.
It does not specify the possible values for Even (which would be
constrained to include only even numbers).