c# - c#中的代码合同问题

Question

我面临一个我无法弄清楚的问题。

假设我有两种方法：public void Method1(object obj)在ViewModel课堂上和public void Method2(object obj)课堂Model上。

Method2从Method1使用Model类的实例调用（例如，objM 是类的对象和Model类的成员ViewModel）。

class ViewModel
{
public void Methods1(object obj)
{
     if (!(
                        (      (false == this.HasSal)
                            && (typeof(Class1) == obj.GetType())
                          )
                    ||
                        (      (true == this.HasSal)
                            && (typeof(Class2) == obj.GetType())
                        )
                   ) 
                )
            {
                throw new ArgumentException("invalid obj");
            }
            Contract.EndContractBlock();
            objM.Method2(obj);
            .....
} 
}

class Model
{
public void Method2(object obj)
{
 Contract.Requires(
                    (      (false == this.HasSal)
                        && (typeof(Class1) == obj.GetType())
                    )
                ||
                    (      (true == this.HasSal)
                        && (typeof(Class2) == obj.GetType())
                    )

            );
    .....
    }
}

现在，每当我尝试构建代码时，Visual Studio 都会产生以下警告

Code contracts: Requires unproven
(
                    (      (false == this.HasSal)
                        && (typeof(Class1) == obj.GetType())
                    )
                ||
                    (      (true == this.HasSal)
                        && (typeof(Class2) == obj.GetType())
                    )

            )

请建议。

Answer 1

由于rtrokzzz已经在评论中给出了另一个 SO 问题.NET 4 Code Contracts 的链接：“需要未经证实：源！= null”</a>

Contract.Ensures您的解决方案是添加Method1()和Method2()

请注意：我没有使用过Code Contracts，但我相信根据我的理解，代码将是

Contract.Ensures(obj != null);

更新

Contract.Requires(obj != null);

参考：使用 Code Contracts 和 Linq To Sql 时如何避免“source !=null”？

Answer 2

我不相信静态检查器将能够验证您的合同，因为obj直到运行时才知道类型 - 不能保证只有类型的对象 Class1或Class2将被传递给Method1.

可以通过向调用Method1. 如果您包含该代码，我可能会提出一种满足静态检查器的方法。

编辑：实际上，还有另一个问题。如果HasSal是 public-setter 属性，那么我不确定您的合同是否可以验证 - 另一个线程总是有可能在被调用和正在执行的方法主体HasSal之间更改值。Method1