论文部分内容阅读
薛锦云教授在国家863和多项国家自然科学基金的资助下,创造性地提出了一种形式化开发方法——PAR方法。就是用数学与逻辑的方法来描述和验证软件,而PAR方法描述的程序又是经过严格的推导、证明,所以保证了程序的正确性和可靠性。而且由于PAR方法和PAR自动转换系统实现有算法规约到抽象程序以及到可执行程序的自动转换,这样就部分实现了软件开发的自动化。其中Apla是一种抽象算法描述语言,它具有高度抽象、表达力强等特点。Apla语言把树、图、集合、序列等组合数据类型作为预定义类型,并且含有明显的语法机制支持泛型程序设计和用户自定义ADT类型。相反,Object Pascal中不能直接使用树、图、集合、序列等组合类型。如何在Delphi中很好的支持Apla的这些机制是本论文所要研究的重点和难点,Apla--Delphi自动程序转换系统的目标是使得所有正确的Apla程序都能通过转换器得到正确的Delphi程序,并且能运行得到正确结果。该转换器的源语言是Apla,目标语言是Delphi编译器所使用的Object Pascal。本文所做的研究是PAR方法的重要组成部分。也是国家自然科学基金课题《实用的软件形式化方法及其开发工具研究》的重要组成部分。本项研究的主要目标是进一步的完善自动转换器中的部件库的内容。正确地实现Apla语言中的组合数据类型在Delphi中的实现。针对上述研究目标,本论文主要进行了以下工作:分析比较现有的形式化方法及其配套工具,并以PAR方法作为本文研究的理论基础。研究Apla语言中的泛型程序设计机制转换为Delphi语言程序的方法。研究Apla-Delphi转换器,实现Apla中的组合数据类型到Delphi中的具体实现。完善Apla-Delphi自动程序转换系统。进一步的工作包括完善Apla--Delphi自动程序转换系统的转换机制;提高Apla-Delphi自动程序转换系统的可靠性;增加Apla转换实例,使产品的商品化程度提高,可以进一步产品化并应用到实际的软件开发中去以促进软件产业的快速发展。