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!