传统软件测试与合金实例生成

Question

在传统的软件开发中，测试代表了您想让软件表达的意思。通过对软件执行测试，您可以了解该软件是否具有您认为的含义。 “这就是我想说的，我真的这么说吗？”

合金实例向您展示了您在模型中所说的内容。你检查实例并决定这是否是你想让模型说的。 “这是你说的，是你想说的吗？”

您是否同意软件测试和 Alloy 实例生成之间的这种区别？在软件测试和 Alloy 实例生成的比较中，您有什么要补充的吗？

Answer 1

是的，您用自己的话描述了验证（我是否构建了正确的东西）和验证（我是否构建了正确的东西）之间的区别。

虽然您命名的“测试”用于验证软件是否已正确构建，但恕我直言，Alloy 可用于验证和验证，如下所述：

验证：从空谓词生成实例为您提供符合您的规范的实例，让您掌握指定的内容。您可以使用从审查这些实例中获得的知识来验证您的规范。 事实上，这些实例将帮助您回答以下问题：生成的实例是否反映了我要指定的内容？（我构建的东西是否正确）。

验证 在 Alloy 中，您还可以通过使用断言来验证您的规范中是否尊重某些属性。检查断言会产生可能的反例，其存在可以证明您的规范对违反的断言的符合性。如果有的话，通过检查断言生成的反例可以帮助您回答这个问题：我是否正确地指定了我的模型 w.r.t.我的断言？（我做对了吗？）。

Answer 2

有趣。我使用合金来表示“测试数据”（不是软件本身）。通过这种方法，我发现使用测试数据和编写测试代码就是验证；但是通过正式规范指定测试数据是验证。当我通过 Alloy 指定测试数据时，我需要比软件测试更广阔的视野。

例如，考虑软件取日期数据，你必须测试软件可以拒绝无效的日期值。另一方面，当您指定测试数据以通过 Alloy 测试软件时，您必须定义满足“日期”要求的数据。

我认为这些观点的变化意味着验证和验证之间的差异（以及软件测试和合金实例生成之间的差异）。