计算机编程的公理化基础（091206）
闵应骅
    大家知道，在1960年代，最著名的计算机程序语言是ALGOL60，基于精美而严格的语法，形式化为一种上下文无关语言。然而，语义更重要，但并没有形式化。英国人相信，形式化应该包含一组公理，使程序员能写出正确而有效的程序。但这个想法本身就无法反映不断前进的计算机体系结构，以及同一程序不同的实现策略。在学术界，这个争论至今未息，而在工业界，对于实际问题，早就不用这种思路了。这种思路的主要优越性是保证程序的正确性。它在软件设计中没得到应用，却在硬件设计中被接受。这就是为什么模型检验(model checking)得到如此的重视。在WRTLT09上，Jacob Abraham在他的特邀报告中大谈 Property checking（特性检验）。当我问他模型检验和特性检验有何区别时，他说是一样的。我来不及继续追问：既然二者相同，为什么要搞两个词呢？
    现在的程序如此复杂，软件测试越来越显得效率不高。其实，软件测试与其说是测试程序，不如说是测试程序员。告诉大量出错的程序员赶快离开这个行业。而形式方法支持程序员的直观判断，并不是取代软件测试。测试帮助发现和纠正程序错误，并不能证明程序的正确性。当然，现在，形式验证离程序正确性证明还差得很远。但应用离散数学的一些分支已经在形式化方面大有进展，例如对象、类、利用堆(heaps)、指针等编程概念，已经引入到当今的标准编程语言，新型的代数已经运用到分布式、并发和通信过程，模型逻辑和抽象域的新形式可以简化关于编程的人机交互，例如行为的动态逻辑、时态逻辑、分离逻辑等。这些东西现在也用于计算生物、遗传学和社会学。
    值得注意的是近年来在逻辑和数学证明自动化方面的进展。随着计算机性能的提升，证明发现和反例产生已经有上千倍的提速。为了security和safety(这两个词都被翻成安全，但意义并不相同），硬件和软件的设计验证都非常重要，而且已经得到工业界的重视。太多事故的教训教育了我们。
    今后需要学术界和工业界的合作。工业界注重近期见效的比较容易解决的热点问题，而基础研究则与此相反，研究这些现象的最广泛的可能范围，寻找必然性的知识，造福于下一代。工业界在开发许多工具，也说了这些工具的优越性，但较少说这些工具出来的结论为什么是正确的。最近我看到一位工业界同仁在评论一篇论文时说：集成电路中串扰的故障模拟在某公司的工具中已经解决。既无科学论文说明这一点，又有许多研究还在进行串扰的定量分析，怎么可能用一个工具就解决了？我表示怀疑。现在我们一些研究者，甚至在公司的工具基础上做研究，而不是面向实际问题做研究。基础研究应该给公司的工具开放提供新思想、新方法，走在公司工具的前面，而不是走在它的后面。

转载本文请联系原作者获取授权，同时请注明本文来自闵应骅科学网博客。
链接地址：https://blog.sciencenet.cn/blog-290937-276461.html

上一篇：澳门之旅（091205）
下一篇：中国大陆新增6位IEEE院士（091208）