为什么代码合同声明此代码的“确保为假”？
这是我的一个类中的构造函数：
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;
}
代码合同静态检查器标记一个错误：
警告：CodeContracts：确保为false：PrereleaseVersion！= null
Maybe<T>是一个包含零个或一个元素的集合。
据我所知，可以为空的唯一方法是在分配之前有一个异常，这应该使得确保需求不相关。 我会盲目密码吗？ 你能看到问题......？
更新 ：发布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>类中唯一的增变器方法本身就是构造函数。 其他任何方法只是获取东西。 因此，您可以将PureAttribute放在类级别，以向分析器提示整个类是纯粹的，因为它是不可变的 - 毕竟，不是一个Maybe的重点，要么你得到了某个东西，要么得到一个Empty 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方法应该足以用合适的合约来处理你的类。
如果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();
}
}
上一篇: Why does Code Contracts claim that "Ensures is false" for this code?