论文部分内容阅读
从“软件危机”爆发至今,人们提出了很多新方法和新工具,这些方法和工具致力于解决“软件危机”的各个方面。但现有的这些解决方案并没有使人们彻底地从“软件危机”中解脱出来。用形式化方法开发正确、高效的算法程序,被当今计算机界誉为克服“软件危机”,提高软件可靠性和生产效率的革命性途径。 薛锦云教授在国家863和多项国家自然科学基金课题的资助下,根据多年从事算法程序设计理论研究的成果,提出了一种简单实用的设计和证明算法的形式化方法——PAR。在该方法的指导下,定义了Radl(Recurrence-based Algorithm Design Language)算法设计语言来描述算法规约和抽象算法。定义了Apla(Abstract Programming Language)语言来描述抽象程序。 自动程序转换系统是整个PAR方法理论框架的重要组成部分,是用PAR方法开发高级语言程序的辅助工具。本研究选取新型程序设计语言Java作为程序自动转换系统的目标语言,在课题组前期研究的基础上,研究和实现了支持泛型程序设计的Apla-Java自动程序转换系统。这项研究是目前两项国家自然科学基金课题“PAR方法应用于Java程序开发方法研究”和“基于PAR方法的算法设计形式化和自动化研究”的子课题。 本研究主要进行了以下工作: 1 对原有程序自动转换系统进行了大量的测试并作出测试报告。 2 对整个自定义Java可重用部件库的结构进行了优化和调整,对部件库进行了完善和补充,使其更好、更自然的支持高级功能的实现,同时也保持了对已实现功能的支持。 3 对转换器进行了重构。在此基础上,对转换系统的原有转换功能进行了完善,使得转换器的语法检测功能更加强大;并为转换系统添加了一些新的特性,增强了其可用性。 4 进一步完善了自动程序转换系统泛型问题中的类型参数化问题,实现了泛型子程序的成功转换,添加了特殊符号直接作子程序参数名等功能。 5 研究了Apla中支持的泛型程序Java实现,并最终在本系统中实现了对其转换的支持。 6 研究了Apla中自定义泛型ADT机制的Java实现,并在本系统中实现了其转换。 目前一些形式化方法的支持工具,只能支持规约的编辑、求精或手工证明等。而本系统在以下方面体现出其特色和创新: 1 它是PAR方法的重要组成部分。问题的算法用Radl语言描述,Apla程序在Radl算法的基础上得到。Radl语言的引入使得算法和程序相分离,并具有引用透明性,这些都有利于算法和程序的推导,从而可保证作为系统输入的Apla程序的正确性。 2 允许用户在Apla程序中使用简单的数学符号; 3 强迫用户使用抽象数据类型设计程序,使其注意力集中于算法的推导; 4 在部件库的支持下,用户使用组合数据类型就像使用简单数据类型一样简单方便; 5 集Apla程序的编辑、编译、运行于一体,使用方便; 6 为我们正在研制的程序设计智能教学软件提供了支撑。 7 能提高软件的可靠性和软件的开发效率,可以为克服“软件危机”作出有益的贡献。 Apla语言具有高度抽象、表达能力强等特点,并且含有明显的语法机制支持泛型程序设计;而Java语言没有明显的机制支持泛型程序设计。如何使用Java语言实现Apla的这些机制是本研究的重点和难点。