形式方法

凡是涉及安全相关或关键软件开发，形式方法几乎都会谈起。形式方法是一种以（离散）数学为基础的软件开发手段。理想状态就是要像解数学题一样，从需求说明（一旦形式化建立起来）可一步步严格推导到实现。从另外一个角度来看，软件测试就变得可有可无，既然实现可以证明是符合需求。

一说形式方法，很多人都会集中在描述方面(formal specification)，如Z, CSP, B, VDM，而忽略了refinement/verification阶段。如果specification不能跟implementation连接话，那更完美的描述也如同废纸。而且这个连接最好是自动：通过automated theorem prover (推导形式）, 或通过model checker（搜索形式）。

个人不看好形式方法。原因一，它不能根本上解决需求问题。需求来自于用户和特定的领域(domain)，形式方法不可能证明它的描述does the right thing (i.e. validation)。而需求描述体现于知识由用户或stakeholders到开发者的传递和交流协调过程。这里涉及的问题很多，以后再讨论。而需求问题一向是软件失效的主要来源。

原因二，它的推导和证明过程都是基于理想化的abstract machine, 不能连接到最终运行的物理实现平台上，例如大到编译器，小到memory clips and logical gates。要把这一切都推导出来，现有的技术来说，是绝对不可能。

其他限制如scalability (可以通过hybrid或lightweight方法来改善）和过高的开发费用等。

当然它有一定的应用：主要是通信/加密协议，算法，或电路设计。我个人理解，也就是当软件的主要问题不是需求问题，而是特定的设计问题。

形式还是要讲究滴，呵呵。