论文部分内容阅读
使用形式化方法对程序进行验证是保证软件可信的重要手段．对于像C语言这样的较低级的命令式语言可以直接对内存进行操作，对其操作语义或公理语义的形式化需要基于合适的内存模型．传统的字节内存模型可以很好地描述各种内存操作，但是无法保证安全性，同时使程序验证变得异常复杂．面向对象语言的内存模型则具有较高的抽象性，便于程序验证，但不适合描述低级的内存操作．结合字节内存模型和面向对象语言内存模型，提出一种安全的类型化的内存模型，既可用于对语义的形式化，也可用于基于霍尔逻辑的程序验证．此内存模型既允许指针算术、结构赋值、