论文部分内容阅读
以往对程序语言的形式化验证不能与类型系统相结合，推理程序的规则依赖于确定的类型。 这篇论文将尝试抹去类型与断言的界限。本文将在分离逻辑的基础上，向状态中引入关于类型的映射来构建一个支持类型的存储模型，并以此为一个支持创建复合类型、类型转换和指针访问的编程语言建立一套公理语义。本文将给出程序语言的语法和操作语义，断言语言的语法语义以及证明了可靠性的程序语言的公理语义规则，根据给出的公理语义规则，可以验证程序中关于类型的性质并且能够推理包含复合类型创建的程序。