1

我有以下测试方法，它接受一个字符串数组，复制它，对其进行排序，然后断言排序后的复制元素应该与原始元素不同。

在大多数情况下，这个测试应该通过，但我认为如果输入数组恰好已经排序，它应该会失败。

我无法让 PEX 发现这种情况（除了将其作为种子输入提供）。我可以在 PEX 中配置什么，或者更改测试的编写方式，以使 PEX 更有可能发现这个问题吗？发现这样的输入是否超出了 PEX/Z3 的能力？

[TestClass]
public class SortingPexTest
{
    [PexMethod(TestEmissionFilter = PexTestEmissionFilter.All, MaxConstraintSolverTime = 4)]
    [PexAllowedContractRequiresFailure]
    public void TM([PexAssumeNotNull] String[] L0)
    {
        PexAssume.AreElementsNotNull(L0);
        PexAssume.AreDistinctValues(L0);

        String[] L1 = new String[L0.Length];
        L0.CopyTo(L1, 0);
        Array.Sort(L1);

        PexAssert.IsTrue(!L0.SequenceEqual(L1));
    }
}

Microsoft Pex 0.94.51023.0 Microsoft Pex Visual Studio 扩展

4

1 回答 1

1

某些版本Array.Copy在当前 CLR 实现中通过调用本机代码进行了优化。Pex 似乎受到这一事实的打击，因为它无法通过Array.Copy例程跟踪数据流。

通过此修改，测试会多次失败：

String[] L1 = L0.OrderBy(x => x).ToArray();

这可能是 Pex 中的一个缺陷，因为它不像Array.Copy其他许多东西那样用可分析的版本代替。

于 2013-09-24T13:01:03.593 回答