Problem with nested objects and expose

Aug 9, 2010 at 12:02 PM

Hi,

I have a method call of the form

expose(this) expose(this.obj1) expose(this.obj1.obj2) {
  obj1.obj2.obj3.impure_method();
}

this owns obj1 owns obj2 owns obj3 as specified by [Rep]. Spec# complains that the target object must be peer consistent.

What is wrong with my code?

Regards, Boris

 

Coordinator
Aug 10, 2010 at 12:03 AM

Hi Boris,

I am unable to reproduce your problem.  In the program below, I have written two versions of what you describe.  One version uses a single class, the other uses four classes.  Both versions verify without complaints for me.  Can you see some difference between this and what you're trying to do?

  Rustan

using Microsoft.Contracts;

class C {
  [Rep] public C obj1;
  [Rep] public C obj2;
  [Rep] public C obj3;

  public void M()
    requires obj1 != null && obj1.obj2 != null && obj1.obj2.obj3 != null;
  {
    expose(this) expose(this.obj1) expose(this.obj1.obj2) {
      obj1.obj2.obj3.impure_method();
    }
  }

  public void impure_method()
  {
  }
}

class X0 {
  [Rep] public X1! obj1 = new X1();
  public void M() {
    expose(this) expose(this.obj1) expose(this.obj1.obj2) {
      obj1.obj2.obj3.impure_method();
    }
  }
}

class X1 {
  [Rep] public X2! obj2 = new X2();
}

class X2 {
  [Rep] public X3! obj3 = new X3();
}

class X3 {
  public void impure_method() {
  }
}
Aug 10, 2010 at 8:09 PM
Edited Aug 30, 2010 at 4:09 PM

Hello Rustan, my code that doesn't verify is structured as in this example:

using System;

using Microsoft.Contracts;



public class A {

	int k;

	

	public void foo(int _k) {

		k = _k;

	}

}



public class B {

	int k;

	[Rep] public A! a = new A();



	public void foo(int _k) {

		k = _k;

	}

}



public class Program {

	[Rep] public B! b = new B();

	

	void main() {

//		expose(this) {

//			expose(this.b) {

				b.a.foo(1);

//			}

			b.foo(1);

//		}

	}

}

This verifies however, regardless if the expose-blocks are commented out or not. I dont't know if the main program is treated differently, but if Program was a regular class it should be valid without the expose blocks, hence b not consistent. I think it didn't verify in either form with the previous release of Spec#.

Boris

P.S.: The button to include source code as well as all other formatting buttons don't always show up in Firefox 3.6.3.