comp.lang.ada
 help / color / mirror / Atom feed
From: wolfgang@uran.informatik.uni-bonn.de (Wolfgang Reddig)
Subject: Re: Simulating Eiffel-style assertions (was: Papers on the Ariane-5 crash and Design by Contract)
Date: 1997/03/25
Date: 1997-03-25T00:00:00+00:00	[thread overview]
Message-ID: <5h8uja$p9o@news.rhrz.uni-bonn.de> (raw)
In-Reply-To: milkweed-2403972252230001@port2.chester.smallmedia.com



In article <milkweed-2403972252230001@port2.chester.smallmedia.com>, milkweed@plainfield.bypass.com (Anders Pytte) writes:
>In article <5h6jc0$jvu@news.rhrz.uni-bonn.de>,
>wolfgang@uran.informatik.uni-bonn.de (Wolfgang Reddig) wrote:
>
>> But these macros dont cover some of the most important aspects of Eiffel-style
>> assertions. In Eiffel, require, ensure and the class invariants are only
>> triggered for "remote-calls" (if I remember well that's what B. Meyer
>calls it).
>> Methods that directly or indirectly call methods with current (this,
>> self, ...) as the receiver wont re-trigger any assertions. This is important
>> because it 1) prevents endless loops caused by assertions and 2) allows
>> objects to be inconsistent between entrance end exit of a "remote call".
>> Consider a 'Car' class having an invariant which states that cars have
>> either two or four doors. Lets assume there is a method
>'make_limousine', which
>> adds two doors (forgive the C++ notation, but I'm not very familiar with 
>> the syntax of Eiffel):
>> 
>> void Car::make_limousine()
>> {
>>    require(no_of_doors() == 2)
>>    ensure(no_of_doors() == 4)
>> 
>>    add_door(); // this would (incorrectly) cause an invariant failure!
>>    add_door();
>> }
>> 
>> In short, C/C++ asserts do not only lack inheritance of assertions, they
>> also dont support this kind of transaction-like concept. In fact, you
>> can simulate much of Eiffel-style assertions in C++, but it requires
>> a little more work in order to be (nearly) as powerful as Eiffel. For example,
>> the 'require' macro may declare a local object whose constructor increments
>> a counter in the object. If the counter is equal to 1, then check the
>> expression passed to 'require' etc. The destructor should of course decrement
>> the counter and can automatically trigger the invariant if the counter
>> equals 1.
>
>
>Good observation! Since I had not actually tried out my suggested approach
>to class invariance, I had not encountered the limitation you pointed out.
>Since posting my suggestions, I thought of some of other problems with my
>approach. As you say, "it requires a little more work in order to be
>(nearly) as powerful as Eiffel".
>
>Sigh - my apologies to anyone who thought i had worked out all of the
>details. I hope the changes suggested below will make this technique more
>useful.
>
>For one thing, I need to push the instantiation onto the stack of
>assertions along with the identifier, so that hiding only occurs when
>calling inherited (i.e. the same method on the same instance). Also, if
>the identifiers were to be scoped (allowing use of the same identifier in
>different methods or classes), I would need to push the method or class
>signature on the stack as well. 
>
>Thanks for the suggestion of adding a counter to distinguish remote calls.
>While I agree something like that is necessary for enforcing invariance,
>could you explain why it is desirable for require and ensure? I have not
>encountered such a need in my use of these.

A must admit that I cannot come up with a practical exmaple, though I'm sure
that I had this problem sonme time ago. But consider a method 'f' which 
(directly or indirectly) calls a method 'g' in its 'require' clause and 
vice versa - you have an endless loop. Another problem might occur with 
'old' expressions: if the system were to check postconditions not only for 
remote calls, a stack of shallow copies would have to be maintained per 
object. This could at least lead to performance problems.

(BTW, calls from within a require, ensure or invariant are completely un-
checked in my implementation - is that what Eiffel compilers do, too?)

>
>Instead of incrementing a counter, I suggest the following. ENTER pushes a
>lock on invariant assertions onto the assertion stack(lock_invariance).

