C# - 代码契约 - 检测表达式语句,评估潜在的副作用

Question

我刚开始在C#中使用CodeContracts,我可能需要一些帮助.我有一个带有静态键列表的类,我有一个名为Remove()的静态方法,它从该列表中删除一个键.

现在我从合同发布条件中理解的是,作为类的程序员,我保证当前的公共方法做了特定的事情,在这种情况下:删除列表的元素.

这是我写的:

    private static List<Keys> m_usedKeys; // private list of keys

    public static void Remove(Keys _key)
    {
        m_usedKeys.Remove(_key);
        Contract.Ensures(!m_usedKeys.Any(x => x == _key));
    }

我在这里尝试"确保"的是,Remove()方法从列表中删除了真实的密钥(是的,这可能是一个简单的例子,但我在那里得到了错误.)

当我写Contract.Ensures()行时,VS2010给出了以下错误:

Error   3   Detected expression statement evaluated for potential side-effect in contracts of method 'LibJungleTimer.KeyBind.Remove(System.Windows.Forms.Keys)'. (Did you mean to put the expression into a Requires, Ensures, or Invariant call?)  C:\Users\Joel\Documents\Programmation\JT\JungleTimer\LibJungleTimer\KeyBind.cs  51

我认为这个错误表明该表达m_usedKeys.remove(_key);具有潜在的副作用.事实上,它有一个副作用,它从列表中删除一个键!

如果我尝试写这样的东西:

Contract.Assert(!m_usedKeys.Any(x => x == _key));

好吧编译好.我的问题是我做错了什么？不应该使用CodeContracts来确保发布条件吗？

编辑:是的,我的意思是真的!m_usedKeys.Any(...);

Answer 1

代码合同工具假定最后一个Contract.Ensures/ 之前的任何内容Contract.Requires都是合同的一部分...因此它认为您的调用Remove是合同的一部分,而不是实施的一部分.您必须反转代码,以便所有合同代码都在实现之前.

public static void Remove(Keys _key)
{
    Contract.Ensures(m_usedKeys.Any(x => x == _key));        
    m_usedKeys.Remove(_key);
}

我怀疑你想要!m_usedKeys.Any(...)顺便...而且我也会开始对这段代码保持警惕,因为你没有安装线程保护.如果这是一个实例方法,它不会打扰我,但访问静态(即全局)状态的静态方法通常应该是线程安全的.