摘要：算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.

摘要：形式化方法有助于从根本上提高软件系统的质量与可靠性,但其开发成本往往过于高昂.一种折衷的办法是在软件系统中选取关键性部件进行形式化开发,但目前尚无非常有效的定量选择方法.将软件系统中的形式化开发关键部件选取建模为一个0-1约束规划问题,以便使用元启发式搜索方法对其进行优化求解.另外,针对该问题专门设计了一种离散水波优化(water wave optimization,简称WWO)算法.在一个大型软件系统上的应用验证了问题模型的有效性,同时证明了WWO算法相对于其他若干典型元启发式搜索方法的优越性.

摘要：泛型程序设计可大幅度提高程序的可重用性、可靠性和开发效率,高抽象的泛型机制则有助于降低泛型编程的复杂度.该文介绍了一种抽象泛型机制的核心思想和编程技术,分析了新型Java中与之对应的实现机理,并归纳出相应的转换规则,且在既有平台中实现了抽象泛型程序到新型Java泛型程序的自动转换和运行,最后通过一个Kleen算法实例,展示了抽象泛型机制的实际运用和相应Java程序的自动生成.抽象泛型机制的新型Java实现,在降低可重用算法构件的设计复杂度、提高算法构件可靠性的同时,也为泛型构件的设计和描述提供了行之有效的新途径.

摘要：泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率.泛型约束机制是对泛型参数进行形式描述,并对其合法性进行检测及验证,从而保证泛型程序的可靠性和安全性.分析总结多种主流语言的泛型约束特性,存在难以描述及验证基于动态语义的复杂约束需求问题,与完整实现GP尚有距离;以抽象程序设计语言Apla为宿主语言,提出了基于代数结构及公理语义的泛型约束方法,给出了基本数据类型、自定义抽象数据类型和子程序的3类泛型约束机制,拓展了泛型程序设计约束的应用范围.同时,支持静态语法和动态语义层约束,提高了泛型约束的精确度;借助Isabelle定理证明器,设计了泛型约束匹配检测和验证算法;进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型.实验部分给出了该泛型约束机制描述、检测及验证一系列复杂泛型约束问题的全过程,自动生成的C++模板程序的可靠性和安全性得到显著提高.

摘要：针对组合优化类问题定义了代数结构模型,从问题的形式规约出发,通过一阶谓词和量词演算将问题逐步简约为搜索空间更小、复杂度更低的子问题,根据问题的简约关系推导出求解算法,并在构造算法的同时也证明了算法的正确性.开发了原型系统以支持上述形式化的开发过程.这种算法推演技术能够显著提高算法程序设计的自动化水平,而问题简约的思想也更有利于对算法本质特征的理解.

摘要：形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率.

摘要：排序是计算机学科中的一类特殊问题,其算法设计策略的灵活性使得求解算法更具多样性.基于形式化方法 PAR(partition-and-recur),研究了排序算法的自动生成问题.刻画了排序问题的代数性质,形式化构建了排序算法领域的泛型类型构件和算法构件,建立了排序领域特定语言和算法生成形式化模型,以参数替换的方式自动生成了一组排序算法,包括快速排序、堆排序、Shell排序等典型的已知算法以及增量选择排序等若干未见于现有文献的算法,并在程序生成系统中予以了实现.通过上层框架研究和底层构件支持,显著提高了特定领域算法的开发效率和可靠性.

摘要：形式化软件规约技术是保证软件质量和提高软件生产率非常有用和重要的手段,但是形式化软件规约的获取是需求工程中一项相当困难的任务.本文针对问题需求自动化转换为形式化规约这个重要问题,研究从结构化需求语言SRL到形式化规约语言Radl自动生成系统及其高可靠性理论.为此,设计了一种受控自然语言-结构化需求语言SRL来描述问题需求;使用基于规则的方法,将结构化需求语言SRL通过分析-转换-综合三阶段生成为形式化软件规约Radl;在该方法的指导下,设计并实现了从结构化需求语言SRL到形式化软件规约Radl的生成系统SRLtoRadl;进一步,使用范畴论框架建立了SRLtoRadl生成系统生成过程的语义模型.实际效果表明该系统能有效的生成高质量形式化软件规约Radl.

摘要：从并发分布式程序设计的角度,对现有的并发分布式语言进行分析比较,选取Jayadev Misra教授近几年提出的全新结构化并发分布式语言Orc作为研究对象。通过深入分析Orc语言的基本原理和语言特征,提出了一个能够适合Apla抽象程序设计语言的并发分布式机制,设计了并发算子、并发语句、进程定义、进程通信和进程同步,并通过实例探讨了该设计方案的可行性和实用性,最后阐述了Apla语言中并发分布式机制具有通用性强、抽象层次高、简单易懂、便于并发分布式程序的开发等优点。

摘要：泛型程序设计通过从更高的层次对具体的算法和数据结构进行抽象,提高了软件的可扩展性、复用性和类型安全性,它主要是基于一系列自定义的类型约束而不是仅局限于预定义类型.该文对C++、Concepts C++、Java、C#以及Python等5种不同的、支持泛型程序设计的面向对象程序设计语言进行综合比较,并执行一个典型的且能够较好支持泛型编程机制的例子来分析这些面向对象语言的特征及对泛型编程机制的支撑程度,从而探寻泛型编程的本质特性,为减少程序开发的冗余、增强程序的可维护性提供参考.