这周我读了《软件工程——实践者的研究方法》，这是一本比较理论的书，看起来略有一些乏味。其中谈到很多项目质量管理，开发模式相关的东西，感觉都太泛泛了。因为比较缺乏实战经验，书中又很少讲实际例子，因此这些内容并没有给我留下太多印象。
但书中花了好几章的篇幅用于讲软件测试，这部分内容我很感兴趣。如何开发出没有bug 或 bug 很少的程序一直我想探究的问题。PL 领域有很多相关的研究用于保证程序正确性和代码质量，例如：模型检查、程序分析、程序证明等。这些方法代价太高，一般只用于十分重要的工程中，例如核反应堆控制系统，动车控制系统等。普通的软件工程很难用到这些方法。
对于普通软件工程来说，测试是很好的保障软件正确性的方法。测试的种类有很多，有单元测试、回归测试、压力测试、alpha 测试、beta 测试等。不同的测试的侧重点不一样，有的是针对软件安全性，有的是针对软件正确性，有的是针对软件易用性。
在看了这些软件工程的书之后，我对保证软件正确性这个问题有了一些新的想法。在程序中，类型可以用来约束程序行为，保证函数调用是安全的。但目前的类型只是描述了这个东西是什么，却很少有关于这个东西性质的描述。例如在 Int 类型，只描述了它是整数类型，而这个整数类型具体映射到解空间是什么东西，却没有涉及。它可以是一个计数器，可以是一个素数，可以是一个年份等等。而且，这些具体在解空间中的语义，有时候还有一些约束条件，例如：计数器通常需要是正数，素数必须满足定义等。在程序验证中，这种类型叫做 “精化类型” (refinement type)。但是学术界用这种方法，通常是用来表示霍尔逻辑，并且交给 SMT Solver 进行约束求解，这种基于验证的方法前面已经提到，代价太昂贵。
因此，我们可以用测试、运行时断言来保证精化类型的约束满足。