c# - 为什么我仍然得到代码契约(Contract) : Ensure unproven warning?

Question

下面是一个非常简单的例子。当我打开静态分析警告时，我仍然得到警告 CodeContracts:确保未经证实:Contract.Result() != string.Empty

在线

return string.Format("{0}, {1}", movie.Title, movie.Description);

请看我下面的代码

namespace CodeContractsSamples
{
    public class MovieRepo
    {
        public string GetMovieInfo(Movie movie)
        {
             Contract.Requires(movie != null);
             Contract.Ensures(Contract.Result<string>() != string.Empty);

             return string.Format("{0}, {1}", movie.Title, movie.Description);
         }
     }

      public class Movie
      {
         public string Title { get; set; }
         public string Description { get; set; }
      }
}

有什么想法吗？

Answer 1

这是 mscorlib dll 中 Contracts 实现的限制。

参见 this link在官方代码契约(Contract)论坛上。

This is because the contract for string.Format doesn't ensure that its result is non-empty, only that it is non-null.

编辑 支持这一点的一些证据:当您在 mscorlib.Contracts.dll 上使用 Reflector 时，您可以看到在 String.Format 上定义的契约(Contract)

[Pure, Reads(ReadsAttribute.Reads.Nothing)]
public static string Format(string format, object[] args)
{
    string str;
    Contract.Requires((bool) (format != null), null, "format != null");
    Contract.Requires((bool) (args != null), null, "args != null");
    Contract.Ensures((bool) (Contract.Result<string>() != null), null, "Contract.Result<String>() != null");
    return str;
}

如您所见，Contract.Result 语句只是非空的，而不是非空的。