摘要
构造性类型理论可作为程序开发的理论基础,其中类型作为程序规约,证明过程作为程序开发过程,从证明抽取满足程序规约的程序.本文提出了一种构造性类型理论TTOOP,引入了类规约类型和类类型的概念.类是类规约类型的元素,它又是一种类型,类的元素为对象.通过证明类规约可构造类,由此构造面向对象软件.
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.
出处
《计算机学报》
EI
CSCD
北大核心
1997年第1期50-57,共8页
Chinese Journal of Computers
基金
国家863高技术基金
国家自然科学基金
关键词
类型理论
面向对象
程序设计
自动程序设计
Type theory, object-oriented programming, program synthesization,automatic programming.