Why do Code Contracts claim to “Provide False” for this code?

Question

This is the 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; } 

Static controller Code Contracts indicates an error:

warning: CodeContracts: provides false: PrereleaseVersion! = null

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

As far as I can see, the only way that can be null is an exception before its appointment, which should make the requirements of the “Collateral” irrelevant. Am I going blind code? Do you see the problem ...?

Update . Posting a Maybe implementation 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 seems that the only mutator methods of the Maybe<T> class are the constructors themselves. Every other method just gets the stuff. That way, you can put PureAttribute at the class level to hint at the analyzer that the whole class is clean because it is immutable and after that is not that Maybe, either you get something or you get Empty Maybe, but you never don't get zero And you cannot change the value in “Maybe,” you can only create a new one, possibly containing a new value.

In addition, I always had problems with the static analyzer and the use of Contract.Ensures with properties in the constructors (in particular, mutable properties), even with the specified invariants of objects; I do not quite understand why this is so.

In any case, if you have immutable properties, then the code 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 clean and the properties are mutable, then you will need to create complete properties that reference private support fields. But the same ObjectInvariants method should be sufficient to ensure that your class tool has the proper contracts.

Answer 2

It can be null if match.Success is false.

Try it...

 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 the comment, here is an example of mutating a state that causes 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(); } }