现在想确定P有没有正确地实现F 也就是要证明
For any x belongs to D, F(x) = P(x)
如果用数理逻辑的方法也就是形式化方法证明了上面的式子 这个就是program verification 不是testing
testing的问题是 能不能找出一个D的子集T 使得
{For any t belongs to T, F(t) = P(t)} implies {For any x belongs to D, F(x) = P(x)}
也就是说 只要程序P能够正确执行T里的每个元素 我们就能断定P正确地实现了函数F 因此T可以看作一个test cases的集合 我们称T为reliable test set
但是 在通常情况下 T=D 找不到一个能作为D的真子集的T 也就是说 我们无法找到一个比D小的reliable test set 如果要确保一个程序的正确 就必须把每个可能的输入值都作为test case来运行一遍 这个叫exhaustive testing 通常情况下是不可能完成的