指導PEX嘗試排序的數組輸入

我有以下測試方法，它接受一個字符串數組，對其進行復制，排序，然後聲明已排序的複製元素應與原始數據不同。指導PEX嘗試排序的數組輸入

這個測試應該在大多數情況下通過，但我認爲如果輸入數組恰好已經被排序，它應該會失敗。

我無法讓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)); 
    } 
}

微軟的Pex 0.94.51023.0 Pex的微軟的Visual Studio擴展

來源

2013-09-24 lexicalscope

的Array.Copy某些版本在當前CLR實現通過調用出來本機代碼優化。 Pex似乎受到這個事實的影響，因爲它無法追蹤通過Array.Copy例程的數據流。

經過這樣的修改，測試失敗多次：

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

這可能是一個Pex的缺陷，因爲它不具有可分析的版本代替Array.Copy喜歡它與許多其他的事情一樣。

來源

2013-09-24 13:01:03 usr

指導PEX嘗試排序的數組輸入

回答

相關問題