• Patrick Down <pat codemoon.com> Dec 22 2002
• "Daniel Yokomiso" <daniel_yokomiso yahoo.com.br> Dec 23 2002

The following D program will cause a Stack Overflow.
The reason is that the invariant calls a member fuction
of the class which in turn invokes the invariant section.
Should calls to member fuctions be allowed in the invariant
section?  If so how can this problem be avoided?    

class Foo 
{
  this()
  {
  }
  
  public int func()
  {
    return 2;
  } 
  
  invariant
  {
    assert(func() == 2);
  }
}

int main(char[][] argv)
{
  Foo b = new Foo;
    
  return 1;
}

"Patrick Down" <pat codemoon.com> escreveu na mensagem
news:Xns92ECC942BF6E4patcodemooncom 63.105.9.61...
 The following D program will cause a Stack Overflow.
 The reason is that the invariant calls a member fuction
 of the class which in turn invokes the invariant section.
 Should calls to member fuctions be allowed in the invariant
 section?  If so how can this problem be avoided?

 class Foo
 {
   this()
   {
   }

   public int func()
   {
     return 2;
   }

   invariant
   {
     assert(func() == 2);
   }
 }

 int main(char[][] argv)
 {
   Foo b = new Foo;

   return 1;
 }


Hi,

    The problem here lies on recursion. It is necessary in some contracts if
you need to transvere some kind of container trying to verify some property,
e.g: comparison of sequences. But most of the times recursion just overflows
the stack, specially if you need to define symmetrical properties of
equality, comparison, etc.. IMHO we don't need recursion in contracts,
because the contract part can have arbitrary statements, including loops
used to transverse said structures. IMO it's not a great problem today, the
compiler must improve in other areas first (e.g.: implement the full spec).
And it's easy to add a dirty boolean global flag somewhere to say:

invariant {
    if (recursing) {
        recursing = false;
    } else {

        recursing = true;
        assert(func() == 2);
    }
}

   It's ugly but it works.

   Best regards,
   Daniel Yokomiso.

"You may want Star Wars compilers, but I'm no Luke Skywalker."
- Cyril Adrian


---
Outgoing mail is certified Virus Free.
Checked by AVG anti-virus system (http://www.grisoft.com).
Version: 6.0.431 / Virus Database: 242 - Release Date: 17/12/2002