Why I still get Code Contracts : Ensure unproven warning?

Question

Below is a very simple example. When I turn on the static analysis warnings, I still get Warning CodeContracts: ensures unproven: Contract.Result() != string.Empty

on the line

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

Please see my below code

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; }
      }
}

Any ideas?

Answer 1

This is a limitation of the implementation of Contracts in the mscorlib dll.

See this link on the official Code Contracts forum.

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

Edit Some proof to back this up: When you use Reflector on the mscorlib.Contracts.dll, you can see the contracts which are defined on 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;
}

As you can see, the Contract.Result statement is only non-null, not non-empty.

Answer 2

Code Contracts is reporting this correctly. It cannot prove that the returned string will not be empty.

The real issue is not with Code Contracts' static analyzer. It is because you have not provided enough contracts to ensure that this method will not return an empty string.

You can, however, fix this method such that you can prove to yourself that this method will not return an empty string, and at the same time, help the static analyzer out.

NOTE
There are a lot of comments in the code below--so it looks even longer than it already is. But, hopefully you'll come away with a better understanding of what Code Contracts can and can't do.

Also, @koenmetsu is also correct about Code Contract with respect to String.Format(string, params object args). However, despite that, I saw some issues in the OP's code for which I felt they warranted this answer. This is elucidated upon within the comments in the code below.

namespace CodeContractsSamples
{
    public class MovieRepo
    {
        [Pure]
        public string GetMovieInfo(Movie movie)
        {
            Contract.Requires(movie != null && 
                              !(string.IsNullOrEmpty(movie.Title) || 
                                string.IsNullOrEmpty(movie.Description)));
            // This ensures was always invalid. Due to your format
            // string, this string was guaranteed to never be empty--
            // it would always contain at least ", ".
            //Contract.Ensures(Contract.Result<string>() != string.Empty);
            Contract.Ensures(!string.IsNullOrEmpty(Contract.Result<string>()));

            // Changed this line to use C# 6 -- see the below
            //return string.Format("{0}, {1}", movie.Title, movie.Description);

            // Help out the static analyzer--and yourself! First, we prove that
            // Title and Description are greater than 0.
            // These asserts aren't strictly needed, as this should
            // follow from the pre-conditions above. But, I put this
            // here just so you could follow the inference chain.
            Contract.Assert(movie.Title.Length > 0);
            Contract.Assert(movie.Description.Length > 0);

            // Introduce an intermediate variable to help the static analyzer
            var movieInfo = $"{movie.Title}, {movie.Description}";

            // The static analyzer doesn't understand String.Format(...) 
            // (or string interpolation). However, above, we asserted that the movie 
            // Title's and Description's length are both greater than zero. Since we
            // have proved that, then we can also prove that movieInfo's length is
            // at least Title.Length + Description.Length + 2 (for the ", ");
            // therefore, we know it's not null or empty.
            // Again, the static analyzer will never be able to figure this out on
            // it's own, so we tell it to assume that that's true. But, again, you
            // have proven to yourself that this is indeed true; so we can safely tell
            // the analyzer to assume this.
            // If this seems like a lot of bloat--this is the cost of provable
            // code--but you can rest assured that this method will always work the
            // way you intended if the stated pre-conditions hold true upon method
            // entry.
            Contract.Assume(!string.IsNullOrEmpty(movieInfo));
            return movieInfo;
        }
    }

    // Since this class contained only data, and no behavior,
    // I've changed this class to be an immutable value object.
    // Also, since the class is immutable, it's also pure (i.e.
    // no side-effects, so I've marked it as [Pure].
    [Pure]
    public class Movie : IEquatable<Movie>
    {
        private readonly string _title;
        private readonly string _description;

        [ContractInvariantMethod]
        [System.Diagnostics.CodeAnalysis.SuppressMessage(
            "Microsoft.Performance", 
            "CA1822:MarkMembersAsStatic", 
            Justification = "Required for code contracts.")]
        private void ObjectInvariant()
        {
            Contract.Invariant(!(string.IsNullOrWhiteSpace(_title) 
                && string.IsNullOrWhiteSpace(_description)));
        }

        public Movie(string title, string description)
        {
            // NOTE: For Code Contracts 1.9.10714.2, you will need to
            //       modify the Microsoft.CodeContract.targets file located
            //       at C:\Program Files (x86)\Microsoft\Contracts\MSBuild\v14.0
            //       (for VS 2015) in order for Code Contracts to be happy
            //       with the call to System.String.IsNullOrWhiteSpace(string)
            //       See this GitHub issue: 
            //           https://github.com/Microsoft/CodeContracts/pull/359/files
            Contract.Requires(!(string.IsNullOrWhiteSpace(title) &&
                                string.IsNullOrWhiteSpace(description)));
            Contract.Ensures(_title == title && 
                             _description == description);

            _title = title;
            _description = description;
        }

        public string Title => _title;
        public string Description => _description;

        // Since this class is now an immutable value object, it's not
        // a bad idea to override Equals and GetHashCode() and implement
        // IEquatable<T>
        public override bool Equals(object obj)
        {
            if (obj == null || !this.GetType().Equals(obj.GetType()))
            {
                return false;
            }

            Movie that = obj as Movie;
            return this.Equals(that);
        }

        public override int GetHashCode()
        {
            // Because we know _title and _description will
            // never be null due to class invariants, tell
            // Code Contracts to assume this fact.
            Contract.Assume(_title != null && _description != null);
            return _title.GetHashCode() ^ _description.GetHashCode();
        }

        public bool Equals(Movie other)
        {
            if (other == null)
            {
                return false;
            }

            return this._title == other._title &&
                   this._description == other._description;
        }

        public static bool operator == (Movie movie1, Movie movie2)
        {
            if (((object)movie1) == null || ((object)movie2) == null)
            {
                return object.Equals(movie1, movie2);
            }

            return movie1.Equals(movie2);
        }

        public static bool operator != (Movie movie1, Movie movie2)
        {
            if (((object)movie1) == null || ((object)movie2) == null)
            {
                return !object.Equals(movie1, movie2);
            }

            return !movie1.Equals(movie2);
        }
    }
}

Once I ran the code above through the Code Contracts static analyzer, I had no warnings.