Private member inaccesible in contract

Jul 14, 2010 at 11:51 AM
Hello, in the following code, Spec# complains that "A.a" is inaccesible du to its protection level. I can get rid of this error message by declaring "a" public. I feel that a contract of a method should have acces to a private member. What is wrong? using System; using Microsoft.Contracts; class A { int a; invariant 0 <= a; public void foo(int k) requires 0 <= k <= a; { a -= k; } } Regards, Boris
Jul 14, 2010 at 6:40 PM
Ok, after having advanced to section 7 of the tutorial, I understand why this doesn't work. However, the error message could be improved to eg "Access to private members is not allowed in precondition of public method. Use a public getter method instead." Users may be tempted to just change the protection level from private to public.
Jul 15, 2010 at 9:06 AM

Just include

using Microsoft.Contracts;

at the start of your file.

Then prepend your int declaration like this:

[SpecPublic]int a;

I think this basically makes your variable publically visibile to the specification tools while not altering its actual privacy level in C#.

There's one or two other issues in your code though.