不完整的测试与详尽的分析是苹果与橘子的比较吗？
Is incomplete testing versus exhaustive analysis an apples-to-oranges comparison?
我经常听到这样的争论：传统测试的一个缺点是它不完整，而 Alloy 分析是详尽和完整的（在一定范围内）。但是，第一个是谈论软件，第二个是谈论模型。这不是苹果和橘子的比较吗？
更新：我错了。比较的不是这个：testing code versus analyzing models。这是一个苹果与橘子的比较。相反，比较是这些：
Testing models versus analysis of models.
Testing code versus analysis of code.
这些是同类比较。
因此，无论工件是模型还是代码，您都可以比较两种分析：测试，对应于随机抽取相对较少的案例，没有大小限制，与小范围分析相对应，这涉及小范围内的所有情况。
感谢丹尼尔·杰克逊消除我的误解。
首先，当 Alloy 被发明时，唯一现有的用于分析数据丰富语言模型的工具（例如 Z 和 VDM）不是基于证明的使用场景来测试模型。每个场景都是由用户构建的，因此该方法受到创建场景的成本和场景数量少的低覆盖率的影响。
其次，Alloy 已被用于查找代码中的错误：请参阅 Mandana Vaziri、Mana Taghdiri、Greg Dennis、Juan Pablo Galeotti 等人的博士论文。在所有这些中，发现了逃避常规测试的错误。
第三，值得注意的是有限详尽的测试形式正在变得可行。 Sarfraz Khurshid 是这项工作的先驱，他的论文是关于生成测试用例的，最初是在一个名为 TestEra 的工具中基于 Alloy，后来（与 Darko Marinov 等人）在一个名为 Korat 的工具中使用了一个更直接的解决方案较少声明性约束的方法。
我经常听到这样的争论：传统测试的一个缺点是它不完整，而 Alloy 分析是详尽和完整的（在一定范围内）。但是，第一个是谈论软件，第二个是谈论模型。这不是苹果和橘子的比较吗？
更新：我错了。比较的不是这个：testing code versus analyzing models。这是一个苹果与橘子的比较。相反，比较是这些：
Testing models versus analysis of models.
Testing code versus analysis of code.
这些是同类比较。
因此，无论工件是模型还是代码，您都可以比较两种分析：测试，对应于随机抽取相对较少的案例，没有大小限制，与小范围分析相对应，这涉及小范围内的所有情况。
感谢丹尼尔·杰克逊消除我的误解。
首先，当 Alloy 被发明时，唯一现有的用于分析数据丰富语言模型的工具（例如 Z 和 VDM）不是基于证明的使用场景来测试模型。每个场景都是由用户构建的，因此该方法受到创建场景的成本和场景数量少的低覆盖率的影响。
其次，Alloy 已被用于查找代码中的错误：请参阅 Mandana Vaziri、Mana Taghdiri、Greg Dennis、Juan Pablo Galeotti 等人的博士论文。在所有这些中，发现了逃避常规测试的错误。
第三，值得注意的是有限详尽的测试形式正在变得可行。 Sarfraz Khurshid 是这项工作的先驱，他的论文是关于生成测试用例的，最初是在一个名为 TestEra 的工具中基于 Alloy，后来（与 Darko Marinov 等人）在一个名为 Korat 的工具中使用了一个更直接的解决方案较少声明性约束的方法。