为什么代码合同声称“；确保为假”；用于此代码

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;
}

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();
        }
    }
}

似乎Maybe<T>类上唯一的赋值函数方法是构造函数本身。其他所有方法都会有收获。因此，您可以将PureAttribute放在类级别，以向分析器提示整个类是纯的，因为它是不可变的—毕竟，这不是"也许"的意义吗，要么你得到了一些东西，要么你获得了一个空的"也许"，但你永远不会变成空的？你不能改变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方法应该足以用适当的约定为类提供工具。

如果match.Success为false，则可能是null。

试试这个。。。

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)
    {
        // set the values here
        PrereleaseVersion = Maybe<string>.Empty;
        BuildVersion =  Maybe<string>.Empty;
        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;
}

基于评论，这里是一个状态在异常期间发生突变的例子。

class Program
{
    static void Main(string[] args)
    {
        var obj = new MyObject() { Prop1 = "Hello", };
        Console.WriteLine(obj.Prop1);
        try
        {
            obj.DoWork();
        }
        catch (Exception)
        {
        }
        Console.WriteLine(obj.Prop1);
        /*
        Hello
        World!
        */
    }
}
public class MyObject
{
    public string Prop1 { get; set; }
    public void DoWork()
    {
        this.Prop1 = "World!";
        throw new Exception();
    }
}