JUnit - 程序验证VS WhiteBox模糊？

Question

我理解程序验证是计算机工程的一个分支 - 但它对现实世界代码基础的实际应用是由组合爆炸的限制。

我也明白，作为设计软件更改的一部分，对于对现有的Java框架进行修改，提前考虑算法的白箱，边界和黑箱测试是有帮助的。（有些人称这个吊床驱动的发展 - 在你的代码之前思考。）

假设您认为此思考并将其嵌入junit样式测试中，我假设内容的计算机科学名称是严格的“白箱测试/模糊”，而且不足以包括“程序验证”。

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

Answer 1

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

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

当然，JUNIT与正式的计划验证无关。