none
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

     

    Wednesday, August 10, 2011 7:52 AM

All replies

  • 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
    Wednesday, August 10, 2011 2:20 PM
  • 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
    Wednesday, August 10, 2011 2:51 PM
  • 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 :)
    Wednesday, August 10, 2011 7:55 PM
  • 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

    Wednesday, August 10, 2011 7:59 PM
  •  

    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
    
    
     &lt;ContractInvariantMethod()&gt; _
     Private Sub ObjectInvariant()
      Contract.Invariant(m_ValueType &lt;&gt; 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 ?

     


    Thursday, August 11, 2011 7:01 AM
  • 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
    Thursday, August 11, 2011 1:17 PM
  • 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

    Thursday, August 11, 2011 6:16 PM
  • Hi Joachim,

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

    - Dave


    http://davesexton.com/blog
    Thursday, August 11, 2011 6:19 PM
  • 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
    Thursday, October 20, 2011 4:38 PM
    Owner
  • 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

    Friday, March 30, 2012 4:47 PM