Huffman算法程序的形式化推导

使用PAR方法形式化推导了解决最优编码问题的Huffman算法。推导过程充分利用最优编码树的特性,在对原问题进行分划归约为子问题时,引入一个新元素来取代原来的2个或多个元素,使用一套接近数学语言的抽象记号表示集合、二叉树等,推导过程简洁且能生成正确的算法。该Huffman算法能在PAR平台上通过自动生成系统转换成可执行语言程序,并正常运行。     

Radl算法到Apla程序的生成系统

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

若干算法程序的形式化推导与生成技术研究

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C 等可执行程序.     

PAR在数学算法中的应用

针对算法走进高中课堂的现状,提出使用PAR作为高中学习算法开发的主要平台,通过PAR形式化推导实现多项式和素数两个经典数学问题,表明PAR具有良好的数学和程序设计语言透明性,得到算法简短易于理解的同时也可以同时保证算法的正确性,理论分析和试验表明,PAR是学习算法开发的一个有效平台。     

三个经典数学问题的形式化开发

计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台,从待求解问题的精确功能描述出发,使用PAR方法和PAR平台的推理和变换规则,经过一系列等价变换,最后得到正确的算法程序。这一系列形式化推演的过程揭示了这3个经典数学问题的奥妙,事实说明PAR方法和PAR平台在算法程序设计过程中可以发挥更大的作用。     

形式推导支持的递归程序向非递归程序的转换

本文提出一种递归消除的方法,适于一类基于递归数据结构的程序。该方法将递归程序作为初始规约,以求解过程的状态变迁序列作迭代模式;通过数据展开和变换实现初始规约向基于序列描述规约的变换,继而用PAR形式推导出序列规约的递推关系,并以之为核心近乎机械地构造出非递归算法。树和图的两个算法实例说明了本方法的有效性。     

后序遍历二叉树非递归算法的推导及形式化证明

开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码。实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性。     

PAR方法和循环不变式的范畴语义

范畴论对理解程序规约及程序设计和正确性证明十分有用。PAR方法则是建立在严格的数学基础之上的一种统一的算法程序设计方法。循环不变式在循环算法程序的设计中至关重要。使用格理论和范畴论作为工具对PAR方法建立一个理论框架,并对其用范畴论的概念加以解释,从而使得PAR有更强的理论基础。在此基础上引入不动点原理深入刻划循环不变式的含义,循环不变式可以表示为谓词泛函的最小不动点,并从范畴论的角度解释该过程。     

最小生成树算法的PAR方法形式化推导

采用PAR方法通过功能归约变换，形式化推导出可读性好、效率高的递推的最小生成树算法，简化了算法程序设计和正确性证明的过程，有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。     

形式化方法在高中算法教学中的应用研究

国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介绍算法与算法设计方法时,无法说清楚算法设计的过程;在教学实践中,这一问题更加突出。这给高中生学习、理解及掌握算法和算法设计方法带来很大的困难。本文从新课程实验教材中及数学高考题中选取两个问题,用支持算法程序形式化开发的PAR（Partition And Recur）方法与PAR平台,从待求解问题的精确功能描述出发,经过一系列等价数学变换,最后得到正确的算法和程序。实践说明PAR方法与PAR平台可以在高中算法教学及学生能力评测中发挥建设性作用。     

基于PAR的算法形式化开发

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

基于Isabelle定理证明器算法程序的形式化验证

形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。     

基于PAR的软件服务外包开发过程应用研究

软件外包中开发效率低、可靠性差的问题一直存在。PAR（Partition and Recur）方法及高可靠软件开发平台PAR平台,在提高软件开发效率和可靠性方面能够发挥很好的作用。本文将PAR方法和PAR平台应用于外包软件开发过程,使用PAR平台成功研发中软国际实训教材中软件外包案例,在软件开发效率和可靠性方面取得显著效果。     

虚拟现实软件系统开发方法研究

虚拟现实技术是一门综合性技术,涉及计算机图形学、多媒体技术、人机交互和人工智能等多个领域,在教育、医疗、娱乐、军事等众多领域有非常广泛的应用。所有这些技术和应用最终都要靠计算机软件来实现,这就使得虚拟现实系统的软件变得十分庞大和复杂,涉及许多多媒体数据。传统软件开发方法和程序设计技术侧重于处理文本数据,显然不能满足开发虚拟现实软件的需要。试图以所在团队研发成功的PAR方法和PAR平台为基础,根据虚拟现实软件系统的特征,探寻虚拟现实软件系统开发的新方法,进一步扩充和完善PAR平台中已有多媒体处理技术、形式化建模技术和C#等高级语言程序自动生成系统。