基于类型理论的面向对象程序设计

OBJECT-ORIENTED PROGRAMMING WITH TYPE THEORY

构造性类型理论可作为程序开发的理论基础，其中类型作为程序规约，证明过程作为程序开发过程，从证明抽取满足程序规约的程序．本文提出了一种构造性类型理论ＴＴＯＯＰ，引入了类规约类型和类类型的概念．类是类规约类型的元素，它又是一种类型，类的元素为对象．通过证明类规约可构造类，由此构造面向对象软件．

A constructive type theory TTOOP, in which the concept of class specification type and class type are introduced, is proposed in this paper. Class is an element of the class specification type, and the elements of the class type are the objects. By proving class specifications, classes can be constructed and the object--oriented software can be constructed with these classes.