形式化方法

形式化方法是基于数学、逻辑、符号化语言，对软件系统进行合格建模、规范描述、逻辑推理和正确验证的一套开发与分析方法。不依靠人工测试猜测bug，而是用数学方式证明程序和系统是否正确。

形式化方法的核心作用在于，它可以用严格的逻辑写清系统规则，避免自然语言的歧义、模糊、理解偏差。在编码前和设计阶段时就能找出死锁、逻辑漏洞、边界错误，不用等测试后期才通过检测发现。它不仅仅只是能测出有bug，还能数学证明无bug，适合与高可靠系统。它可以约束模块与方法之间的调用规则，谁调用、要满足什么条件、执行完产出什么都有明确的规定。

形式化方法的主要特点：

严谨性：采用数学逻辑与形式语法，无模糊歧义。

抽象性：剥离五官细节，只建模核心状态与逻辑。

可推导性：支持逻辑推理、定理证明、模型检测。

高可靠性：从测试尽量找错变为数学证明无误。

下面举一个生活场景中的例子与编程中的例子来简单理解形式化方法：

电梯运行规则：

用自然语言来描述就是电梯到层开门，没人就关门，超载就不运行。形式化方法则是用逻辑符号严格定义则是电梯到达楼层->开门；开门停留超时^无请求->关门；载重>额定载重->禁止运行并报警。通过如此逻辑符号来定义电梯的运行规则，确保可靠性。

java方法契约：

public class DivDemo {
//@ requires y != 0; // 前置条件：调用时y不能为0
//@ ensures \result == x / y; // 后置条件：返回值一定是x/y
public static int div(int x, int y){
return x / y;
}
}

如上述代码，形式化方法约束调用规范，一旦传如y=0，工具可直接检测违规。

形式化方法与传统测试的区别在于，传统测试跑部分用例只能发现有错，不能确保无错。而形式化方法通过数学建模和逻辑证明，可严格证明形态满足规范。