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

Question

我知道程序验证是计算机工程的一个分支——但它在现实世界代码库中的实际应用受到组合爆炸的限制。

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

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

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

Answer 1

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

看看pi-calculus来理解我的意思。

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