论文部分内容阅读
由于泛型构件具有广泛的复用性，我们相信有必要为泛型构件定义内存访问与操作的安全规则(即泛型概念的安全性规则)。然而当前的程序设计语言和编译系统无法高效地检验泛型概念的安全性。本文给出了用于验证泛型概念安全性的通用模型Safe-GConcept。此模型扩展了多态类型系统(类型系统F)：引入了子类型关系、内存地址类型、泛型指针类型、数理逻辑等等。定义了泛型概念的安全规则的指称语义。比起类型化的汇编语言，该模型不仅仅检验最基本的内存访问的安全性。同时，本文指出了在C++程序设计语言中存在的泛型指针操作的不安全因素并针对性地引入了新的检验机制。本文定义了安全环境的概念作为检验内存安全状态的标准，并且证明了该模型具有可靠性。在实践方面，我们在本文中把定义的数理逻辑系统映射为用指称证明语言(DPL)描述的公理系统，用带有指称证明特征的定理证明器ATHENA实现了该系统，利用ATHENA来证明内存操作、泛型指针操作和泛型概念的安全性，并用ATHENA来检验证明的正确性。