haskell - 使用 Haskell 的 Quickcheck 进行传递性的最佳测试

Question

在下面的三个测试中，哪个是传递性的最佳测试。这来 self 的 previous question .通常的传递性逻辑规则 (R(a,b) and R(b,c)) => R(a,c) 似乎不适用于这种情况。因此，我认为 prop_trans3这不是一个好的测试，因为这三个术语中的每一个都代表不同的堆栈。但是 prop_trans1 和 prop_trans2 中的哪一个最适合测试传递性？

import Test.QuickCheck
data Block = Block Int deriving (Show,Eq)
-- MoveOnto(bl,b2,s) is read as b2 is moved into and onto bl on stack or table.
data Stack = EmptyTable  |  MoveOnto Block Block Stack deriving  (Show,Eq) 
isOn :: Block -> Block -> Stack -> Bool
isOn b1 b2 (MoveOnto b3 b4 s) |  ((b1 == b3) && (b4 == b2)) || (isOn b4 b2 s)   =  True
isOn _ _ _  = False

instance Arbitrary (Block) where
  arbitrary = fmap Block arbitrary

instance Arbitrary (Stack) where
  arbitrary = oneof [return EmptyTable, MoveOnto <$> arbitrary <*> arbitrary <*> arbitrary]

prop_trans1 b1 b2 s      =  isOn b1 b2 (MoveOnto b1 b2 s)
prop_trans2 b1 b2 b3 s   =  isOn b3 b1 (MoveOnto b3 b2 (MoveOnto b2 b1 s))
prop_trans3 b1 b2 b3 s   =  ((isOn b2 b1 (MoveOnto b2 b1 s)) && (isOn b3 b2 (MoveOnto b3 b2 s))) <=  (isOn b3 b1 (MoveOnto b3 b1 s))

Answer 1

我认为传递性的通常定义确实适用，即使在这种情况下也是如此。

prop_trans a b c s = (r a b && r b c) ==> r a c
    where r x y = isOn x y s

不幸的是，检查这个属性会导致很多丢弃。只需从出现在 s 中的 block 中绘制 a、b 和 c 就可以做得更好:

listBlocks (MoveOnto b1 b2 s) = b1:b2:listBlocks s
listBlocks EmptyTable = []

prop_trans2 s = do
    [a,b,c] <- replicateM 3 . elements . listBlocks $ s
    return (prop_trans a b c s)

还有可能做得更好，但似乎没有必要，因为这很快就给了我一个反例:

> quickCheckWith stdArgs { maxDiscardRatio = 1000 } prop_trans2
*** Failed! Falsifiable (after 6 tests):  
MoveOnto (Block 4) (Block (-2)) (MoveOnto (Block (-2)) (Block 4) (MoveOnto (Block 2) (Block 5) EmptyTable))