CODEWITHSUNDEEP
haskellquickcheck
Arek' Fu
Arek' Fu

Reputation: 857

How do I use QuickCheck to test if a function terminates?

I would like to use QuickCheck to test a function to make sure it terminates (no infinite recursion, no exceptions thrown, etc.). This is what I do at the moment:

f :: Int -> Int -> Int

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

Is there a better (more expressive and idiomatic) way?

Upvotes: 2

Views: 734

Answers (2)

Chris Taylor
Chris Taylor

Reputation: 47402

This is the halting problem. There is no algorithm capable of telling you whether a function terminates or not.

In particular, you may be able to get a positive result (i.e. if the function does terminate, this proposition will tell you) if you are willing to wait long enough. But just by waiting, you can never know the difference between this function does not terminate and this function has not terminated yet.

You can implement a check like does this function terminate in time T which may be appropriate for your needs.

Edit As written, your function does not do what you require. Consider

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

The reason is that seq only evaluates to weak head normal form. Instead you could use deepseq which evaluates data structures deeply,

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

Upvotes: 7

Ben
Ben

Reputation: 71535

I probably wouldn't bother, I'd just test other properties of its output.

Any property that examines the output of f x y in any way is going to do at least as much termination checking as your prop_fTerminates, so why waste time doubling up on that check?

If for some reason "f x y terminates" is the only property you can test about f, then what you've got seems reasonable.

Upvotes: 4

Related Questions