c# - Code Contracts 如何知道 ToString 重写不应返回 null？

Question

我在 C# 中使用 Microsoft 的 Code Contracts 扩展。当我编写一个带有返回 null 的重写 ToString 实现的类时，它正确地识别了问题:

我假设这是因为 Microsoft 在内部使用代码契约，并且他们添加了一个 Contract.Ensures 调用到 Object.ToString。但是，当我查看 Object.ToString source code我没有看到任何契约(Contract)(我确实看到了其他契约(Contract)，但不是我要找的契约(Contract))。代码契约如何确定 ToString 不应返回 null？

Answer 1

这是 System.Object 的代码契约内部定义:(link) .如您所见，他们定义了具有以下约束的 ToString():

Contract.Ensures(Contract.Result<string>() != null);

为了回答您的问题，Code Contracts 知道它不是 null，因为内部契约(Contract)定义。