Java 中的形式化方法：契约式设计、JML 与验证工具入门

前言

提起“形式化方法”，不少Java开发者会想到数学公式、繁琐的证明，觉得距离业务开发太远。但实际上，现代Java已经吸收了大量形式化思想，通过断言、契约、静态检查等手段，在编译期或测试期就能发现隐藏的Bug.本文将带你用“开发者视角”走进形式化方法，了解：

• 什么是形式化方法，为什么它值得关心
• 契约式设计（Design by Contract）在Java中的落地
• JML（Java Modeling Language）和OpenJML的基本使用
• Checker Framework 等可插拔类型检查工具
• Java PathFinder 等模型见擦汗工具简介

所有示例均可在本地运行，帮助你零成本体验形式化验证。

---

一、形式化方法概述

1.1什么是形式化方法？

形式化方法是使用数学和逻辑的严格手段来规范、设计和验证软件系统的技术。它要求我们以精确的、无歧义的方式描述程序”应该做什么“，然后用工具自动检查程序是否满足规范。

常见的表示形式有：

• 契约式设计：为方法定义前置条件、后置条件和类不变量。
• 模型检测：穷举系统所有可能状态，验证是否违反特定性质（如死锁）。
• 静态类型检查：通过类型系统证明某些错误不可能发生（如空指针）。
• 定理证明：将程序行为转化为数学命题，由证明器推导。

1.2为什么Java需要形式化方法？

Java虽然拥有类型系统和异常机制，但仍无法表达一下约束：

• “这个参数不能为null，且必须是正数”
• “该方法执行后，列表的长度应该增加1”
• “在多线程环境下，这两个方法不能同时执行”

这些”隐藏的规则“通常只存在于注释或者开发者的大脑中，一旦被违反，Bug就产生了。形式化方法可以将它们变成可检查的代码，由工具24小时不间断地守护你的系统。

---

二、Java自带的“轻量形式化”：断言与Guava Preconditions

2.1使用‘assert’定义前置条件

Java的‘assert’关键字允许在代码中嵌入可校验的条件，如果条件为假，则抛出‘AssertionError’。

public int divide(int a,int b){
	assert b!=0：”除数不能为0“;
	return a/b;
	}

注意：assert默认在运行期间是关闭的，需要-ea参数启用。因此它更适合开发/测试阶段，不应作为生产环境的参数校验。

2.2 Guava Preconditions:生产级前置条件

Google Guava 提供的Preconditons可以优雅地替代手动if-else校验。

import com.google.common.base.Preconditons;

public void setName(String name){
	Preconditions.checkNotNull(name."名称不能为null");
	Preconditions.checkArgument(name.length()>0,“名称不能为空”);
	this.name=name;
}

这种方式已经具备了“契约”的影子：它把“输入必须满足的条件”写在了方法开头，任何调用者都必须遵守。
但是对于更复杂的后置条件（例如：“该方法必须返回一个偶数”），仅靠assert或Preconditions就无法表达了，这时需要引入JML。

---

三、JML：为Java插上契约的翅膀

3.1JML简介

JML（Java Modeling Language）是一种形式化规约语言，可以嵌入到Java注释中。
它支持：

• @requires：前置条件
• @ensures：后置条件
• @invariant：类不变量
• @assert：中间断言

JML不会影响正常编译，但可以被OpenJML、KeY等工具解析，进行运行时检查或静态证明。

3.2一个银行账户的例子

public class Account{
	private int balance;
	//@invariant balance>=0;
	/*@requires amount >0;
	@ensures balance==\old(balance)+amountl;
	@*/
	public void deposit(int amount){
	balance+=amount;
	}
	/*@requires amount>0&& balance >=amount;
	@ensures balance==\old(balance)-amount;
	@*/
	public void withdraw(int amount){
		balance-=amount;
	}
}

看不懂\old(balance)?它表示方法执行前balance的值。
解读：

• deposit要求金额大于0，执行后余额增加相应数值。
• withdraw要求金额大于0且余额充足，执行后余额减少。

如果没有遵守契约，比如balance被减成负数，工具会立即报告。

3.3使用OPENJML进行验证

OpenJML是一个开源工具，可以对带JML注解的代码进行：

• 运行时断言检查（-rac）：在运行程序时动态检查契约。
• 静态检查（-esc）：不运行程序，通过定理证明验证是否正确。

安装：下载OpenJML的jar包或使用Maven插件。
运行示例：

java -jar openjml.jar -rac Account.java

当某个调用违反了withdraw的前置条件时，会立刻抛出JMLIntetnalPreconditionError，帮你精准定位Bug。

四、其他形式化工具速览

4.1Checker Framework:可插拔的类型系统

Checker Framework可以为Java增加额外的类型检查器，例如：

• Nullness Checker：防止空指针异常。
• Index Checker：数组/集合下标安全。
• Lock Checker：并发锁遵守情况。

使用方式：在编译命令中加入-processor参数。

import org.checkerframework.checker.nullness.qual.*;

public String greet(@NonNull String name){
	return "Hello"+name;
} 

如果试图传入null,编译器会直接报错，将错误消灭在编码阶段。

4.2Java PathFinder（JPF）：模型检查并发

JPF是NASA开发的一款Java模型检查器，它会穷举程序所有可能的执行路径，找出死锁、活锁、断言违反等问题。
例如，你可以用它验证一个双线并发程序：

public class Counter{
	int value=0;
	void increment(){value++；}
}

JPF会探索所有线程交织顺序，检查是否存在数据竞争，并给出详细的错误轨迹。

4.3KeY:交互式定理证明

KeY可以直接对带JML的Java代码进行定理证明，能够处理循环、递归等复杂逻辑。它提供图形化界面，适合研究级别的高保证系统。

---

五、如何在实际项目中引入形式化方法？

不必追求“100%形式验证”，可以从以下步骤渐进式引入：
1.用assert和Preconditions取代注释：将隐式的前置条件显示化。
2.在核心模块添加JML注解：如资金计算、状态机、安全关键逻辑。
3.集成OpenJML到CI/CD：在测试阶段开启运行时检查，防止回归。
4.采用CheckerFramework：在编译期自动拦截空指针等低级错误。
5.对并发组件使用JPF：确保无死锁和竞争。
这种“轻量级形式化”已经能在现实工程中产生巨大收益。

---

六、总结

形式化方法听起来高冷，但其实在 Java 生态中已经有许多成熟的工具和理念可以直接使用。契约式设计教你如何写出“带规矩”的代码，**JML + OpenJML **让规矩可以被机器执行，Checker Framework 和 JPF 则在类型系统和并发领域提供了强有力的验证。

在软件质量要求越来越高的今天，掌握一点形式化思维，不仅能帮你写出更健壮的代码，更是高级工程师必备的硬实力。

如果你对某个工具的使用细节感兴趣，欢迎在评论区留言。