Yusaku Hashimoto wrote:
So what I want to know is "how to find good properties." Please let me know how do you find QuickCheck properties. There are so many tutorials or papers for using QuickCheck, but when I try to apply them to my programming, I often miss properties in my codes.
Dijkstra would have said a good program (or program fragment, such as a library or even a single function) should /start out/ with properties, ideally a set of properties which completely specifies the program's output/behaviour. The implementation should then be structured in a way that makes it possible to prove (with reasonable effort) that the properties hold (and runnign QC on these properties then merely tests whether your proof was erroneous). Thus your problem is solved by construction. However, in practice we most often start out with only a vague idea of what our program should do. After hacking away for a time, however, we usually arrive at a level of granularity (individual small functions) where we have a more or less precise idea what we want it to achieve. It is then a matter of making this specification as precise as possible. If it turns out that a precise spec is unwieldy (too complex) then this is a hint that maybe it is not a good abstraction. Try to generalize or otherwise simplify the spec (refactoring the program) until you arrive at something manageable. It should then be possible to formalize this specification and convert it into a QC property. I think that this process is not something that can be automated (in general). Cheers Ben