这是我的类(class)之一的构造函数:
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静态检查器标记一个错误:
Maybe<T>是一个包含零个或一个元素的集合。据我所知，唯一可以为null的方法是在分配异常之前是否存在异常，这应该使确保需求不相关。我会成为代码盲人吗？你看到问题了吗...？
更新:张贴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();
}
}
}
最佳答案
看来Maybe<T>类上唯一的mutator方法是构造函数本身。其他所有方法都可以得到东西。因此，您可以将PureAttribute放在类级别，以向分析器暗示整个类是纯净的，因为它是不可变的–毕竟，这不是Maybe的意思，要么您得到了东西，要么得到了Empty Maybe。 ，但您永远不会得到null？而且，您无法在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;
}
如果您的类不是纯类，并且属性是可变的，那么您需要创建引用私有(private)支持字段的完整属性。但是，相同的
ObjectInvariants方法应该足以用适当的协定来对您的类进行检测。关于c# - 为什么代码契约(Contract)要求此代码为 "Ensures is false"？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/33631307/