Re: Ada vs Eiffel - Ada programmer approach

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

Tim Rowe schrieb:
> Ludovic Brenta wrote:

>> - in most of the examples I saw in the literature, only very simple
>> subprograms would have a contract and the contract would mostly repeat
>> the body of the subprogram. This redundancy is counter-productive.

I tought that too, but don't consider redundancy counter-productive any
more; it makes me think twice.  In fact, trying to find a post-condition
---which must be consistent with the module invariant, for
which there isn't any support in Ada yet---has forced my to simplify
program structure. :-)  Isn't that a good thing?



>> For
>> more complex subprograms, it can be very difficult to write pre and
>> postconditions and invariants; Ada's pragma Assert provides what I
>> need in these (rare) cases  because I can put such pragmas in the
>> middle of a subprogram, for example.

Eiffel has "check" and "debug" which are more specific than
pragma Assert.


> Both of the problems you describe are programming issues, not design
> issues.  There's nothing about the *design* process that mandates any
> run-time checks or that requires you to have pre- and post-conditions
> expressed in the target language. That's a matter for coding standards.
> To me, Design by Contract simply means working out and documenting in
> advance under what circumstances a section of code can legitimately be
> entered, and, if that is satisfied, what we can guarantee on exit.

This "section of code" bit is important; loop invariants and
variants are part of Eiffel DbC.  Is there a loop variant
annotation is SPARK (so far, I didn't think there was).