Page 146 - 《软件学报》2021年第6期

1720 Journal of Software 软件学报 Vol.32, No.6, June 2021

Blazy 和 Leroy 在 Coq 中给出了 C 的子集 Clight 的大步语义,它支撑了 CompCert 项目的 C 语言编译器验证任
务 [32] .Ellison 等人在 K framework 中形式化 C 语言的可执行语义,并利用 GCC 测试集进行全面测试 [33] .关于 C++
语言,Wasserrab 等人在 Isabelle/HOL 中对 C++中的多重继承提供形式化语义和类型安全性的形式化证明 [34] .
Norrish 在 HOL 中对 C++的多种动态语义进行了形式化建模 [35] .关于 Java 语言,Drossopoulou 和 Eisenbach 对
Java 子集的操作语义和类型系统进行形式化描述,并给出了类型系统可靠性的证明 [36] .Bogdanas 等人在 K
framework 中首次完整地实现 Java 1.4 的形式化可执行语义,并开发了一个涵盖所有 Java 构造的综合测试集 [37] .
与本工作相比,上述工作形式化不同的程序语言,在基本思想方法上有许多共通之处,而在技术路线上亦有
差异.如文献[32]中给出的 Clight 语义采用 Coq 的归纳类型定义,在形式化证明中易于使用,但不可执行.在文献
[31]中给出的 C0 语义使用浅层嵌入(shallow embedding)将基本操作直接表示为 Isabelle/HOL 中的函数,而本工
作的 Yul 语言形式化采用完全的深层嵌入(deep embedding),具体定义基本操作的语法和语义.在 K framework
中所定义语义均为可执行语义,但基于该工具的程序验证结果尚未达到证明辅助工具所允许的可信度,尽管由
K framework 向 Coq 等证明辅助工具生成验证结果证书(certificate)的工作正在开展.

2 Isabelle/HOL 简介

本文的形式化工作在高阶逻辑证明辅助工具 Isabelle/HOL 中完成,它支持以函数式编程方式对系统进行形
式规约,以及运用证明策略(tactics)或结构化证明语言 Isar 对系统性质进行证明 [38] .以下通过简单例子说明
Isabelle/HOL 中进行类型定义、函数定义、函数求值的方法.
在 Isabelle/HOL 中,用关键字 datatype 进行数据类型定义.下面例子中定义了类型 T,具有该类型的元素须由
构造子 Ty1,Ty2,Ty3,Ty4 之一进行构造.若使用 Ty4,则需要提供整型参量,而其他构造子无需参量.
datatype T=Ty1|Ty2|Ty3|Ty4 int
Isabelle/HOL 中定义了内建列表类型′a list,这里,′a 是类型变量,即列表为多型(polymorphic)类型,如 int list
表示整型元素的列表,T list 表示 T 类型元素的列表,等等.函数定义往往使用关键字 fun 进行.以下定义函数
ins_lst,用于向 T 类型列表中无重复地插入元素.
fun ins_lst::“T list⇒T⇒T list” where
“ins_lst ts t=(
if t∈(set ts) then ts else ts@[t]
)”
本定义中,::后为函数 ins_lst 的类型.Isabelle/HOL 中,A⇒B 表示由类型 A 到类型 B 的函数类型,其中,⇒右结
合.因此,函数 ins_lst 作用于给定的 T 类型列表和给定的 T 类型元素,返回新的 T 类型列表.关键字 where 后为该
函数的具体定义:当元素为类型 T 的列表 ts 中不存在试图插入的元素 t 时,则在该列表的尾部添加此元素;否则,
该列表保持不变.该定义中,set 是 Isabelle/HOL 的库函数,set ts 获取表 ts 中元素所组成的集合;@表示同类型列
表之间的连接.此外,后文亦用到操作符#,用于连接单个元素与列表.
关键字 value 支持对表达式进行求值.下面给出对函数 ins_lst 进行求值的两个示例.本工作中,对语义的测
试就是借助 value 关键字进行的.
value “ins_lst[ ] Ty1” 结果:“[Ty1]”::“T list”
value “ins_lst[Ty1,Ty3] Ty1” 结果:“[Ty1, Ty3]”::“T list”

本文的形式化工作中大量使用基于列表的映射类型,该类型为自定义类型.具体而言,′a list_map 表示由整
型元素到可选的′a 类型元素(Some ′a 或 None)的映射.它由整型和′a 类型元素所组成二元组的列表实现(事实上,
′a list_map 定义为(int×′a) list 的同义词).对列表中的二元组(i,a),若它后面不再有形为(i,a′)的二元组,则视为 i 映
射到 Some a;若对某个整型元素 i,列表中不存在形为(i,a′)的二元组,则视为 i 映射到 None.函数 lm_dom 给出某
个′a list_map 类型映射的定义域,函数 lm_get 给出某个整型元素被映射到的值.