Re: GNAT packages in Linux distributions

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

On Sat, 15 May 2010 01:45:50 +0200, Georg Bauhaus wrote:

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

No type system can express the program semantics. Otherwise you would need
not program any bodies, only declarations.

> Again, can you produce a statically checked invariant for
> subtype Even?

Yes, I can:

   type Even is private; -- No literals visible
   function To_Integer (X : Even) return Integer;
   function To_Even (X : Integer) return Even;
private
   type Even is new Integer;  -- Use literals as follows: 1 means 2

   function To_Integer (X : Even) return Integer is
   begin
      return Integer (X * 2);
   end To_Integer;

   function To_Even (X : Integer) return Even is
   begin
      if X mod 2 = 0 then
         return Even (X / 2);
      else
         raise Constraint_Error;
      end if;
   end To_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,

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;

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

You say that Eiffel DbC is about writing structured comments? I do not
object.

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

Really? What about:

pre : not HALT(p)

There is a reason why they aren't static.

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

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

They are *all* valid, that is the contract of Careful.

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

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

Come on. C has preprocessor!

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

That is what your car manufacturer will tell you next time, when the brake
system will accelerate instead of braking...

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

It was unary minus.

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

Bounds are one kind of constraints. Eiffel has more of those. Ada goes in
the same direction as Robert's response shows. I don't like it for two
reasons:

1. Dynamic checks. This was discussed. Correctness checks shall be static,
else it is a part of the behavior to be contracted as any other.

2. It is weakly/un-typed. The constraints you impose on input and output
are specifications of a [sub]type.

2.a. This type is anonymous
2.b. This type mutates (precondition /= postcondition)
2.c. This type is inferred and structurally equivalent

To me this is a deep breach with the core of Ada type system.

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

You have to define "possible value":

1. Member of the type domain set. (3 is a member of the Even as a subtype
of Integer)
2. Value of an initialized instance (3 cannot be a value of any Even
object)

(Considering Even an Ada subtype or a type inheriting to integer.)

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