希望您已阅读本系列的第1部分，在那里您可以发现传统方法在验证铁路联锁的安全需求时不是很给力。
这次我的任务是说服大家形式化验证是一个更好的选择。
那么什么是形式化验证呢？
好吧，我们已经知道验证意味着什么。 “形式化”其实就是指“数学”。因此，形式验证意味着将验证问题转化为数学问题。大家都知道一旦连结到数学领域，我们就可以获得数学所带来的严谨性和精确性。
数学中的典型活动是发表陈述或声明（statements），然后证明（prove）它们是真实或成立的。听起来很熟悉？数学陈述的证明必须是令人信服的，无懈可击的，任何受过适当教育的人看过证明过程后都应该同意陈述是真的。当然，在实践中，最后一部分可能会难以实现。即使接受适当的教育，数学的某些部分也很难理解。但让我们考虑一个算术的经典例子。考虑如下声明：
1 + 2 + … + n = n(n + 1)/2
看我的答案之前请考虑几秒钟，看看你能否想到证明方法。
Hmmm…
在我看来，最优雅的证明方法，是在把等式左侧连续写两次，每次写数字序列的方向不同。比如：
1 + 2 + … + n
n + (n-1) + … + 1
请注意，数字的顺序在较低的一行中是倒序。如果我们查看此表达式中的列，每列的总和为 n+1，并且有n 列。因此，所有这两行数字相加总和是
n(n + 1)
然后我们就得到了如下的结果
2(1 + 2 + … + n）= n(n + 1)
这意味着
1 + 2 + … + n = n(n + 1)/2
这不是一个令人信服的论点吗？
相反，如用测试方法来验证这个数学公式是成立的，我们可以把数学公式的左侧看做是规范（specification），右侧看做是实现（implementation）。要验证实现的正确性，需要选择测试用例，也就是选择n 的具体赋值，然后做简单数值计算来验证等式两端是否一致。问题是，自然数的值域是无限的。测试永远也做不到所有n 赋值的全覆盖。
通过这个简单的例子，我试图告诉你如何进行数学证明，并期待你能同意，如果做得好，数学证明的结论是无懈可击的。事实上，数学证明是人类唯一已知的可以做到无懈可击的证明方式。正如我们在第1部分中提到的那样，验证问题的主要障碍是潜在状态空间的巨大规模。数学也为此提供了解决方案，因为数学问题中所有领域（domain）都是巨大的，通常是无限的（infinite）。
非常不巧，我说了一半时间到该下班了
。如果您希望更多的了解形式化验证的适用性，请等到下一篇文章。