最近在上一门叫做新技术讲座的课，我估计好多同学是看到讲座这两个字感觉这课会很水才选的，但实际上这门课讲的内容是非常硬核的软件工程形式化方法，而且授课老师也是国内第一批研究软件工程形式化方法的教授，现任日本埼玉大学教授，且上课非常认真负责，每节课都有课堂练习。不过了解了软件工程形式化的概念后，发现这个研究方向真的了不得，简直可以颠覆整个软件行业。 在早期的软件开发过程中，开发者们往往拿到问题后就直接开始编码，软件往往会出现各种各样的问题，大部分软件的质量十分低下，被称为“软件危机”。为了解决软件质量低下的问题，人们提出了软件工程化的思想，也就是目前主流的软件开发方式，引入了从需求分析到最后编码实现这一系列的过程，以及需要遵守的一系列规范，并定义了如CMMI这样的规范性等级。然而软件工程里面有很多内容的规范是非常主观的，没有一个确定的评定标准，另外很多步骤只能尽量争取正确，但根本无法确保正确，比如对于软件的测试，在软件测试这门课中就了解到全覆盖基本上是不可能完成的，并提出了语句覆盖、判定覆盖、条件覆盖等一系列只能尽量争取正确的测试覆盖。而且在执行的过程中，就算是CMMI 5级的开发单位也往....