none
Simple contracts on System.Guid failing

    Frage

  • Per this thread, the following should work perfectly for both the String and Guid property/field.  However, while it works for the String type, apparently there's something different about the Guid type that causes the static analyzer to fail when checking this code.

    using System;
    using System.Diagnostics.Contracts;
    
    namespace MSDNForumSample
    {
        public sealed class Foo
        {
            [ContractInvariantMethod]
            private void ObjectInvariant()
            {
                Contract.Invariant(!String.IsNullOrEmpty(_bar));
                Contract.Invariant(!Guid.Equals(_id, Guid.Empty));
            }
    
    
            private string _bar;
            private Guid _id;
    
    
            public string Bar
            {
                [Pure]
                get
                {
                    Contract.Ensures(!String.IsNullOrEmpty(Contract.Result<string>()));
                    return _bar;
                }
                set
                {
                    Contract.Requires(!String.IsNullOrEmpty(value));
                    _bar = value;
                }
            }
    
            public Guid Id
            {
                [Pure]
                get
                {
                    Contract.Ensures(!Guid.Equals(Contract.Result<Guid>(), Guid.Empty));
                    return _id;
                }
                set
                {
                    Contract.Requires(!Guid.Equals(value, Guid.Empty));
                    _id = value;
                }
            }
    
    
            //public Foo(string bar)
            //    : this(bar, Guid.NewGuid())
            //{
            //    Contract.Requires(!String.IsNullOrEmpty(bar));
            //}
    
            public Foo(string bar, Guid id)
            {
                Contract.Requires(!String.IsNullOrEmpty(bar));
                Contract.Requires(!Guid.Equals(id, Guid.Empty));
                Contract.Ensures(String.Equals(Bar, bar));
                Contract.Ensures(Guid.Equals(Id, id));
    
                _bar = bar;
                _id = id;
            }
        }
    }

    Result: "CodeContracts: Checked 10 assertions: 5 correct 5 unknown"

    I'm pretty sure Guid is a value type. :)  So what's going on here?

    (Note: The constructor overload that passes in Guid.NewGuid() is also not verified - apparently there's no postcondition on Guid.NewGuid() that the result will not be Guid.Empty?)


    Lars Kemmann


    P.S.: I'm using Code Contracts 1.4.50126.1 with a .NET Framework 4.0 project, VS 2010 Pro, assembly mode = "Standard Contract Requires", "Perform Static Contract Checking" with  "Show squigglies" and "Suggest Requires" plus "Warning Level = hi".
    • Bearbeitet Lars Kemmann Freitag, 16. März 2012 23:58 Added relevant configuration details.
    Freitag, 16. März 2012 23:57