In our projects this would probably lead to performance problems. Accessing
counters, however, is fast. Remember that the counters need to be
in/decremented in each and every non-static member function.

>EXIT pops the immediate lock_invariance off the stack, then tests to see
>if invariance was previously locked for this instance. I suppose
>ENTER_INVARIANT and EXIT_INVARIANT could be used anywhere the object is
>known to stay consistent, but they are intended just for use in
>CheckInvariants() to avoid recursion.
>
>enum EAssertionType {eRequire, eEnsure, eInvariant, eCheck};
>
>#define ENTER_INVARIANT                                           \
>   long assertionStackSize = globalAssertionStack->GetSize()      \
>
>#define EXIT_INVARIANT                                            \
>   globalAssertionStack->SetSize(assertionStackSize)              \
> 
>#define ENTER                                                     \
>   long assertionStackSize = globalAssertionStack->GetSize()      \
>   globalAssertionStack->Push(this, lock_invariance);             \
>
>#define EXIT                                                      \
>   globalAssertionStack->SetSize(assertionStackSize)              \
>   if (!globalAssertionStack->Contains(this, lock_invariance))    \
>      CheckInvariants();                                          \
> 
>#define REQUIRE(identifier, expression)                           \
>   if (!globalAssertionStack->Contains(this, identifier))         \
>   {                                                              \
>      globalAssertionStack->Push(this,  identifier);              \
>      if (!(expression))                                          \
>         (AssertionFailed(__FILE__, __LINE__, eRequire,           \
>            #identifier, #expression));                           \
>  }                                                               \
>
>And so on for ENSURE, CHECK and INVARIANT. Here is how I would apply these
>macros:
>
>class Person: public LifeForm
>{
>private:
>
>   EGender gender;
>   EStatus status;
>   Boolean married;
>   Person spouse;
>
>protected:
>
>   virtual void CheckInvariants()
>   {
>      ENTER_INVARIANT;
>
>      INVARIANT(married_iff_has_spouse, married == (spouse != NULL));
>      INVARIANT(married_to_spouse, !married || (spouse.spouse == Current));
>      INVARIANT(married_to_other_sex: !married || (gender != spouse.gender));
>      
>      LifeForm::CheckInvariants();
>      
>      EXIT_INVARIANT;
>   }
>
>public:
>
>   void Marry (Person other)
>   {
>      ENTER;
>
>      REQUIRE(available, !married);
>      REQUIRE(other_exists, other);
>      REQUIRE(other_not_married, !other.married);
>      REQUIRE(different_gender, gender != other.gender);
>
>      // the wedding...
>
>      ENSURE(married, married);
>      ENSURE(married_to_other, spouse == other);
>
>      EXIT;
>   }
>}

But the 'ENTER' and 'EXIT' macros are not really needed. In fact, if the
programmer forgets 'EXIT', no more checks are performed until the program
terminates? That's why my 'require' macro constructs a local object whose
destructor triggers the invariant.

void Person::Marry(Person other)
{
   require(!married && !other.married && 
           gender != other.gender)
   ensure(married && spouse == other)

   // the wedding...
   Return;
}

One of the ugly things in our approach is the 'Return' - it is needed to
trigger the postcondition check. On the other hand, there is no problem
with multiple exits.

>
>As has been pointed out by Paul Johnson, there is no protection in this
>scheme of overriding assertions against strengthening a require or
>weakening an ensure or invariant. Neither are requires and ensures
>automatically inherited in a method override. So the engineer must beware!

Absolutely true. I dont program anything without my assertions, but they
are far from the power of Eiffel.

>
>Anders.
>
>-- 
>Anders Pytte            Milkweed Software
>RR 1, Box 227           Voice: (802) 472-5142
>Cabot VT 05647          Internet: milkweed@plainfield.bypass.com

Regards,
Wolfgang

+---------------------------------------------------------------------+
|  Wolfgang Reddig                |  e-mail:                          |
|  Institut fuer Informatik III   |  wolfgang@informatik.uni-bonn.de  |
|  Roemerstrasse 164              |                                   |
|  53117 Bonn                     |  Tel.: (49) 228 / 73-4513         |
|  Germany                        |  Fax:  (49) 228 / 73-4382         |
+---------------------------------------------------------------------+






  reply	other threads:[~1997-03-25  0:00 UTC|newest]

Thread overview: 247+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1997-03-15  0:00 Papers on the Ariane-5 crash and Design by Contract Bertrand Meyer
1997-03-18  0:00 ` Ariane-5: can you clarify? (Re: Please do not start a language war) Jon S Anthony
     [not found] ` <tz8ohcjv7cc.fsf@aimnet.com>
1997-03-16  0:00   ` Papers on the Ariane-5 crash and Design by Contract Robert Dewar
1997-03-17  0:00     ` Please do not start a language war (was " Jean-Marc Jezequel
1997-03-18  0:00       ` Richard Irvine
1997-03-18  0:00       ` Ken Garlington
1997-03-19  0:00         ` Jean-Marc Jezequel
1997-03-19  0:00           ` Richard Kaiser
1997-03-21  0:00           ` Ken Garlington
1997-03-21  0:00             ` Jean-Marc Jezequel
1997-03-25  0:00               ` Ken Garlington
1997-03-26  0:00                 ` Trust but verify " Robert S. White
1997-03-25  0:00                   ` Bertrand Meyer
1997-03-26  0:00                     ` Robb Nebbe
1997-03-27  0:00                     ` Ken Garlington
1997-03-28  0:00                       ` Jeffrey W. Stulin
1997-03-31  0:00                         ` Ken Garlington
1997-03-28  0:00                       ` Karel Th�nissen
1997-03-28  0:00                         ` Ken Garlington
1997-04-07  0:00                           ` Jean-Marc Jezequel
1997-03-29  0:00                     ` the one and only real true kibo
     [not found]         ` <199703190839.JAA02652@stormbringer.irisa.fr>
1997-03-19  0:00           ` Please do not start a language war " Ken Garlington
1997-03-20  0:00             ` Roger T.
1997-03-21  0:00               ` Jean-Marc Jezequel
1997-03-24  0:00                 ` Ken Garlington
1997-03-21  0:00               ` Ken Garlington
1997-03-20  0:00             ` Robert S. White
1997-03-20  0:00               ` Martin Tom Brown
1997-03-21  0:00                 ` Robert S. White
1997-03-21  0:00                 ` Wolfgang Gellerich
1997-03-20  0:00               ` John L. Ahrens
     [not found]       ` <tz8913l930b.fsf_-_@aimnet.com>
1997-03-18  0:00         ` Ariane-5: can you clarify? (Re: Please do not start a language war) Gavin Collings
1997-03-18  0:00         ` Ariane-5: can you clarify? (Re: Please do not start a language war Roedy Green
1997-03-17  0:00   ` Papers on the Ariane-5 crash and Design by Contract Alexander Anderson
1997-03-17  0:00   ` Nick Leaton
1997-03-17  0:00     ` Richard Kaiser
1997-03-18  0:00     ` Richard Kaiser
1997-03-18  0:00       ` Jean-Marc Jezequel
1997-03-19  0:00         ` Ken Garlington
1997-03-18  0:00       ` Nick Leaton
1997-03-19  0:00         ` Richard Kaiser
1997-03-19  0:00           ` Fergus Henderson
1997-03-19  0:00           ` Jean-Marc Jezequel
1997-03-19  0:00             ` Richard Kaiser
1997-03-18  0:00     ` Richard Kaiser
1997-03-18  0:00       ` Nick Leaton
1997-03-18  0:00         ` "Paul E. Bennett"
1997-03-19  0:00           ` Nick Leaton
1997-03-24  0:00           ` Joachim Durchholz
1997-03-25  0:00             ` Robert Dewar
1997-03-31  0:00               ` Joachim Durchholz
1997-04-02  0:00                 ` Robert Dewar
1997-04-03  0:00                   ` Martin Tom Brown
1997-04-04  0:00                   ` Derek Clarke
1997-04-04  0:00                   ` Jonathan Egre'
1997-04-06  0:00                     ` Robert Dewar
1997-04-06  0:00                       ` Nick Roberts
1997-03-31  0:00               ` Jan Galkowski
1997-03-31  0:00             ` Alexander Anderson
1997-04-01  0:00             ` Alexander Anderson
1997-04-02  0:00             ` Ken Garlington
1997-03-20  0:00         ` John the Hamster
     [not found]     ` <tz8g1xtzx9y.fsf@aimnet.com>
1997-03-18  0:00       ` Anders Pytte
1997-03-18  0:00         ` Jean-Marc Jezequel
1997-03-18  0:00           ` Anders Pytte
1997-03-18  0:00           ` Anders Pytte
1997-03-19  0:00             ` Programming language fanaticism! Louis Bastarache
1997-03-20  0:00               ` Anders Pytte
1997-03-20  0:00             ` Papers on the Ariane-5 crash and Design by Contract Matt Kennel (Remove 'nospam' to reply)
1997-03-24  0:00             ` Joachim Durchholz
1997-03-24  0:00               ` Anders Pytte
1997-03-26  0:00                 ` Matt Kennel (Remove 'nospam' to reply)
1997-03-29  0:00                   ` Anders Pytte
1997-03-29  0:00                     ` Steve Furlong
1997-03-26  0:00                 ` Robert Dewar
1997-03-27  0:00                   ` the one and only real true kibo
1997-03-29  0:00                   ` the one and only real true kibo
1997-03-29  0:00                     ` Nick S Bensema
1997-03-30  0:00                       ` the one and only real true kibo
1997-03-21  0:00           ` Ken Garlington
1997-03-21  0:00             ` Bertrand Meyer
1997-03-21  0:00               ` William Clodius
1997-03-21  0:00                 ` Bertrand Meyer
1997-03-23  0:00                   ` William Clodius
1997-03-23  0:00                   ` the one and only real true kibo
1997-03-22  0:00               ` Fergus Henderson
1997-03-22  0:00                 ` Bertrand Meyer
1997-03-23  0:00                   ` the one and only real true kibo
1997-03-23  0:00                     ` Anders Pytte
1997-03-24  0:00                   ` FUD (Re: Papers on the Ariane-5 crash and Design by Contract) Alexander Anderson
1997-03-24  0:00                   ` Alexander Anderson
1997-03-23  0:00               ` Papers on the Ariane-5 crash and Design by Contract Anders Pytte
     [not found]                 ` <3335BC24.13728473@eiffel.com>
1997-03-23  0:00                   ` Bertrand Meyer
1997-03-24  0:00                     ` Robert Dewar
1997-03-31  0:00                       ` Ken Garlington
1997-04-01  0:00                         ` Bertrand Meyer
1997-03-25  0:00                     ` Ken Garlington
1997-03-24  0:00                 ` Ken Garlington
1997-03-24  0:00                 ` the one and only real true kibo
1997-03-24  0:00               ` John Hogg
1997-03-24  0:00               ` Ken Garlington
1997-03-26  0:00                 ` Robert Dewar
1997-03-26  0:00                   ` Ken Garlington
     [not found]                     ` <E7ox17.MKx@syd.csa.com.au>
1997-03-28  0:00                       ` Ken Garlington
1997-03-18  0:00         ` Laurent Moussault
1997-03-17  0:00   ` Bertrand Meyer
1997-03-18  0:00     ` John McCabe
1997-03-18  0:00       ` Ray McVay
1997-03-27  0:00         ` Robert Dewar
1997-03-29  0:00           ` the one and only real true kibo
1997-03-30  0:00             ` Nick Roberts
1997-04-06  0:00             ` Doctorb
1997-04-08  0:00         ` Ron Crocker
1997-04-11  0:00           ` Richard Riehle
1997-03-17  0:00   ` Robert I. Eachus
1997-03-17  0:00     ` Martin Tom Brown
1997-03-17  0:00   ` Please do not start a language war (was " Jon S Anthony
1997-03-18  0:00     ` Kent Tong
1997-03-20  0:00       ` Ranan Fraer
1997-03-17  0:00   ` John McCabe
     [not found]     ` <tz8n2s1hrdc.fsf@aimnet.com>
1997-03-20  0:00       ` John McCabe
1997-03-20  0:00         ` Jean-Marc Jezequel
1997-03-20  0:00           ` John McCabe
1997-03-21  0:00             ` Niall Cooling
1997-03-21  0:00               ` Gavin Collings
1997-03-27  0:00                 ` Joachim Durchholz
1997-04-03  0:00                   ` Robert I. Eachus
1997-04-04  0:00                     ` Chris Beer
1997-04-04  0:00                     ` Derek Clarke
1997-04-03  0:00                   ` Gavin Collings
1997-04-03  0:00                     ` Ken Garlington
1997-04-04  0:00                       ` Derek Clarke
1997-04-04  0:00                     ` Derek Clarke
1997-04-06  0:00                       ` Robert Dewar
1997-04-07  0:00                         ` Ken Garlington
1997-04-09  0:00                           ` Gavin Collings
1997-04-04  0:00                   ` Ken Garlington
1997-04-04  0:00                     ` Robert Dewar
1997-04-03  0:00                 ` Robin Rosenberg
1997-03-24  0:00             ` Ken Garlington
1997-03-26  0:00           ` Thomas Beale
1997-03-26  0:00             ` Ken Garlington
1997-03-20  0:00       ` John McCabe
1997-03-21  0:00       ` "Paul E. Bennett"
1997-03-22  0:00     ` Nigel Tzeng
1997-03-23  0:00       ` John McCabe
1997-03-17  0:00   ` Paul Johnson
1997-03-17  0:00     ` Enrico Facchin - Sartori E.T.
1997-03-19  0:00       ` Anders Pytte
1997-03-18  0:00     ` Ken Garlington
1997-03-18  0:00   ` Tarjei Jensen
1997-03-18  0:00   ` Jon S Anthony
1997-03-18  0:00   ` Ken Garlington
1997-03-19  0:00     ` Eric M. Boyd
1997-03-19  0:00       ` Jeffrey W. Stulin
     [not found]       ` <3345cd60.2092398@news.sydney.apana.org.au>
1997-04-03  0:00         ` Ariane-5 crash , Eiffel and Ada Jeffrey W. Stulin
1997-04-03  0:00         ` Nick Leaton
1997-04-08  0:00         ` AdaWorks
1997-03-18  0:00   ` Papers on the Ariane-5 crash and Design by Contract Jon S Anthony
1997-03-18  0:00   ` Jon S Anthony
1997-03-19  0:00     ` Ron Forrester
1997-03-21  0:00       ` Ken Garlington
1997-03-22  0:00         ` Ron Forrester
1997-03-18  0:00   ` Ulrich Windl
1997-03-18  0:00   ` Jon S Anthony
1997-03-18  0:00   ` Robert I. Eachus
1997-03-19  0:00   ` Jon S Anthony
1997-03-19  0:00   ` Karel Th�nissen
1997-03-19  0:00   ` Ken Garlington
1997-03-19  0:00   ` Ken Garlington
1997-03-20  0:00     ` Richard Kaiser
1997-03-24  0:00       ` Ken Garlington
1997-03-20  0:00     ` Martin Tom Brown
1997-03-21  0:00       ` Frank Manning
1997-03-21  0:00         ` Martin Tom Brown
1997-03-23  0:00           ` Frank Manning
1997-03-25  0:00             ` Ken Garlington
1997-03-19  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Karel Th�nissen
1997-03-19  0:00   ` Papers on the Ariane-5 crash and Design by Contract Karel Th�nissen
1997-03-19  0:00   ` Nick Leaton
1997-03-19  0:00   ` Jon S Anthony
1997-03-20  0:00     ` Jean-Marc Jezequel
1997-03-24  0:00       ` Ken Garlington
1997-03-20  0:00     ` Paul Johnson
1997-03-24  0:00       ` Ken Garlington
1997-03-24  0:00         ` Design by Contract in C++ (was Re: Papers on the Ariane-5 crash and Design by Contract) Anders Pytte
1997-03-20  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Nick Leaton
1997-03-20  0:00   ` Karel Th�nissen
1997-03-20  0:00   ` Nick Leaton
1997-03-20  0:00   ` Papers on the Ariane-5 crash and Design by Contract Robert I. Eachus
1997-03-20  0:00   ` Robert I. Eachus
1997-03-21  0:00   ` Please do not start a language war (was " Jon S Anthony
     [not found]   ` <tz8sp1qiywm.fsf@aimnet.com>
1997-03-21  0:00     ` ae59
1997-03-21  0:00   ` Ulrich Windl
1997-03-21  0:00   ` Alexander Anderson
1997-03-23  0:00     ` "Paul E. Bennett"
1997-03-22  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Stuart Yeates
1997-03-22  0:00   ` Papers on the Ariane-5 crash and Design by Contract Jon S Anthony
1997-03-28  0:00     ` Matt Kennel (Remove 'nospam' to reply)
1997-03-22  0:00   ` Bertrand Meyer
1997-03-22  0:00     ` Anders Pytte
1997-03-23  0:00       ` Steve Furlong
1997-03-24  0:00         ` Anders Pytte
1997-03-24  0:00           ` Simulating Eiffel-style assertions (was: Papers on the Ariane-5 crash and Design by Contract) Wolfgang Reddig
1997-03-24  0:00             ` Anders Pytte
1997-03-25  0:00               ` Wolfgang Reddig [this message]
1997-03-25  0:00                 ` Anders Pytte
1997-03-31  0:00                 ` Joachim Durchholz
1997-03-26  0:00             ` Alan Brain
1997-03-26  0:00               ` Wolfgang Reddig
1997-03-29  0:00                 ` How old time languages survive EJon
1997-03-22  0:00   ` Papers on the Ariane-5 crash and Design by Contract Bertrand Meyer
1997-03-23  0:00     ` Dale Stanbrough
     [not found]       ` <3335E18E.33590565@eiffel.com>
1997-03-23  0:00         ` FUD (Re: Papers on the Ariane-5 crash and Design by Contract) Bertrand Meyer
1997-03-24  0:00           ` William Grosso
1997-03-24  0:00             ` Brad Appleton
1997-03-24  0:00             ` Bertrand Meyer
1997-03-24  0:00             ` William Clodius
1997-03-24  0:00     ` Papers on the Ariane-5 crash and Design by Contract Robert Dewar
1997-03-24  0:00       ` Manners (was Re: Papers on the Ariane-5 crash and Design by Contract) Bertrand Meyer
1997-03-25  0:00         ` the one and only real true kibo
1997-03-24  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Nick Leaton
1997-03-24  0:00   ` Papers on the Ariane-5 crash and Design by Contract Ken Garlington
1997-03-27  0:00     ` Joachim Durchholz
1997-03-31  0:00       ` Ken Garlington
1997-04-06  0:00         ` Joachim Durchholz
1997-03-24  0:00   ` Ken Garlington
1997-03-24  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Ken Garlington
1997-03-24  0:00   ` William Clodius
1997-03-24  0:00   ` Papers on the Ariane-5 crash and Design by Contract Robb Nebbe
1997-03-24  0:00   ` Ken Garlington
1997-03-24  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Ken Garlington
1997-03-24  0:00   ` Papers on the Ariane-5 crash and Design by Contract Jon S Anthony
1997-03-24  0:00   ` Alexander Anderson
1997-03-25  0:00   ` Ariane-5: can you clarify? (Re: Please do not start a language war) Ken Garlington
1997-03-25  0:00   ` David Starr
1997-03-25  0:00   ` Ken Garlington
1997-03-25  0:00   ` Papers on the Ariane-5 crash and Design by Contract Robert I. Eachus
1997-03-26  0:00   ` Alexander Anderson
1997-03-26  0:00   ` Jon S Anthony
1997-03-26  0:00   ` Ken Garlington
1997-03-27  0:00   ` Trust but verify (was " Robert I. Eachus
1997-03-28  0:00   ` Jon S Anthony
1997-03-28  0:00   ` Trust but verify (was " Robert I. Eachus
1997-03-31  0:00   ` Ken Garlington
1997-03-19  0:00 ` Chris Brand
1997-03-23  0:00 ` the one and only real true kibo
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox