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: 1108a1,5da92b52f6784b63 X-Google-Attributes: gid1108a1,public X-Google-Thread: fac41,a48e5b99425d742a X-Google-Attributes: gidfac41,public X-Google-Thread: ffc1e,a48e5b99425d742a X-Google-Attributes: gidffc1e,public X-Google-Thread: f43e6,a48e5b99425d742a X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,a48e5b99425d742a X-Google-Attributes: gid103376,public From: milkweed@plainfield.bypass.com (Anders Pytte) Subject: Re: Simulating Eiffel-style assertions (was: Papers on the Ariane-5 crash and Design by Contract) Date: 1997/03/24 Message-ID: X-Deja-AN: 228139628 References: <5h6jc0$jvu@news.rhrz.uni-bonn.de> Organization: Milkweed Software Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.programming.threads,comp.lang.ada Date: 1997-03-24T00:00:00+00:00 List-Id: 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. Instead of incrementing a counter, I suggest the following. ENTER pushes a lock on invariant assertions onto the assertion stack(lock_invariance). 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; } } 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! Anders. -- Anders Pytte Milkweed Software RR 1, Box 227 Voice: (802) 472-5142 Cabot VT 05647 Internet: milkweed@plainfield.bypass.com