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.3 required=5.0 tests=BAYES_00,INVALID_MSGID
	autolearn=no autolearn_force=no version=3.4.4
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: f43e6,a48e5b99425d742a
X-Google-Attributes: gidf43e6,public
X-Google-Thread: 1108a1,5da92b52f6784b63
X-Google-Attributes: gid1108a1,public
X-Google-Thread: ffc1e,a48e5b99425d742a
X-Google-Attributes: gidffc1e,public
X-Google-Thread: fac41,a48e5b99425d742a
X-Google-Attributes: gidfac41,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/25
Message-ID: <milkweed-2503971356010001@port7.chester.smallmedia.com>#1/1
X-Deja-AN: 228294525
References: <milkweed-2403972252230001@port2.chester.smallmedia.com>
 <5h8uja$p9o@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-25T00:00:00+00:00
List-Id: <comp.lang.ada>


In article <5h8uja$p9o@news.rhrz.uni-bonn.de>,
wolfgang@uran.informatik.uni-bonn.de (Wolfgang Reddig) wrote:

> 
> 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.
> 


I tried to think of a way to use local object destruction for ensure;
would be a great way to deal with multiple returns. But I could not figure
out how to give the object access to local variables or class members.
Will you give me a hint (if not a code sample)? Also, how are you testing
for invariance? Do you have a mechanism for overriding/hiding assertions,
and if so how?

Local object destruction is an excellent idea for making sure every ENTER
is balanced with an EXIT. Something like:

class AssertionMixin
{
private:
   friend class AssertionFrame;

   Identifier* identifierStack;

   AssertionMixin(); // Create stack for assertion identifiers.
   ~AssertionMixin(); // Delete stack.

   long GetStackSize();
   void SetStackSize(long stackSize);

   void PushAssertion(Identifier id);           // Adds to end of stack.
   Boolean ContainsAssertion(Identifier id);    // Searches entire stack.

   virtual void CheckInvariants() {}   // abstract
}

class AssertionFrame
{
private:
   AssertionMixin* currentObject;
   long assertionStackSize;

public:
   AssertionFrame(AssertionMixin* object)
   {
      currentObject = object;
      assertionStackSize = currentObject->GetStackSize();
      currentObject->PushAssertion(lock_invariance);
   }

   ~AssertionFrame()
   {
      currentObject->SetSize(assertionStackSize);
      if (!currentObject->ContainsAssertion(lock_invariance))
          currentObject->CheckInvariants();
   }

   void PushAssertion(Identifier id)
      { currentObject->PushAssertion(id); }

   Boolean ContainsAssertion(Identifier id);
      { return currentObject->ContainsAssertion(id); }
}

#define REQUIRE(identifier, expression)                           \
   if (!frame.ContainsAssertion(identifier))                      \
   {                                                              \
      frame.PushAssertion(identifier);                            \
      if (!(expression))                                          \
         (AssertionFailed(__FILE__, __LINE__, eRequire,           \
            #identifier, #expression));                           \
   }                                                              \

#define FRAME_ASSERTIONS                                          \
   AssertionFrame frame(this);                                    \


Note that the reference to AssertionFrame::ContainsAssertion in REQUIRE
forces the programmer to declare an AssertionFrame in their method before
they can use require! This is a nice safety feature. Also, the
AssertionFrame members may be inlined.

Adding the mixin class is a nuisance, but extending it to create a
separate assertion stack for every class instance means we don't need to
push the current object on the stack. This strategy also improves
execution speed, though at the cost of more overall memory usage.
Unfortunately, one would probably want to turn all this functionality off
for production code.

Usage:

void Person::Marry(Person other) : public AssertionMixin
{
      FRAME_ASSERTIONS;

      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);
}

Anders.

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