코드 계약에서 올바르게보고하고 있습니다. 반환 된 문자열이 비어 있지 않음을 증명할 수는 없습니다.
코드 계약의 정적 분석기에는 실제 문제가 없습니다. 이 메서드가 빈 문자열을 반환하지 않도록 계약을 충분히 제공하지 않았기 때문입니다.
그러나이 방법으로 빈 문자열을 반환하지 않으면 서 정적 분석기를 쉽게 사용할 수 있음을 스스로 입증 할 수 있습니다.
참고
아래의 코드에 주석이 많이있다 - 그래서 더 오래 이미보다 보인다. 그러나 코드 계약이 할 수있는 것과 수행 할 수없는 것에 대해 더 잘 이해하게 될 것입니다.
또한 @koenmetsu는 String.Format(string, params object args)에 관한 코드 계약에 대해서도 정확합니다. 그러나 그에도 불구하고 나는 OP의 코드에서이 대답을 보증한다고 느낀 몇 가지 문제점을 보았다. 아래 코드의 주석에 설명되어 있습니다. 내가 코드 계약 정적 분석을 통해 위의 코드 실행되면
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);
}
}
}
, 나는 아무런 경고도 없었다.
어떤 언어입니까? –
그것은 C#에 있습니다 : 아무도 내가 왜 제발 경고를 받고 있어요 말해 줄래? – Simon