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

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

PAR在数学算法中的应用

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

PAR平台从规约出发的算法推导与自动生成

简要介绍PAR方法及其支撑平台,使用PAR方法及其平台从规约出发形式化推导并生成了两个典型的算法程序。PAR方法及其平台使用一阶谓词逻辑表示功能规约,分划与递推来进行算法形式推导,各种转换系统来自动生成算法程序。这显著地提高了算法程序的正确性和开发效率,也有助于深刻地理解算法设计思想。     

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

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

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

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

算法及其时间复杂度可同步形式化推导的方法*

对在长期的算法研究中提出的PAR方法和PAR平台引入时间谓词加以扩展,不仅可以形式化推导出顺序查找和二分查找问题的算法程序,而且这两个问题关于时间复杂度的递归方程式也可同步且自然地推导得到.这为开发并验证高效率的算法开辟了一条新途径.     

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

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

一种高效的算法程序设计方法-PAR方法

利用在长期的算法研究中提出的分划递推法（简称PAR方法）开发了三个问题的算法程序,说明PAR方法不仅为算法设计提供了统一而有效的途径,也为开发循环不变式奠定了基础。     

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

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

Huffman算法程序的形式化推导

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

天课时分配下的多阶段新高考走班制排课算法

伴随新高考改革,高中排课过程需要考虑学生的科目选择。潜在的学生上课时间冲突提高了排出可行课表的难度,排课过程中对课表的复杂要求也更难得到满足。针对这些挑战提出一种多阶段优化算法解决高中“走班制”教学课程时间表优化问题。优化侧重点从课表时段分配转为天课时分配,即对每个课程班每天的课时数目进行决策。除需要满足课时不冲突的约束条件外,主要优化目标为“课时分布均匀”“教案平齐”“同时上课”。根据问题特点设计了三种课表变换算子用于在教学班天课时分配阶段提升新设计的爬山算法的寻优能力。在三组不同难度和规模的实验数据上,多阶段优化算法以高于85%的概率排出可行课表。相较大规模真实案例,人工生成案例和中规模真实案例在目标函数上得到较为理想的优化。整体课表的教案平齐违反主要源于行政班课表。发现同时上课的设置具有指导其他目标函数优化的能力。     

浅谈初中数学为何要进行数字化教学

《数学新课程标准》中指出初中数学课程的设计与执行应重视运用数字化教学模式,把数字化教学模式作为学生学习数学和解决问题的基本工具,主要要注意改变学生的学习模式,使学生将乐学并有更多的精力投入到现实的、创新性的数学学习中去。在日常教学中合理运用数字化技术以及网络技术,丰富课程资源,拓宽学生的视野,优化数学课堂教学,创设"探究、自主、协作"的课堂教学模式,提高数学课堂教学效率,实现与数字化技术的整合已成为我们当前数学教师必须掌握的一种教学模式。而如何将数字化技术有效的运用到数学教学中,如何将数字化技术与数学教学有效的整合起来等众多急需解决的问题。     

智能搜索算法教学软件的设计与开发

为提高人工智能导论课程的教学质量,协调好教与学的双边关系,结合教学实践,在Microsoft Visual Studio2005环境中用C++语言开发了智能搜索算法的教学软件,设计了A*算法、模拟退火算法和遗传算法的演示程序和验证程序,提供了这些算法的核心代码,方便学生开展各算法的自主实验设计。     

形式化开发Hanoi塔问题非递归算法

使用形式化方法PAR及循环不变式开发新策略,开发了Hanoi塔问题非递归算法,并对其进行了形式化地正确性证明。本文直接面向非递归算法,在得到求解Hanoi塔问题的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发新策略开发非递归算法作了较深入的实践和探讨。     

单元制教学专业混合排课算法的设计与实现

排课问题是典型的组合优化和不确定性调度问题,以往排课算法的研究通常将合班课程及单元制教学课程排除在外。根据单元制教学的特殊性,详细描述单元制排课问题,提出一种有效解决单元制教学排课问题的算法,并加以实现。将该算法应用于上海出版印刷高等专科学校艺术系课程表编排,试验结果验证了算法的有效性,为教学管理工作提供了有效的技术手段。     

继续教育学院排课算法的研究与应用

针对教学管理中手工排课难的问题，我们设计了排课算法。在设计排课算法中，我们主要用数学集合的思想来讨论存在的问题，然后采用回溯算法设计出算法的流程，最后再采用链表的结构加于实现，并给出了核心算法的伪代码。     

一种形式化开发非递归算法的方法*

提出了一种简单、统一的形式化开发非递归算法的方法.该方法直接面向非递归算法,在形式化方法PAR的指导下,使用循环不变式的开发新策略,在得到求解递归问题的循环不变式的同时,能直接得到易读、高效且可靠的非递归算法,并通过一个具体实例进行了阐述.对使用形式化方法及循环不变式开发新策略开发非递归算法的方法作了较深入的实践和探讨.     

工业设计专业CAD课程设置与教学方法改革探索

计算机辅助设计是当前工业设计专业教学的重要内容,根据工业设计CAD课程教学的目标,针对当前课程设置和教学中的问题,提出了通过构建模块化CAD课程,将CAD教学贯穿到设计实践中,并采用连续性的教学进程来构建新的课程体系;在教学中采用突出思维方法的归类,注重CAD对设计要素的表达,以设计任务驱动的CAD学习等教学方法来提高学生利用计算机设计的能力和持续学习CAD的能力。     

Hanoi塔非递归算法的形式化推导和正确性验证

关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.