如何使用QuickCheck测试函数是否终止？

Question

我想使用QuickCheck来测试一个函数,以确保它终止(没有无限递归,没有抛出异常等).这就是我现在所做的:

f :: Int -> Int -> Int

prop_fTerminates :: Int -> Int -> Bool   -- say
prop_fTerminates x y = f x y `seq` True

是否有更好的(更具表现力和惯用语)的方式？

Answer 1

这是暂停的问题.没有能够告诉您函数是否终止的算法.

特别是,如果你愿意等待足够长的时间,你可能会得到一个积极的结果(即如果函数确实终止,这个命题会告诉你).但只是等待,你永远不会知道这个函数没有终止的区别,这个功能还没有终止.

您可以执行检查,例如此功能在时间T中终止,这可能适合您的需要.

编辑如上所述,您的功能无法满足您的要求.考虑

> let f = 1:f
> f `seq` True
True

原因是seq只评估弱头正常形式.相反,你可以使用deepseq它深入评估数据结构,

> import Control.DeepSeq (deepseq)
> f `deepseq` True
* never returns *