为什么我仍然获得代码合同:确保未经证实的警告？

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实现的限制.

请参阅官方代码合同论坛上的此链接.

这是因为string.Format的契约不能确保其结果非空,只是它非空.

编辑一些证明来支持这一点:当您在mscorlib.Contracts.dll上使用Reflector时,您可以看到在String.Format上定义的合同

[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语句只是非null,而不是非空.