Why does Code Contracts claim that "Ensures is false" for this code?

Question

This is a constructor in one of my classes:

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

The Code Contracts static checker flags an error:

warning : CodeContracts: ensures is false: PrereleaseVersion != null

Maybe<T> is a collection containing zero or one elements.

As far as I can see, the only way that can be null is if there's an exception before it is assigned, which should make the Ensures requirements irrelevant. Am I going code blind? Can you see the problem...?

Update: Posting implementation of Maybe in response to comments.

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

It appears that the only mutator methods on the Maybe<T> class are the constructors themselves. Every other method just gets stuff. Therefore, you could put the PureAttribute at the class level to hint to the analyzer that the entire class is pure, as it's immutable—afterall, isn't that the point of a Maybe, either you get something, or you get an Empty Maybe, but you never get null? And you can't change the value in a Maybe, you can only create a new Maybe containing a new value.

Also, I've always had problems with the static analyzer and using Contract.Ensures with properties in constructors (particularly, mutable properties), even with object invariants specified; I'm not quite sure why this is.

Anyway, if you have immutable properties, then the code below should work:

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

If your class is not pure and the properties are mutable, then you'll need to create full properties referencing the private backing fields. But the same ObjectInvariants method should be enough to instrument your class with the proper contracts.

Answer 2

It could be null if match.Success is false.

Try this...

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

... Based on a comment here is an example of state being mutated durning an exception.

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