Logical foundations for typed object-oriented languages
Logical foundations for typed object-oriented languages
复制标题
类型化面向对象语言的逻辑基础
DOI：
10.1007/978-0-387-35358-6_26
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
Peter Müller
中科院分区：
文献类型：
--
作者：
A. Poetzsch;Peter Müller
本文介绍了最重要的面向对象语言特性的逻辑基础，包括抽象类型、动态绑定、子类型和继承。这些基础与面向对象的内核语言一起介绍。我们展示了这些语言的对象环境如何以代数的方式形式化。在此基础上，开发了面向对象程序形式化验证的hoare式逻辑。
This paper presents logical foundations for the most important object-oriented language features, including abstract types, dynamic binding, subtyping, and inheritance. These foundations are introduced along with an object-oriented kernel language. We show how object environments of such languages can be formalized in an algebraic way. Based on this foundation, we develop a Hoare-style logic for formal verification of object-oriented programs.