![](https://csdnimg.cn/release/download_crawler_static/88626441/bg4.jpg)
E. Cohen
等人
/
理论计算机科学电子笔记
254
(
2009
)
85
1.1
贡献
我们为C引入了一个类型化的内存模型,其中指向结构的指针被解释为隐式
不重叠的对象,这些对象具有隐式不相交的字段(Sect.4)。这个模型是健
全的(节。5.1)和完整(第五节)。5.2)相对于无类型(C)内存模型,但
对程序员和定理证明者的负担明显较低(Sect.7)。我们还展示了其他C类型
(如联合,数组和位字段)是如何被合并到类型化模型中的。6.4)以及我
们如何处理性能问题,如位向量推理,这通常太慢而无法验证。
除了使验证更加方便和有效之外,这项工作还为将面向对象的验证技术
(例如所有权和类型不变量)应用于C程序奠定了基础,如在配套出版物[6]
中所述
第二章玩具语言
图3列出了一种玩具编程语言的结构,支持指针算术和在内存中任意位置的
更新(但不包括条件,迭代或过程抽象,可以使用标准技术添加的扩展
[11])。该语言支持整数(TI)、指针
(即,
t
是指向
t
的
指针)和结构类型
(T
S
,范围为S)。指针类型
和指针类型统称为
基元
类型(
TP
)。 表达式
(E)
是无侧射的,由二进制表达式e
1
e
2
(其中是任何C二进制整数运算
符),字段地址计算
e
~
f
(在C中它将被写为
&e->f
),类型转换(允许指
针和
整数之间的转换,从而允许任意指针算术),变量引用和literal-
als组
成。 常量和变量被限制为无符号的64位整数(但
可以用于保存具有适当类
型转换的指针)。公式(Formulas)由应用于表达式的
二元关系(binary
relationships)组成。 语句(S)由断言
、假设、内存写入、内存读取和类
型重解释组成
操作拆分和连接;程序(S)是语句的序列
结构类型被定义为程序环境的一部分。我们使用struct S
{
f
1
:t
1
;. ;
f
n
:t
n
}
作为谓词,这意味着结构S是程序环境的一部分,并且包含字段
f
1
,
.
,
f
n
类型为
t
1
,
...
,
t
n
.和C一样,结构类型是非循环的,即,一个结
构体S不能在任何嵌套层次包含一个类型为S的字段(但它可以包含类型
为S
的
字段)。
类型
化
程序
S
_
tp
(
e
)是
这样的程序
,其中在
程序
中
发生
的每个
表达式
e
都有一
个定义的类型
tp
(
e
),见图1。三是对
TP
的定义。语句
也必须是类型化的:
对于
e
1
:=
e
2
,我们要求
tp
(
e
1
)=
tp
(
e
2
)
n
,对于
v
:
=
e
,
我们要求
tp
(
e
)
=t
n
,对于某些t
∈
T
P
,以及对于
拆分
e和
连接
e,tp(e)=t
n