A Type-Theoretic Memory Model for Verification of Sequential Java Programs
A Type-Theoretic Memory Model for Verification of Sequential Java Programs
复制标题
用于验证顺序 Java 程序的类型理论内存模型
DOI：
10.1007/978-3-540-44616-3_1
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
E. Poll
中科院分区：
文献类型：
--
作者：
J. Berg;M. Huisman;B. Jacobs;E. Poll
本文详细介绍了在“LOOP”项目（[14，20]）中验证顺序Java程序的内存模型。这种内存的构建块是单元，从它们可以存储任意Java对象的字段内容的意义上说，这些单元是无类型的。主存被建模为三个无限系列的这样的单元，一个用于存储堆上的实例变量，一个用于存储堆栈上的局部变量和参数，一个用于静态（或类）变量。在PVS和Isabelle/HOL中，通过几个Java程序的例子，说明了这种内存模型的基础上的验证，涉及语言的各种微妙之处（wrt.存储器存储）。
This paper explains the details of the memory model underlying the verification of sequential Java programs in the “LOOP” project ([14,20]). The building blocks of this memory are cells, which are untyped in the sense that they can store the contents of the fields of an arbitrary Java object. The main memory is modeled as three infinite series of such cells, one for storing instance variables on a heap, one for local variables and parameters on a stack, and and one for static (or class) variables. Verification on the basis of this memory model is illustrated both in PVS and in Isabelle/HOL, via several examples of Java programs, involving various subtleties of the language (wrt. memory storage).