健全性和完整性

Question

我正在参加软件分析课程，并被问到以下问题。它与编程逻辑有关，因此我在这里发布它的原因。 （我也将其发布到数学堆栈溢出站点。）：

假设阴影部分表示所有程序不包含被零除错误，黑色矩形内的未阴影部分表示所有程序都包含此类错误。

假设 A1、A2 和 A3 是检查被零除错误的不同程序分析。每个分析要么接受（即声明它没有被零除错误）或拒绝（即声明至少存在一个被零除错误）给定程序。

对于每个分析，该分析接受的程序包含在相应的椭圆形内，而该分析拒绝的程序包含在相应的椭圆形外。

参考问题4，假设我们设计了一个分析A4，它在输入程序P上表现如下：

if (A1 rejects P) reject P;
else if (A3 accepts P) accept P; 
else run forever; 

A4 声音好吗？ A4完整吗？

我选择 A4 是合理的，因为 A1 接受有效的程序并拒绝无效的程序。这被标记为正确。我说它不完整，因为 A4 不接受确实是有效程序并被标记为错误的程序。想知道是否有人可以为我阐明这一点？提前致谢。

Answer 1

我认为它会是完整的。假设您有一个给出 DBZ 错误的程序，我们想对此进行测试。将该程序发送到 A1。 A1 包含有和没有 DBZ 的两个程序的空间。所以它可以被 A1 接受，也可以被 A1 拒绝。如果它被 A1 拒绝，那么我们可以将程序拒绝为有 DBZ 错误。如果 A1 没有拒绝，则转到 A3，它只接受没有 DBZ 错误的程序。请记住，这是针对未被 A1 拒绝的程序。如果程序被 A3 接受，那么我们就知道它没有 DBZ 错误。如果它在这里也被拒绝，我们知道它包含一个 DBZ 错误。

基本上单独使用A1并不能完全确定该程序是否会被接受。但是由于 A3 只包含可以接受的程序空间，如果它在 A1 和 A3 中被接受，我们可以推断它是一个有效的程序。

从这个解释看来，如果一个程序是有效的，即使 A1 没有捕捉到该程序是无效的，它也会被 A3 接受，因为 A3 只会接受有效的程序，这与你所说的相反为什么A4不能完整。

如果我应该澄清这个答案中的一些观点，请告诉我。