不一致的警告 [英] Inconsistent invariant warning

问题描述

我在合同不变量上收到了一个不一致的警告。在下面的类中，通过对构造函数中注释掉的Test的方法调用，我得到了验证器的警告！= null如预期的那样。  但是，当我取消对
测试的注释时，警告消失。

I'm getting an inconsistent warning on a contract invariant. In the class below, with the method call to Test commented out in the constructor I get a warning for validators != null as expected.  However, when I uncomment the call to Test the warning disappears.

    class Class1
    {
        private Dictionary<string, int[]> Validators { get { return validators; } }
        private readonly Dictionary<string, int[]> validators;

        [ContractInvariantMethod]
        private void Invariants()
        {
            Contract.Invariant(validators != null);
        }

        public Class1()
        {
            //Test();
        }

        [Pure]
        public void Test()
        {

        }
    }

欢迎任何建议。

Alan

推荐答案

它与我们假设/断言不变量的方式有关。

It has to do with the way we assume/assert the invariants.

对于构造函数，我们在出口点断言不变量。 如果构造函数为空，那么当然我们无法证明不变量，并且你得到了警告。

For the constructor, we assert the invariant at the exit point.  If the constructor is empty, then of course we cannot prove the invariant, and you get the warning.

对于实例方法，我们假设条目处的不变量，并且我们在出口。因此，你没有得到Test（）的警告。

For the instance methods, we assume the invariant at the entry, and we assert at the exit. Therefore you get no warning for Test().

现在，在调用站点，我们没有断言实例方法的不变量（主要是为了减少警告/注释的数量），但我们假设它在返回时保持不变。

Now, at call site, we do not assert the invariant for instance methods (mainly to reduce the amount of warnings/annotations), but we assume that it holds on return.

因此，当您取消注释Test（）时，假设"validators！= null"在通话结束后出现，检查员用来证明不变量。

Therefore, when you uncomment Test(), an assume "validators != null" appears after the call, that the checker uses to prove the invariant.

ciao

f

这篇关于不一致的警告的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！