Detected call to method 'System.Diagnostics.Contracts.Contract.Invariant(System.Boolean)' without [Pure] in contracts of method ...

Question

Hi

I'm having trouble creating object invariants for my class. I wish to express that, until the object has been explicitly initialized (it has an Init() method), the stored "ValueType" (which is an Integer enum) must be "Undefined". And, after initializing, the ValueType should be NOT "Undefined":

  <ContractInvariantMethod()> _
  Private Sub ObjectInvariant()
    Contract.Invariant(IsInitialized() OrElse ValueType = Definitions.ValueType.Undefined)
    Contract.Invariant(IsInitialized() AndAlso ValueType <> Definitions.ValueType.Undefined)
  End Sub

Relevant code below (ok, it doesn't make a lot sense, but before extending, the base should be solid, right?

 

  Private m_ValueType As Definitions.ValueType = Definitions.ValueType.Undefined

  Public ReadOnly Property ValueType() As Definitions.ValueType
    Get
      Return m_ValueType
    End Get
  End Property

  <Pure()> _
  Public Function IsInitialized() As Boolean
    If m_ValueType = Definitions.ValueType.Undefined Then
      Return False
    Else
      Return True
    End If
  End Function

But after compiling I get this warning, (from the code rewriter?) :

 

Detected call to method 'System.Diagnostics.Contracts.Contract.Invariant(System.Boolean)' without [Pure] in contracts of method 'ValueTypeControl.ObjectInvariant'. 

The called function is marked pure, and I gathered that property getters are also considered Pure by Code Contracts. So what is causing this?

Thanks for helping me out!

Joachim

 

Answer 1

Hi Joachim,

Try removing one or the other and see if the error goes away, to narrow down the problem.

Also consider using a nullable value to indicate "undefined".

- Dave

---

http://davesexton.com/blog

Answer 2

I'm not sure about the error, but your invariant does not express what you have described. Your second invariant statement says that IsInitialized should ALWAYS be true AND ValueType should ALWAYS not be Undefined. That is not what you want. What you want is an exclusive-or comparison:

Contract.Invariant(IsInitialized() Xor ValueType = Definitions.ValueType.Undefined

Either IsInitialized is false and ValueType is Undefined, or IsInitialized is true and ValueType is not Undefined.

---

Moderator | MCTS .NET 2.0 Web Applications | My Blog: http://www.commongenius.com

Answer 3

I'm not sure about the error, but your invariant does not express what you have described. Your second invariant statement says that IsInitialized should ALWAYS be true AND ValueType should ALWAYS not be Undefined. That is not what you want. What you want is an exclusive-or comparison:

 

Contract.Invariant(IsInitialized() Xor ValueType = Definitions.ValueType.Undefined

Either IsInitialized is false and ValueType is Undefined, or IsInitialized is true and ValueType is not Undefined.

 

---

Moderator | MCTS .NET 2.0 Web Applications | My Blog: http://www.commongenius.com

It doesn't explain the errior, but it's certainly helpful and absolutely right - thanks for saving me some nasty bughunting :)

Answer 4

Hi Joachim,

Try removing one or the other and see if the error goes away, to narrow down the problem.

Also consider using a nullable value to indicate "undefined".

- Dave

---

http://davesexton.com/blog

Hi,

The error stays even if I put simply:

<ContractInvariantMethod()> _
 Private Sub ObjectInvariant()
  Contract.Invariant(IsInitialized() )
 End

 

I'm starting to think that the error not caused at all by something in this code, but by a problem in some other public method? Code rewrite would put the invariants logic in all public methods, right? (If that's the case, which I'll test later, that warning is no better than just "An error occured" :P )

 

thanks,

Joachim

Answer 5

 

OK, I copied into a test class and started removing things to narrow down. This is now the full code:

 

Imports System.Diagnostics.Contracts

Public Class test


 <ContractInvariantMethod()> _
 Private Sub ObjectInvariant()
  Contract.Invariant(m_ValueType <> 0)
 End Sub

 Private m_ValueType As Integer = 0



End Class

But the erors stays:

Detected call to method 'System.Diagnostics.Contracts.Contract.Invariant(System.Boolean)' without [Pure] in contracts of method 'test.ObjectInvariant'. 

Is there something essential I'm overlooking ?

 

Answer 6

Hi,

I can't repro with just that code.  The only warning that I get is:

Warning 1 CodeContracts: invariant is false: m_ValueType <> 0 Test.vb 11 10 TestContracts.VB

Is that the only code in your test project?

- Dave

---

http://davesexton.com/blog

Answer 7

Hi,

No I just created a blank class in the project. But indeed, the above code in a blank test project does not create that warning. I.e., it's not the class itselft.

So now what? Something somewhere in my project is causing this error? How do I start to find it, if that's the only warning I get? Nowhere in the project this Test class is referenced!

 

Thanks for input already, btw !

- Joachim

Answer 8

Hi Joachim,

I guess it's a bug in Code Contracts.  Maybe the CC team will investigate...

- Dave

---

http://davesexton.com/blog

Answer 9

Sorry about the problem! If it doesn't reproduce in the small standalone example in a clean project, then I will need your whole solution to debug it. Can you put it in a zip file and send it to me?

---

Mike Barnett

Answer 10

Hello everyone.

Same here, but my problem was caused by some garbage (not even a file path) in "Extra Contract Library Paths" I leave by mistake. Maybe this will help someone else with same problem in the future.

Best regards,

  Baal