Code Contracts Invariant unproven.. Works fine with Contract.Assert at the end of each method

125 views Asked by At

I'm hoping someone can help me..

I have a C# class in which I have implemented a Code Contracts invariant. My methods keep throwing "invariant unproven" errors unless I explicitly assert the invariant is true.

My suspicion is that the problem derives from the use of void return type?

[ContractInvariantMethod]
private void FooInvariant()
{
    Contract.Invariant(!(Foo1.GetState() == "failed") || (Foo2.Get_State() == "off"));
}

//this method works fine
public void FooBar()
{
    Foo1.IncreaseInternalInt();
    Contract.Assert(!(Foo1.GetState() == "failed") || (Foo2.Get_State() == "off"));
}

//As does this method
public void FooBarTwo()
{
    Contract.Assert(!(Foo1.GetState() == "failed") || (Foo2.Get_State() == "off"));
    Foo1.IncreaseInternalInt();
}

//This method doesn't work
public void FooBarThree()
{
    Contract.Requires(!(Foo1.GetState() == "failed") || (Foo2.Get_State() == "off"));
    Foo1.IncreaseInternalInt();
}

//This method doesn't work either
public void FooBarFour()
{
    Contract.Ensures(!(Foo1.GetState() == "failed") || (Foo2.Get_State() == "off"));
    Foo1.IncreaseInternalInt();
}

I hope I haven't dumbed this down too much.

Any help would be greatly appreciated!

0

There are 0 answers