locked
Proving bug RRS feed

 > 

  • Question

  • Question
    Sign in to vote
    0
    Sign in to vote
    Hi,

    see the source snippet below. CodeContracts solver doesnt manage to solve that the return code of the property Default is always not null.

    namespace ConsoleApplication1 {
    [ContractClass(typeof(ITestContracts))]
    public interface ITest {
        string Default {
            get;
        }
    }

    [ContractClassFor(typeof(ITest))]
    sealed class ITestContracts : ITest {
        string ITest.Default {
            get {
                Contract.Ensures(Contract.Result<string>() != null);
                throw new NotImplementedException();
            }
        }
    }

    public class MyTest : ITest {
        private readonly string DefaultString = "blaat";

        public string Default {
            get {
                return DefaultString;
            }
        }
    }
}
    Friday, October 23, 2009 11:24 AM

Answers

  • Question
    Sign in to vote
    0
    Sign in to vote
    Yes, thanks for the feed back. This is currently expected, as the static checker isn't trying to infer object invariants (even as trivial as this one). We are working on this support. For now you need to write an object invariant to MyTest yourself:

    [ContractInvariantMethod]
void ReadonlyInvariants() {
   Contract.Invariant( this.DefaultString != null);
}
    This will make the checker prove that all constructors (and all methods) maintain this invariant and will let you prove the ensures in the Default getter.
    Cheers, -MaF (Manuel Fahndrich)
    Friday, October 23, 2009 3:07 PM