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-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 103376,cd1591f986baca62
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2001-03-14 11:42:08 PST
Newsgroups: comp.lang.ada
Path: 
 supernews.google.com!sn-xit-03!supernews.com!news-feed.riddles.org.uk!newsfeed.direct.ca!look.ca!newsfeed.media.kyoto-u.ac.jp!newsfeed.mesh.ad.jp!osa.uu.net!sac.uu.net!ash.uu.net!world!bobduff
From: Robert A Duff <bobduff@world.std.com>
Subject: Re: AdaYY; Assertions?
Sender: bobduff@world.std.com (Robert A Duff)
Message-ID: <wcczoeocf7w.fsf@world.std.com>
Date: Wed, 14 Mar 2001 19:39:31 GMT
References: <3AAA9B7A.36B601F0@ix.netcom.com> <uk85udfln.fsf@gsfc.nasa.gov>
	<3AAFA79A.66F86B99@ix.netcom.com>
Organization: The World Public Access UNIX, Brookline, MA
X-Newsreader: Gnus v5.3/Emacs 19.34
Xref: supernews.google.com comp.lang.ada:5731
Date: 2001-03-14T19:39:31+00:00
List-Id: <comp.lang.ada>

Lao Xiao Hai <laoxhai@ix.netcom.com> writes:

> Pre-conditions
> 
> These could be applied to a subprogram or a data type.

I don't understand what a precondition on a type would mean?
Perhaps you meant to say "invariant"?  IMHO, invariants should apply to
types and packages.

> I personally have a problem with the retry semantics, but it seems to be
> effective
> with Eiffel.  Not sure about all the implications for Ada.

I don't like the "retry" thing in Eiffel.  It's no better than a goto
statement.  In fact, it's the worst kind of goto, because it jumps
backwards into the code, rather unexpectedly.  And Meyer's arguments in
favor of retry, based on assertions and whatnot, don't hold water.

> I do believe that run-time is the wrong place to find a pre-condition
> error.   It is too
> late in the process.  However,  if the pre-condition error can be detected
> at run-time
> and corrective action other than an exception handler be taken, perhaps it
> has some
> virtue.

The "obvious" thing to do with a precondition failure in the Ada context
is to raise an exception.  I have thought a lot about how to move this
checking to compile time -- it's not easy.  The same comments apply to
the run-time checks that already exist in Ada.

> These should apply to the type/class.   Invariants should be inherited.
> Eiffel allows overriding of the
> invariant (they call it something else, but same general effect).

I don't recall any way to override an invariant in Eiffel.  The
invariant of the parent class is automatically "and"-ed to the new
invariant (as far as I remember).

- Bob