2010-11-18 11 views
5

नीचे एक बहुत ही सरल उदाहरण है। जब मैं स्थिर विश्लेषण चेतावनी चालू करते हैं, मैं अभी भी चेतावनी CodeContracts मिलती है: अप्रमाणित सुनिश्चित करता है: Contract.Result() = string.Emptyमुझे अभी भी कोड अनुबंध क्यों मिलते हैं: अनुमोदित चेतावनी सुनिश्चित करें?

लाइन पर

वापसी String.Format (" {0}, {1} ", मूवी। टिटल, मूवी। डिस्क्रिप्शन);

कृपया मेरे नीचे कोड

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

कोई भी विचार देखते हैं?

+0

इसमें कौन सी भाषा है? –

+0

यह सी # में है :) क्या कोई मुझे बता सकता है कि मुझे चेतावनी क्यों मिल रही है? – Simon

उत्तर

8

यह mscorlib dll में अनुबंधों के कार्यान्वयन की एक सीमा है।

आधिकारिक कोड अनुबंध मंच पर this link देखें।

इसका कारण यह है String.Format के लिए अनुबंध सुनिश्चित नहीं करता है कि अपनी परिणाम गैर खाली है, केवल कि यह में गैर-शून्य है।

संपादित कुछ सबूत इस बैकअप लेने के लिए: आप mscorlib.Contracts.dll पर परावर्तक का उपयोग करते हैं, तो आप अनुबंध है जो आप के रूप में 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; 
} 

पर परिभाषित कर रहे हैं देख सकते हैं देख सकते हैं, अनुबंध। परिणाम कथन केवल गैर-शून्य है, न कि खाली।

1

कोड अनुबंध इस रिपोर्ट को सही तरीके से रिपोर्ट कर रहे हैं। यह साबित नहीं कर सकता कि लौटाई गई स्ट्रिंग खाली नहीं होगी।

वास्तविक समस्या कोड अनुबंधों के स्थिर विश्लेषक के साथ नहीं है। ऐसा इसलिए है क्योंकि आपने यह सुनिश्चित करने के लिए पर्याप्त अनुबंध प्रदान नहीं किए हैं कि यह विधि खाली स्ट्रिंग नहीं लौटाएगी।

हालांकि, आप इस विधि को ठीक कर सकते हैं जैसे कि आप स्वयं को साबित कर सकते हैं कि यह विधि एक खाली स्ट्रिंग वापस नहीं करेगी, और साथ ही, स्थिर विश्लेषक की सहायता करें।

नोट
नीचे कोड में टिप्पणी की एक बहुत कुछ कर रहे हैं - तो यह भी लंबे समय तक यह पहले से ही है की तुलना में लग रहा है। लेकिन, उम्मीद है कि आप कोड अनुबंध क्या कर सकते हैं और नहीं कर सकते हैं की बेहतर समझ के साथ आ जाएगा।

इसके अलावा, @koenmetsu String.Format(string, params object args) के संबंध में कोड अनुबंध के बारे में भी सही है। हालांकि, इसके बावजूद, मैंने ओपी के कोड में कुछ मुद्दों को देखा जिसके लिए मुझे लगा कि उन्होंने इस जवाब की जरुरत है। यह नीचे दिए गए कोड में टिप्पणियों के भीतर स्पष्ट है।

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

एक बार मैं कोड संविदा स्थिर विश्लेषक के माध्यम से कोड के ऊपर दिखाया गया, मुझे कोई चेतावनी थी।

संबंधित मुद्दे