为什么Code Contracts声称此代码的"确保是错误的"？

Question

这是我的一个类中的构造函数:

public SemanticVersion(string version)
{
    Contract.Requires<ArgumentException>(!string.IsNullOrEmpty(version));
    Contract.Ensures(MajorVersion >= 0);
    Contract.Ensures(MinorVersion >= 0);
    Contract.Ensures(PatchVersion >= 0);
    Contract.Ensures(PrereleaseVersion != null);
    Contract.Ensures(BuildVersion != null);

    var match = SemanticVersionRegex.Match(version);
    if (!match.Success)
    {
        var message = $"The version number '{version}' is not a valid semantic version number.";
        throw new ArgumentException(message, nameof(version));
    }

    MajorVersion = int.Parse(match.Groups["major"].Value, CultureInfo.InvariantCulture);
    MinorVersion = int.Parse(match.Groups["minor"].Value, CultureInfo.InvariantCulture);
    PatchVersion = int.Parse(match.Groups["patch"].Value, CultureInfo.InvariantCulture);
    PrereleaseVersion = match.Groups["prerelease"].Success
        ? new Maybe<string>(match.Groups["prerelease"].Value)
        : Maybe<string>.Empty;
    BuildVersion = match.Groups["build"].Success
        ? new Maybe<string>(match.Groups["build"].Value)
        : Maybe<string>.Empty;
}

Code Contracts static checker标记错误:

警告:CodeContracts:确保为false:PrereleaseVersion!= null

Maybe<T> 是一个包含零个或一个元素的集合.

据我所知,唯一可以为null的方法是在分配之前有异常,这应该使Ensures要求无关紧要.我的代码是盲目的吗？你能看出问题吗？

更新:发布Maybe的实现以响应评论.

using System.Collections;
using System.Collections.Generic;
using System.Diagnostics.Contracts;
using System.Linq;

namespace TA.CoreTypes
{
    /// <summary>
    ///     Represents an object that may or may not have a value (strictly, a collection of zero or one elements). Use
    ///     LINQ expression
    ///     <c>maybe.Any()</c> to determine if there is a value. Use LINQ expression
    ///     <c>maybe.Single()</c> to retrieve the value.
    /// </summary>
    /// <typeparam name="T">The type of the item in the collection.</typeparam>
    public class Maybe<T> : IEnumerable<T>
    {
        private static readonly Maybe<T> EmptyInstance = new Maybe<T>();
        private readonly IEnumerable<T> values;

        /// <summary>
        ///     Initializes a new instance of the <see cref="Maybe{T}" /> with no value.
        /// </summary>
        private Maybe()
        {
            values = new T[0];
        }

        /// <summary>
        ///     Initializes a new instance of the <see cref="Maybe{T}" /> with a value.
        /// </summary>
        /// <param name="value">The value.</param>
        public Maybe(T value)
        {
            Contract.Requires(value != null);
            values = new[] {value};
        }

        /// <summary>
        ///     Gets an instance that does not contain a value.
        /// </summary>
        /// <value>The empty instance.</value>
        public static Maybe<T> Empty
        {
            get
            {
                Contract.Ensures(Contract.Result<Maybe<T>>() != null);
                return EmptyInstance;
            }
        }

        public IEnumerator<T> GetEnumerator()
        {
            Contract.Ensures(Contract.Result<IEnumerator<T>>() != null);
            return values.GetEnumerator();
        }

        IEnumerator IEnumerable.GetEnumerator()
        {
            Contract.Ensures(Contract.Result<IEnumerator>() != null);
            return GetEnumerator();
        }

        [ContractInvariantMethod]
        private void ObjectInvariant()
        {
            Contract.Invariant(values != null);
        }

        [Pure]
        public override string ToString()
        {
            Contract.Ensures(Contract.Result<string>() != null);
            if (Equals(Empty)) return "{no value}";
            return this.Single().ToString();
        }
    }

    public static class MaybeExtensions
    {
        public static bool None<T>(this Maybe<T> maybe)
        {
            if (maybe == null) return true;
            if (maybe == Maybe<T>.Empty) return true;
            return !maybe.Any();
        }
    }
}

Answer 1

看来Maybe<T>类上唯一的变异方法是构造函数本身。其他所有方法都只是得到东西。因此，您可以将 放在PureAttribute类级别来向分析器暗示整个类是纯的，因为它是不可变的 - 毕竟，这不是 Maybe 的意义所在，要么您得到一些东西，要么您得到一个空 Maybe，但你永远不会为空？并且您无法更改 Maybe 中的值，只能创建一个包含新值的新 Maybe 。

另外，即使指定了对象不变量，我在使用静态分析器和使用Contract.Ensures构造函数中的属性（特别是可变属性）时也总是遇到问题；我不太清楚这是为什么。

无论如何，如果您有不可变的属性，那么下面的代码应该可以工作：

// If this class is immutable, consider marking it with:
// [Pure]
public class SemanticVersion
{
    private readonly int _majorVersion;
    private readonly int _minorVersion;
    private readonly int _patchVersion;
    private readonly Maybe<T> _buildVersion;
    private readonly Maybe<T> _prereleaseVersion;

    public SemanticVersion(string version)
    {
        Contract.Requires<ArgumentException>(!string.IsNullOrEmpty(version));

        var match = SemanticVersionRegex.Match(version);
        if (!match.Success)
        {
            var message = $"The version number '{version}' is not a valid semantic version number.";
            throw new ArgumentException(message, nameof(version));
        }

        _majorVersion = int.Parse(match.Groups["major"].Value, CultureInfo.InvariantCulture);
        _minorVersion = int.Parse(match.Groups["minor"].Value, CultureInfo.InvariantCulture);
        _patchVersion = int.Parse(match.Groups["patch"].Value, CultureInfo.InvariantCulture);
        _prereleaseVersion = match.Groups["prerelease"].Success
            ? new Maybe<string>(match.Groups["prerelease"].Value)
            : Maybe<string>.Empty;
        _buildVersion = match.Groups["build"].Success
            ? new Maybe<string>(match.Groups["build"].Value)
            : Maybe<string>.Empty;
    }

    [ContractInvariantMethod]
    private void ObjectInvariants()
    {
        Contract.Invariant(_majorVersion >= 0);
        Contract.Invariant(_minorVersion >= 0);
        Contract.Invariant(_patchVersion >= 0);
        Contract.Invariant(_prereleaseVersion != null);
        Contract.Invariant(_buildVersion != null);
    }

    // Properties that only contain getters are automatically
    // considered Pure by Code Contracts. But also, this point
    // is moot if you make the entire class Pure if it's
    // immutable.
    public int MajorVersion => _majorVersion;
    public int MinorVersion => _minorVersion;
    public int PatchVersion => _patchVersion;
    public Maybe<T> PrereleaseVersion => _prereleaseVersion;
    public Maybe<T> BuildVersion => _buildVersion;
}

如果您的类不是纯类并且属性是可变的，那么您需要创建引用私有支持字段的完整属性。但同样的ObjectInvariants方法应该足以为您的班级提供适当的合同。