コード契約：証明されていないソースが必要です！= null

Question

このタイプの質問に対する他の回答の一部を読んだ後、私はまだ警告が残っています。このスニペットで私は自分のデータベースからUserActivationを取得します。この時点までに、少なくとも1つのUserActivationが常に存在します。それ以上のものが1つあれば、すべての洋梨の形になっています...私は、証明されていないソースに関する警告をどのようにスケルチするのかについて、いくつかの指示に従っていますが、役に立たないものです。警告：警告83 CodeContracts：unproven：source！= null 161行目で、特定の行の下のメソッドを参照してください。

これは、ここで要求されたとして、私は、CCのバージョン1.4.40602.0を使用しています方法

private static UserActivation GetUserActivation(Guid userId) 
    { 
     UserActivations userActivations = UserActivation.GetUserActivationsByUser(userId: userId); 

     Contract.Assume(userActivations != null); 

     if (userActivations.Count() > 1) // Line Number 161 
      throw new Exception("More then one user action found in database"); 

     return userActivations[0]; 
    } 

がUserActivations宣言です。

Public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid()) 
    { 
     Guid id = new Guid(); 
     if (user != null) 
      id = user.Id; 
     else 
      if (userId != Guid.Empty) 
       id = userId; 
      else 
       throw new Exception("Either user or userId must have a value"); 

     UserActivations uas = new UserActivations(StorageManager.SelectAll(
      Criteria.And(
      Criteria.EqualTo("UserId", id), 
      Criteria.EqualTo("Deleted", false)))); 

     Contract.Ensures(Contract.Result<UserActivations>() != null); 

     return uas; 
    } 

Answer 1

私はおそらくLINQ Enumerable拡張メソッドを避け、別の方法を使用してみます。ここ

public class UserActivations : BusinessListBase<UserActivation> 
{ 
    #region Constructors 
    internal UserActivations() 
    { 
    } 

    internal UserActivations(IList<UserActivation> list) 
     : base(list) 
    { 
    } 

    internal UserActivations(IEnumerable<UserActivation> list) 
     : base(list) 
    { 
    } 

とは、元のコードだったGetUserActivationByUser方法

public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid()) 
    { 
     Contract.Requires(user != null || userId != null, "Either user or userId must have a value"); 
     Contract.Ensures(Contract.Result<UserActivations>() != null); 

     Guid id = new Guid(); 
     if (user != null) 
      id = user.Id; 
     else 
      id = userId; 

     return new UserActivations(StorageManager.SelectAll(
      Criteria.And(
      Criteria.EqualTo("UserId", id), 
      Criteria.EqualTo("Deleted", false)))); 
    } 

です。 UserActivationsクラスには、インスタンスが保持する要素の数を決定するための独自のメソッドまたはプロパティがありませんか？いずれにしても

（シーケンスがICollectionを実装していない場合）、それは全体のシーケンスを列挙しますので、あなたは、シーケンスが空であるかどうかをテストするためにCount()拡張メソッドを使用しないでください。または、オブジェクトがIQueryableを実装する場合、Pavel Gatilovが指摘したように、Countは予期せずデータベースクエリを実行することがあります。

ここでは大きな要素はありませんが、要素が1つあると予想されますが、シーケンスには何千もの要素が定期的に含まれる場合があります。代わりに、Any()拡張メソッドを使用する必要があります。

Any()を使用すると、おそらく契約アナライザの観点から変わることはないため、UserActivationsクラスのCountプロパティを使用する必要があります（たとえばICollectionを実装すると仮定します）。

おそらく、あなたが契約アナライザをこのように助けることができる：あなたがUserActivationsクラスをコントロールしている場合、

private static UserActivation GetUserActivation(Guid userId) 
{ 
    UserActivations userActivations = UserActivation.GetUserActivationsByUser(userId: userId); 

    IEnumerable<UserActivation> e = (IEnumerable<UserActivation>)userActivations; 

    Contract.Assume(e != null); 

    if (e.Count() > 1) // Line Number 161 
     throw new Exception("More then one user action found in database"); 

    return userActivations[0]; 
} 

より良いソリューションを、メソッドがnullを返すことはありませんと言うことはGetUserActivationsByUserにContract.Ensuresを追加することです。

Answer 2

ビルドログを確認してください。 Contract.Ensuresが正しく使用されていません。あなたは、このように、間違った使用のための警告を持っている必要があります。

警告CC1025を：CodeContracts：契約ブロックの後には、あなたの方法契約ブロックで定義されたローカル変数「のDataEvent」

の使用を見つけなければなりませんbe：

public static UserActivations GetUserActivationsByUser(User user = null, Guid userId = new Guid()) 
{ 
    Contract.Ensures(Contract.Result<UserActivations>() != null); 

    Guid id = new Guid(); 
    if (user != null) 
     id = user.Id; 
    else 
     if (userId != Guid.Empty) 
      id = userId; 
     else 
      throw new Exception("Either user or userId must have a value"); 

    UserActivations uas = new UserActivations(StorageManager.SelectAll(
     Criteria.And(
     Criteria.EqualTo("UserId", id), 
     Criteria.EqualTo("Deleted", false)))); 

    return uas; 
} 

私は証明できませんが、これが検証者を怒らせるかもしれないと思います。

実際、実行時のチェックをオンにすると、コードはコンパイルされず、ccrewriteは失敗します。