基于类型理论的面向对象程序自动化

软件工程的重要目标之一是实现软件开发的自动化。为此，我们以构造性类型理论为基础，深入地探讨了面向对象方法的基本机制及面向对象程序的构造方法，并取得了如下成果：1、以Mrtin-Luf的构造性类型理论为基础，建立了支持面向对象程序设计的一种类型理论TTOOP。2、以TTOOP为基础，设计了一种面向对象软件形式规约语言OOSL。3、以TTOOP为基础，提出了以规程为单位，自顶向下、逐步求精的程序设计方法。4、设计实现了两个面对象软件自动化实验系统DTPS和JDAUTO/O。