Junit - 程序验证与白盒模糊测试？

Question

我了解程序验证是计算机工程的一个分支，但它在实际代码库中的实际应用受到组合爆炸的限制。

我还了解，作为设计软件更改的一部分，对于现有 Java 框架的修改，提前考虑算法的白盒、边界和黑盒测试会很有帮助。 （有些人称之为吊床驱动的开发 - 在编码之前思考。）

假设您采用这种想法并将其嵌入到 junit 样式测试中，我假设内容的计算机科学名称严格来说是“白盒测试/模糊测试”，不足以构成“程序验证”。

所以我的问题是 - junit 测试 - 白盒模糊测试或程序验证？

Answer 1

程序验证是在与您的应用程序相关的数学模型上证明数学属性完成的（它可以从编程语言的形式语义或手工派生，例如编写为您的网络服务建模的行为类型）。

查看pi-calculus 了解我的意思。

当然，junit与形式化程序验证无关。