Code Contracts如何知道ToString重寫不應該返回null？

我正在使用C＃的微軟代碼合同擴展。當我寫一個類與返回null一個重寫的ToString實現，它正確地識別問題：Code Contracts如何知道ToString重寫不應該返回null？

我認爲，這是因爲微軟使用代碼契約內部，和他們增加了Contract.Ensures調用Object.ToString。但是，當我看到Object.ToString source code時，我沒有看到任何合同（我看到其他合同，但沒有看到我正在尋找的合同）。 Code Contracts如何確定ToString不應該返回null？

來源

2015-10-27 Will

這是代碼合同內部定義System.Object：(link)。正如你所看到的，他們已經確定ToString()這一限制：

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

要回答你的問題，代碼契約知道這是因爲內部合同的定義不爲空。

來源

2015-10-27 04:18:57 Amy

提供更多信息：代碼合同不在官方程序集中，因此您不會在referencesource.microsoft.com上看到它們。代碼合同團隊自己定義了所有代碼合同，並將其提供給單獨的合同參考程序集，該程序集僅包含合同而非實際來源。 – cremor

@cremor謝謝！只是FYI，我看到很多關於ReferenceSource的合同（例如[Object.cs]（http://referencesource.microsoft.com/#mscorlib/system/object.cs,180）），但我想合約可以在.NET核心或代碼合同中指定，具體取決於誰寫的。 – Will

Code Contracts如何知道ToString重寫不應該返回null？

回答

相關問題