February 18, 2005
Consider the following code:

class Test
{
  int[]   array;
  uint    count = 0;

  uint    capacity() { return array.length; }

  invariant { assert( count <= capacity ); }

  this() {}
}

void main( char[][] arg )
{
  Test test = new Test();
}

This produces a stack overflow....

If I change the 'capacity' in the invariant to array.length it does not crash.

I am guessing the problem is that the invariant call capacity() also calls the invariant upon entry.

Is this improper behavior re: contracts in D or simply unspecified?

In DBC as I understand it, no contracts can fire while another contract is being checked.  Apparently this rule is not enforced in D?

-David
February 19, 2005
David Medlock wrote:

| Consider the following code:
|
| class Test
| {
|   int[]   array;
|   uint    count = 0;
|
|   uint    capacity() { return array.length; }
|
|   invariant { assert( count <= capacity ); }
|
|   this() {}
| }
|
| void main( char[][] arg )
| {
|   Test test = new Test();
| }
|
| This produces a stack overflow....
|
| If I change the 'capacity' in the invariant to array.length it does
| not crash.
|
| I am guessing the problem is that the invariant call capacity() also
| calls the invariant upon entry.
|
| Is this improper behavior re: contracts in D or simply unspecified?

http://digitalmars.com/d/class.html#invariants
# The code in the invariant may not call any public non-static members
# of the class, either directly or indirectly.

| In DBC as I understand it, no contracts can fire while another contract
| is being checked.  Apparently this rule is not enforced in D?

Known compiler bug:
http://dstress.kuehne.cn/nocompile/invariant_17.d

Thomas