Safe type checking in a statically-typed object-oriented programming language
Safe type checking in a statically-typed object-oriented programming language
复制标题
静态类型面向对象编程语言中的安全类型检查
DOI：
--
复制
发表时间：
1993
期刊：
影响因子：
--
通讯作者：
Kim B. Bruce
中科院分区：
文献类型：
--
作者：
Kim B. Bruce
在本文中，我们介绍了一个静态类型，功能，面向对象的编程语言，TOOPL，它支持类，对象，方法，实例变量，子类型和继承。
设计一种静态类型的面向对象语言，它几乎和Smalltalk一样具有表达能力，但在类型系统中没有漏洞，这已经被证明是令人惊讶的困难。静态类型检查面向对象语言的一个特殊问题是确定超类中提供的方法在继承到子类中时是否继续进行类型检查。这个程序在我们的语言中通过提供类型检查规则来解决，这些规则保证作为类的一部分进行类型检查的方法将在继承它的所有法律的子类中正确地进行类型检查。此功能使库提供程序能够仅提供具有可执行文件的类的接口，并且仍然允许用户安全地创建子类。
TOOPL的设计一直由语言的语义分析指导，该语言的语义分析是根据F-有界二阶lambda演算的足够丰富的模型给出的。这种语义通过提供一种方法来证明语言的类型检查规则是合理的，确保良好类型的术语产生适当类型的对象，从而支持语言设计。特别是，在一个良好类型的程序中，不可能向一个缺少相应方法的对象发送消息。
In this paper we introduce a statically-typed, functional, object-oriented programming language, TOOPL, which supports classes, objects, methods, instance variable, subtypes, and inheritance.
It has proved to be surprisingly difficult to design statically-typed object-oriented languages which are nearly as expressive as Smalltalk and yet have no holes in their typing systems. A particular problem with statically type checking object-oriented languages is determining whether a method provided in a superclass will continue to type check when inherited in a subclass. This program is solved in our language by providing type checking rules which guarantee that a method which type checks as part of a class will type check correctly in all legal subclasses in which it is inherited. This feature enables library providers to provide only the interfaces of classes with executables and still allow users to safely create subclasses.
The design of TOOPL has been guided by an analysis of the semantics of the language, which is given in terms of a sufficiently rich model of the F-bounded second-order lambda calculus. This semantics supported the language design by providing a means of proving that the type-checking rules for the language are sound, ensuring that well-typed terms produce objects of the appropriate type. In particular, in a well-typed program it is impossible to send a message to an object which lacks a corresponding method.