I've run into another interesting problem with the invariant section.  Let's say I have the following setup.

import random;

class Foo
{
  void changeState()
  {
    if(a)
      a = 0;
    else
      a = rand()+1;
  }

  invariant
  {
    assert(a >= 0);
  }

  int a;
}

class Bar : Foo
{

  void changeState()
  {
    super.changeState();

    if(a)
      b = rand();
    else
      b = 0;
  }

  int b;

  invariant
  {
    assert((a && b) || !(a || b));
  }
}

int main(char[][] argv)
{
  Bar c = new Bar();

  c.changeState();

  return 0;
}

Now this code will generate an assertion failure from Bar's invariant section.  The problem is that Bar's changeState() will leave the object in a correct state according to the test in the invariant section.  However, the call to super.changeState() in Bar.changeState() calls the invariant section also.  After this call the object is in a transition state that is invalid so the invariant section generates an assertion failure.

Now I am of the opinion that calls from a member function to another member function of the same class should not be subject to an invariant test.  However I can see implementation issues with this.

Another interesting point of note is that if Foo's invariant section is removed then this program will no longer generate an assertion failure.

The invariant test is done only on public member functions, the end of constructors, and the beginning of the destructor. The solution to the problem below is to make a protected function changeState() in the base class. -Walter

"Patrick Down" <pat@codemoon.com> wrote in message news:Xns92ECD79FE127Epatcodemooncom@63.105.9.61...
>
>
> I've run into another interesting problem with the invariant section.  Let's say I have the following setup.
>
> import random;
>
> class Foo
> {
>   void changeState()
>   {
>     if(a)
>       a = 0;
>     else
>       a = rand()+1;
>   }
>
>   invariant
>   {
>     assert(a >= 0);
>   }
>
>   int a;
> }
>
> class Bar : Foo
> {
>
>   void changeState()
>   {
>     super.changeState();
>
>     if(a)
>       b = rand();
>     else
>       b = 0;
>   }
>
>   int b;
>
>   invariant
>   {
>     assert((a && b) || !(a || b));
>   }
> }
>
> int main(char[][] argv)
> {
>   Bar c = new Bar();
>
>   c.changeState();
>
>   return 0;
> }
>
> Now this code will generate an assertion failure from Bar's invariant section.  The problem is that Bar's changeState() will leave the object in a correct state according to the test in the invariant section.  However, the call to super.changeState() in Bar.changeState() calls the invariant section also.  After this call the object is in a transition state that is invalid so the invariant section generates an assertion failure.
>
> Now I am of the opinion that calls from a member function to another member function of the same class should not be subject to an invariant test.  However I can see implementation issues with this.
>
> Another interesting point of note is that if Foo's invariant section is removed then this program will no longer generate an assertion failure.