简介形式化Z语言规格说明与Z-EVES辅助工具资源包面向软件工程、安全关键系统设计与形式化验证方向的学习者及开发者。资料以Z语言建模和Z-EVES环境为核心提供从Z语言基础概念到工具实际使用的完整支持。压缩包共5个文件以可执行程序、PDF文档和HTML说明页为主exe文件包含适用于Windows的Z-EVES安装程序及运行环境PDF文档分别介绍用户指南与Windows平台使用指引HTML为下载、安装和使用的图文教程。包体仅8.63MB轻量易获取。已有820人学习适合正在了解形式化方法并希望在真实工具中编写Z规格、进行证明和检查的学习者。借助这份资源可以快速安装并上手Z-EVES理解Schema、关系、谓词等核心建模元素并通过官方指南减少环境配置弯路为后续在航空、医疗等安全攸关领域应用形式化验证打下基础。1. 为什么需要 Z-EVESZ 语言规范的形式化验证不能只靠读代码在民航、轨道交通这些对安全等级要求极高的领域需求规格里的一个小漏洞到编码阶段可能放大成一次事故。很多团队选择用 Z 语言把系统状态和操作写严谨但写出来的规范怎么保证是对的人眼很难排查一个两百行的模式里隐藏的类型错误或者不可满足的谓词。Z-EVES 就是在这个场景下被反复提起的辅助工具它能把 Z 规范解析成数学结构做类型检查并对用户声明的定理执行交互式证明不依赖任何商业授权。这篇文章面向那些想在真实项目里用 Z-EVES 但不知道怎么入手的工程师、学生和研究者我会从原理讲到环境搭建、实际验证再到我踩过的坑。2. 从集合论到证明器Z 语言的数学基础与 Z-EVES 的验证机制2.1 Z 语言的数学底座集合、关系与函数Z 语言的表达力植根于经典集合论和一阶逻辑。要用工具之前先要建立两个基本认识。首先Z 语言中所有的数据类型本质上都是集合。PERSON 是一个给定的基本类型表示“人”这个论域P PERSON 表示人的所有子集也就是“所有人组成的集合”而 PERSON → DATE 表示从人到日期的部分函数对应“某些人有生日日期”的约束。凡是能出现在模式里的量最终都可以被解释为某种集合关系。其次模式schema是 Z 语言组织信息的基本单元。一个模式由上下两半组成上半部分是声明signature列出变量及其类型下半部分是谓词predicate约束这些变量的取值。比如下面这段描述门禁系统初始状态的定义InitialAccessSystem ─────────────────── authorized : P PERSON inside : P PERSON ─────────────────── inside ∅这种书写方式看起来简单但精确到足以让机器判断如果 inside 里有元素不属于 authorized这个状态就不合法。Z-EVES 对规范的处理流程的第一步就是把这些声明和谓词展开成带类型标注的一阶逻辑公式。在实际使用中Z-EVES 需要的是带 LaTeX 风格控制符号的源文件。对于同一段定义在 Z-EVES 里我会写成\begin{schema}{InitialAccessSystem} authorized : \power PERSON \\ inside : \power PERSON \where inside \emptyset \end{schema}这里的 \power 和 \emptyset 分别对应集合的幂集与空集。Z-EVES 内部维护着一个“数学上下文”每加载一个模式就把其中声明的变量加入上下文谓词则作为后续证明可用的假设。这一步如果类型对不上工具会在解析阶段直接报错不会进入证明阶段。声明顺序会对类型推导产生实质影响。把 inside 放在 authorized 前面这里也能推导通过因为两个变量互不依赖但一旦后续定理里用 inside ⊆ authorizedZ-EVES 就要在上下文中找到 authorized 的类型。我的习惯是先声明被依赖的集合再声明依赖它的集合减少不必要的显式类型标注。常见的一个误区是以为 Z 语言只适合描述数据库或者通信协议这类“离散系统”。实际上Z 语言没有内置的时序概念它描述的是状态和操作前后状态关系所以被用在许多安全关键场景包括航空电子设备的模式切换逻辑和银行核心系统的账户状态机。Z-EVES 正好承接这些场景的自动化验证需求因此它才被叫做形式化开发的辅助工具。关于名字容易望文生义的另一个点Z 语言与“零知识证明Zero-Knowledge Proof”在英文缩写上沾边但完全不是一个东西。零知识证明的形式化验证走的是 Coq、Isabelle 那套构造型理论路线Z 语言走的是 Zermelo-Fraenkel 集合论路线。如果有人上来就拿着 ZKP 的论文问能不能用 Z-EVES 跑答案是不能。2.2 Z-EVES 的分层设计类型检查、上下文与交互式证明Z-EVES 本身可以拆成三个协作的组成部分数学上下文mathematical context、检查器checker、证明器prover。上下文是一个全局知识库记录所有已经定义的类型、常量和定理。检查器负责把规范文本解析成逻辑公式同时执行类型检查。证明器再根据用户发起的命令在上下文中搜索可用的定理和定义对目标进行重写与归约。这么设计的理由是Z 规范通常很大证明也往往复杂把“规范本身是否正确”和“定理能否被证明”分成两个阶段能大幅缩短排查链路。Z-EVES 的证明器并非全自动的 SMT 求解器而是一个交互式证明助手。它接受用户的证明命令比如展开某个定义、应用某条引理然后逐步缩小待证目标。你直接让它“全自动证明”一条涉及集合包含的定理它往往会卡在需要做 case analysis 的节点上。这时候由你告诉它按什么条件拆分情况证明才能继续推进。证明命令的粒度也反映在 GUI 界面上。Z-EVES 的 Windows 版提供一个编辑器能高亮显示当前证明目标并在证明树中展开每一步已经应用的规则。命令行版本则输出证明树状态。两边的内核是同一个所以不必担心 GUI 与命令行结果不一致——这一点在第五章的坑里我会详细讲。一个常见误用是拿 Z-EVES 当 model checker 用。Z-EVES 不会自动枚举状态空间也不会告诉你一个操作模式能否到达某个状态。它只回答“在给定上下文里目标公式是否可从假设推导出来”。功能边界想清楚才不会在工具上浪费时间。作为辅助工具Z-EVES 负责证明你声称的定理不负责从模型里自动揪出反例。期望定得太高往往会在用过一次之后就放弃整条形式化路线。3. 搭建 Z-EVES 环境并跑通第一个规范从下载到类型检查3.1 获取与安装Windows 与 Linux 的差异Z-EVES 目前的开源版本可以在 SourceForge 的项目页直接获取有 Windows 安装包和 Linux 二进制两个发行线。Windows 版本自带图形界面安装后能直接打开 .tex 后缀的规范文件。Linux 版本更适用于自动化批处理脚本我一般会在 CI 里调用命令行版的 z-eves 对规范做回归检查。Windows 安装过程几乎无脑下一步唯一要注意的是安装路径不要带空格否则后续命令行的批处理调用会撞上引号解析问题。Linux 下更简单解压后把可执行文件路径加到 PATH 里就行export PATH$PATH:/opt/z-eves/bin z-eves --version输出里会显示版本号和版权信息。如果看到 “command not found”先检查解压目录的 bin 下是否有 z-eves 这个可执行文件有些发行版把可执行文件命名为 zeves不是 z-eves。在 Linux 下跑命令行时Z-EVES 默认读取标准输入里的规范文本并把结果写到标准输出。为了不把每一步交互都敲进终端我习惯用脚本驱动z-eves spec.tex result.txt 21这个命令把 spec.tex 交给 Z-EVES所有证明命令、错误信息都进 result.txt。第二个参数 21 把标准错误也合并到输出文件方便一次性排查。执行完之后用 grep 过滤 ERROR 关键字能很快定位到失败点。grep -n ERROR result.txt | head -20这段过滤命令只保留含 ERROR 的行并显示行号。第一次看到 Z-EVES 输出时大概率会被满屏的提示信息吓到但真正需要关心的只有 ERROR 和 WARNING 两类。把其他信息当成正常过程输出即可。注意如果你的 Linux 发行版缺少 X11 库GUI 版可能无法启动。纯命令行模式不需要 X11这也是我推荐在服务器上使用命令行版的原因。3.2 第一个规范声明基本类型与状态模式先从最简单的门禁系统开始。第一步声明给定类型 PERSON表示系统中所有人员标识然后定义初始状态模式并把“进门后必须已被授权”写成不变式。完整的规范文件里模式定义通常放在前部定理放在后部。\begin{schema}{AccessSystem} authorized : \power PERSON \\ inside : \power PERSON \where inside \subseteq authorized \end{schema}接着定义初始状态\begin{schema}{InitialAccessSystem} AccessSystem \where inside \emptyset \end{schema}InitialAccessSystem 通过包含 AccessSystem 继承了 authorized 和 inside 两个变量及其不变式再额外约束 inside 为空。这种继承写法叫模式包含schema inclusion是 Z 语言里复用状态定义的标准方式。Z-EVES 在解析时会把继承关系展开成完整的声明和谓词集合。写完两个模式之后不要急着点证明。先用 Z-EVES 的检查功能把规范吃进去。如果直接运行证明命令多数情况下会先收到 “not checked” 的提示因为规范还没有进入上下文。正确顺序是解析 → 检查 → 生成上下文 → 证明。在 GUI 版本中选择菜单里的 Check 命令。命令行下可以执行z-eves -check spec.tex-check 参数只做解析和类型检查不进入证明。输出没有 ERROR 就说明声明和谓词的类型都对上了。这一步是复现的关键动作很多第一次用 Z-EVES 的人直接把例子粘贴进去就点证明结果被 “unresolved reference” 卡住。原因通常是前面的类型没有加载进上下文或者模式名拼写不一致。养成先 check、再 prove 的习惯能省掉一半无意义的报错。检查通过后就可以开始第一条定理的证明。我在实践中会把初始状态和操作模式放在同一个文件里这样上下文一建立所有定理都能直接引用。项目再大一点就按基础类型、状态模式、操作模式、引理、定理拆成五个文件用 include 组织起来。include 路径用相对路径避免不同机器上绝对路径不一致的问题。\begin{theorem}{InitInsideAuthorized} InitialAccessSystem \implies inside \subseteq authorized \end{theorem}这条定理说的是在 InitialAccessSystem 的假设下inside 一定是 authorized 的子集。由于初始状态里 inside 是空集而空集是任何集合的子集它在数学上必然成立。真正的问题在于 Z-EVES 能不能自动发现这条证明路径这要留给第四章展开。4. 把规范变成可证明的定理Z-EVES 的证明命令与回归流程4.1 从应用场景推导定理状态不变式与操作前置条件规范本身只是描述了“系统应该怎样”真正验证要做的是证明规范和我们的预期一致。以门禁系统为例我关心两件事初始化之后 inside 是否合法执行进入操作之后合法状态是否保持。第一件事可以直接写成定理\begin{theorem}{InitInsideAuthorized} InitialAccessSystem \implies inside \subseteq authorized \end{theorem}由于初始状态里 inside 是空集而空集是任何集合的子集这条定理在数学上必然成立。Z-EVES 能不能自动完成这条证明取决于我们给它的命令。第二件事需要定义“进入”操作。操作模式引入 Δ 约定表示状态会发生变化\begin{schema}{EnterSystem} \Delta AccessSystem \\ person? : PERSON \where person? \in authorized \\ person? \notin inside \\ inside inside \cup \{person?\} \end{schema}这里 person? 带问号后缀表示输入变量inside 带撇号表示操作之后的新状态。ΔAccessSystem 展开后提供了 inside 和 inside、authorized 和 authorized 两组变量。EnterSystem 有前置条件人已被授权、人不在场内和后置条件人进入场内。于是“进入操作保持不变量”就可以写成\begin{theorem}{EnterPreservesInvariant} AccessSystem \land EnterSystem \implies inside \subseteq authorized \end{theorem}这条定理是验证闭环里最典型的形态前提是状态合法再执行操作结论是操作后的状态依然合法。从直觉上讲如果 authorized 不变化而 inside 只是增加了一个原本就在 authorized 里的元素inside 当然还是 authorized 的子集。但机器不承认直觉它需要从类型信息、集合成员关系和等式替换里逐步推导。此时正好演示 Z-EVES 的证明命令。4.2 交互式证明命令reduce、split、prove 的配合在 Z-EVES 里证明不是一次“运行”完成的而是由一条条命令推进的。reduce 是最常用的起点命令。它把目标中出现的模式定义展开并尝试利用上下文中的已知事实完成自动化简。GUI 里操作的话打开目标 EnterPreservesInvariant先点 Prove再点 Reduce。证明窗口里会看到待证目标被展开成inside ⊆ authorized where: inside ⊆ authorized person? ∈ authorized person? ∉ inside inside inside ∪ {person?}此刻 reduce 已经把模式里的 where 子句提取成假设剩下的目标只是集合包含关系。接着集合包含关系可以按定义拆开X ⊆ Y 等价于对每个元素 ee ∈ X 推出 e ∈ Y。Z-EVES 对这种拆解的自动推理能力有限要么手动引入集合论引理要么用 split 对目标做逻辑分支。一个可用的证明脚本如下\begin{proof} reduce; split; prove; \end{proof}第一行 reduce 展开模式定义第二行 split 按逻辑连接词把目标拆成分支第三行 prove 在分支上调用自动推理。这个脚本能处理相当大一部分“状态不变式”类的定理。把脚本写在定理后面Z-EVES 重新加载时会自动重放不需要每次重新输入命令。有些读者可能希望直接敲 prove 一把梭在复杂规范上基本不可能。Z-EVES 的自动证明能力覆盖命题逻辑和简单的集合代数但只要出现量词或函数相等通常就要人工介入。我的经验是先走到“目标展开、假设足够、卡在某个集合论事实”的位置再判断缺引理还是缺拆分而不是指望工具猜出全部路径。4.3 把验证挂进日常循环批处理回归一个正式项目不可能只证明一条定理。更常见的做法是在规范里挂了三四十条定理每次改动规范都要全部重放。Z-EVES 批处理模式正好适合这个场景。写一个简单的 shell 脚本#!/bin/bash for f in theories/*.tex; do echo checking $f z-eves -check $f || echo FAIL: $f done这段脚本遍历 theories 目录下所有 .tex 文件逐一做类型检查。如果任何一个文件返回非零退出码就打印 FAIL。把这段脚本挂进 CI 工作流之后每次提交规范都能自动得到类型层面的反馈比等人肉眼 review 靠谱得多。需要说明的是批处理脚本只解决“检查”环节要让证明也自动跑需要把 proof 脚本写进每个定理文件里。Z-EVES 在处理 include 时会按先后顺序把各文件的定义纳入上下文所以交叉引用不会出问题。唯一要注意的是文件排序——B 依赖 A就必须让 A 先被 include。这也是第五章要详细展开的常见坑。5. 避坑与排查Z-EVES 使用中我记下的五个真实问题把拆过的项目遇到的问题记下来是最值得复用的资产。下面五条全部来自真实使用场景每一条都按现象、原因、解决的顺序写清楚。5.1 规范文件里出现中文注释导致解析失败现象在规范文件里写了中文注释Z-EVES 打开后注释变成乱码甚至解析报错说某个字符不在字母表内。原因Z-EVES 的输入解析器严格按 LaTeX 兼容的字符集合识别内容源文件默认按 ASCII 处理。中文字符在工具里不被识别为注释内容而会被当成非法符号。解决规范源文件一律用纯英文注释如果团队确实需要中文说明放在单独的说明文档里不要混进 .tex 规范文件。检查源文件传输时的编码转换尽量另存为 UTF-8 无 BOM 或纯 ASCII。这个习惯帮我避开了大量毫无价值的编码报错。5.2 类型检查报“变量类型未知”声明顺序与上下文隔离现象检查某个模式 D 时报错说变量 t 类型未知。单独看 D 的定义t 的声明就在上面几行。原因Z-EVES 检查时只使用当前数学上下文。如果 t 在另一个文件里被声明而那个文件没有被 include 进当前上下文检查器就不认识它。还有一种情况是 include 顺序反了——B 文件里的模式引用了 A 文件的类型但 B 先被加载。解决把所有公共类型和全局常量放在一个基础文件 base.tex 中其他文件按依赖顺序 include base.tex。顺序用 Makefile 或脚本固定下来避免手工排列。这样每次新增文件时上下文依赖关系一目了然。5.3 定理明显成立但证明不完缺一条辅助引理现象定理 EnterPreservesInvariant 的证明走到中间步骤目标变成只需证明 {person?} ⊆ authorized但 prove 命令无法完成。原因Z-EVES 的自动证明不会主动引入“单元素集合包含等价于元素属于集合”这条集合论定理而我们的规范上下文里也没有这条引理。工具不是不知道这条数学事实而是不知道你需要在当前这一步使用它。解决先把 {x} ⊆ S 这类目标归纳成通用引理在上下文里显式声明它。例如\begin{theorem}{SingletonSubset} \forall x : PERSON; S : \power PERSON (\{x\} \subseteq S) \iff x \in S \end{theorem}定理文件里先证明 SingletonSubset 并把它加入上下文再证明 EnterPreservesInvariant 时Z-EVES 就能检索到这条引理并自动使用。把频繁出现的集合论小结论固化成引理是减少手工证明命令的关键。5.4 证明脚本重放失败上下文改动影响后续重写现象同一份 .tex 文件昨天重放证明全部通过今天改了一处类型定义之后某条定理的证明脚本在第五步报错。原因Z-EVES 的证明重放严格按照脚本行的顺序与上下文状态执行。如果修改了前一个模式那么后续定理的假设集合可能发生变化原本能命中的重写规则不再可用。表面上“无关”的改动实际改变了上下文中某个常量的定义。解决每次修改规范后不只对修改处的定理重放而是对全部定理做完整重放如果失败先看失败步骤的目标与前一次有何不同再决定是补引理还是改脚本顺序。把证明脚本当作代码来管提交前跑全量回归。5.5 GUI 能过但命令行过不了会话状态掩盖问题现象同一个规范文件在 GUI 里点 Proof 菜单能通过命令行执行同样证明命令却报错。原因GUI 可能已经加载过某些上下文或执行过某些命令当前证明状态并不是从文件初始状态开始的。命令行每次都是全新解析不包含任何 GUI 历史状态。两者内核一致但 GUI 的会话状态会掩盖问题。解决在 GUI 里验证完任何证明都要用命令行从零重放一遍。我个人的习惯是GUI 只用来做交互式探索和阅读证明树真正的验证结果以命令行批处理的输出为准。从那以后我再也没有被“GUI 能过但 CI 挂掉”这种事困扰过。6. 让 Z-EVES 更好用的三个习惯引理拆分、命名体系与回归脚本6.1 把大定理拆成小引理每条证明控制在十条命令内大型规范里一条超过五十行的证明命令链是灾难。一旦某个模式改了中间步骤全部失效且没有可读性。实践证明把目标定理拆成三五个小型引理每条证明控制在十条命令以内是最容易维护的方式。例如要验证一个复杂操作先证明前置条件满足再证明类型不变最后证明核心不变量。每个小引理独立重放失败点定位到具体一条引理而不是整条证明链。6.2 给定理一套可读的命名前缀让证明脚本变成文档我会按用途给定理加前缀init_、op_、inv_。op_EnterSystem_Pre 表示进入操作的前置条件引理inv_InsideAuthorized 表示不变量相关。目录结构则固定为基础类型、状态模式、操作模式、引理、顶级定理五层。这样即使某个文件半年没打开靠名字也能立刻知道它在验证链中的位置。配合全量回归脚本Z-EVES 就能真正嵌入开发流程。真正让我下定决心固定这套习惯的是一次返工当时一个门禁项目里改了授权规则我去掉了一条看似无关的引理结果两天后才发现另一条定理的证明重放失败。从那以后每次改规范我都强制走一遍“改文件 → 全量 check → 全量重放证明 → 对比失败清单”的流程。希望这套流程对你也有用。本文还有配套的精品资源点击获取