From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Thread: a07f3367d7,5add429c86f59001 X-Google-Attributes: gida07f3367d7,public,usenet X-Google-NewGroupId: yes X-Google-Language: ENGLISH,ASCII-7-bit Path: g2news2.google.com!news3.google.com!feeder1-2.proxad.net!proxad.net!feeder2-2.proxad.net!newsfeed.arcor.de!newsspool4.arcor-online.net!news.arcor.de.POSTED!not-for-mail Date: Tue, 26 May 2009 18:37:29 +0200 From: Georg Bauhaus User-Agent: Thunderbird 2.0.0.21 (Macintosh/20090302) MIME-Version: 1.0 Newsgroups: comp.lang.ada Subject: Re: Ada vs Eiffel - Ada programmer approach References: <405b5054-4c8f-4e16-9ea8-503a9b9f976e@t21g2000yqi.googlegroups.com> <4A19765C.608@obry.net> <8105b65f-4de9-4653-b43a-d55ee33f072d@k2g2000yql.googlegroups.com> <4vCdnRo6At8-mIHXnZ2dnUVZ8n2dnZ2d@brightview.co.uk> In-Reply-To: <4vCdnRo6At8-mIHXnZ2dnUVZ8n2dnZ2d@brightview.co.uk> Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Message-ID: <4a1c1aca$0$30229$9b4e6d93@newsspool1.arcor-online.net> Organization: Arcor NNTP-Posting-Date: 26 May 2009 18:37:30 CEST NNTP-Posting-Host: c48aa906.newsspool1.arcor-online.net X-Trace: DXC=PTe7l0P>cn]U6b:FjPaGjQic==]BZ:af^4Fo<]lROoRQ^YC2XCjHcbY48SASO@aB9T;9OJDO8_SKVNSZ1n^B98iZSGCd4WI7;3^ X-Complaints-To: usenet-abuse@arcor.de Xref: g2news2.google.com comp.lang.ada:6021 Date: 2009-05-26T18:37:30+02:00 List-Id: 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).