期刊文献+
共找到62篇文章
< 1 2 4 >
每页显示 20 50 100
基于PAR的算法形式化开发 被引量:28
1
作者 石海鹤 薛锦云 《计算机学报》 EI CSCD 北大核心 2009年第5期982-991,共10页
形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的... 形式化方法是构建可信软件的重要途径.基于对算法问题的分析,针对形式化方法PAR开发算法的特征,刻划了问题分划、递推关系构造方面的规律.从一类问题的形式化功能规约出发,可机械地完成问题的分划及规约的变换,自然地揭示出求解问题的算法思想,在相关工具的支持下自动生成算法程序.研究结果将算法设计中尽可能多的创造性劳动转化为非创造性劳动,降低了形式化求解算法问题的难度,提高了算法程序的可靠性和形式化开发效率. 展开更多
关键词 算法 形式化方法 par 规约 可信软件
下载PDF
温室透光覆盖材料透光特性的测试 被引量:23
2
作者 丁小明 周长吉 《农业工程学报》 EI CAS CSCD 北大核心 2008年第8期210-213,共4页
透光特性是温室透光覆盖材料的一个重要指标,其数值的表达却因测试方法的不同而有所差异。该文介绍了透光覆盖材料太阳辐射透过率的测试及计算方法,选用聚乙烯塑料膜(PE)、浮法玻璃、聚碳酸酯双层中空板(PC)三种典型的覆盖材料进行了测... 透光特性是温室透光覆盖材料的一个重要指标,其数值的表达却因测试方法的不同而有所差异。该文介绍了透光覆盖材料太阳辐射透过率的测试及计算方法,选用聚乙烯塑料膜(PE)、浮法玻璃、聚碳酸酯双层中空板(PC)三种典型的覆盖材料进行了测试,计算了国际照明委员会(CIE)规定的标准C、标准A和标准D65三种光源下,在可见光与PAR波段范围内,基于4种权重系数下的覆盖材料透光率和光合有效辐射(PAR)透过率。结果表明,PE薄膜几乎不受影响,浮法玻璃相差2%左右,聚碳酸酯双层中空板差异达2%~3.7%。 展开更多
关键词 温室覆盖材料 透光率 可见光 par 测试方法
下载PDF
基于PAR的排序算法自动生成研究 被引量:12
3
作者 石海鹤 薛锦云 《软件学报》 EI CSCD 北大核心 2012年第9期2248-2260,共13页
排序是计算机学科中的一类特殊问题,其算法设计策略的灵活性使得求解算法更具多样性.基于形式化方法 PAR(partition-and-recur),研究了排序算法的自动生成问题.刻画了排序问题的代数性质,形式化构建了排序算法领域的泛型类型构件和算法... 排序是计算机学科中的一类特殊问题,其算法设计策略的灵活性使得求解算法更具多样性.基于形式化方法 PAR(partition-and-recur),研究了排序算法的自动生成问题.刻画了排序问题的代数性质,形式化构建了排序算法领域的泛型类型构件和算法构件,建立了排序领域特定语言和算法生成形式化模型,以参数替换的方式自动生成了一组排序算法,包括快速排序、堆排序、Shell排序等典型的已知算法以及增量选择排序等若干未见于现有文献的算法,并在程序生成系统中予以了实现.通过上层框架研究和底层构件支持,显著提高了特定领域算法的开发效率和可靠性. 展开更多
关键词 排序算法 自动生成 领域特定语言 形式化模型 par.方法
下载PDF
循环不变式开发新策略及其应用 被引量:8
4
作者 石海鹤 肖正兴 薛锦云 《计算机工程与应用》 CSCD 北大核心 2006年第4期105-107,161,共4页
循环不变式体现了循环程序的本质特征,在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上,详细阐述了刻画循环不变式本质特征... 循环不变式体现了循环程序的本质特征,在算法程序的开发、证明和推导中具有十分重要的作用。而传统的循环不变式开发策略并没有很好地解决循环不变式开发难的问题。文章在阐述现有策略局限性的基础上,详细阐述了刻画循环不变式本质特征的新定义及基于此定义的开发循环不变式的新策略,并通过三个典型的实例,对开发新策略的具体应用作了比较深入的探索。 展开更多
关键词 循环不变式 算法程序 形式化方法 par方法
下载PDF
形式化开发若干组合数学问题的算法 被引量:7
5
作者 石海鹤 石海鹏 薛锦云 《江西师范大学学报(自然科学版)》 CAS 北大核心 2006年第5期423-427,共5页
计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最... 计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最终可得到简洁、易理解、可靠性高的算法程序.对形式化方法开发组合算法做了积极的探索,有利于促进组合算法设计自动化的研究及形式化开发方法的推广应用. 展开更多
关键词 形式化推导 par方法 算法程序
下载PDF
Radl算法到Apla程序的生成系统 被引量:10
6
作者 谢武平 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2014年第4期856-864,共9页
算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进... 算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率. 展开更多
关键词 par方法 Radl算法 程序生成 算法推导 生成规则
下载PDF
基于Isabelle定理证明器算法程序的形式化验证 被引量:9
7
作者 游珍 薛锦云 《计算机工程与科学》 CSCD 北大核心 2009年第10期85-89,共5页
形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序... 形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。 展开更多
关键词 形式化验证 定理机械证明 Dijkstra最弱前置谓词理论 par方法 算法程序 定理证明器
下载PDF
后序遍历二叉树非递归算法的推导及形式化证明 被引量:9
8
作者 左正康 游珍 薛锦云 《计算机工程与科学》 CSCD 北大核心 2010年第3期119-123,共5页
开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的... 开发涉及非线性数据结构算法程序的循环不变式一直是形式化方法的难点。本文使用PAR方法开发循环不变式的新策略,对后序遍历二叉树问题循环不变式的开发使用递归定义技术,得到了该问题循环不变式的简单精确的表达形式,简化了算法程序的推导和证明过程;利用PAR平台提供的抽象程序设计语言Ap1a中的数据抽象机制,使所得的算法程序结构简洁清晰且易于证明;最后,使用Dijkstra-Gries标准程序证明法形式证明了该问题的核心算法程序(只有4行代码),并使用PAR平台将Apla程序转换成正确的C++代码。实例的成功进一步说明PAR方法提供的循环不变式的开发技术对推导和证明非线性数据结构算法程序的有效性。 展开更多
关键词 后序遍历二叉树 循环不变式 par方法 非线性数据结构 Dijkstra-Gries标准程序证明法
下载PDF
Hanoi塔非递归算法的形式化推导和正确性验证 被引量:5
9
作者 游珍 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2008年第z1期143-147,共5页
关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法... 关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性. 展开更多
关键词 HANOI塔 par方法 循环不变式 非递归算法 Dijkstra最弱前置谓词法
下载PDF
若干算法程序的形式化推导与生成技术研究 被引量:7
10
作者 胡启敏 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2008年第z1期148-153,共6页
PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于... PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序. 展开更多
关键词 par方法 形式化推导 算法程序 递推关系
下载PDF
形式化开发Hanoi塔问题非递归算法 被引量:3
11
作者 石海鹤 石海鹏 薛锦云 《计算机工程与应用》 CSCD 北大核心 2007年第11期96-99,共4页
使用形式化方法PAR及循环不变式开发新策略,开发了Hanoi塔问题非递归算法,并对其进行了形式化的正确性证明。直接面向非递归算法,在得到求解Hanoi塔问题的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及... 使用形式化方法PAR及循环不变式开发新策略,开发了Hanoi塔问题非递归算法,并对其进行了形式化的正确性证明。直接面向非递归算法,在得到求解Hanoi塔问题的循环不变式的同时,直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发新策略开发非递归算法作了较深入的实践和探讨。 展开更多
关键词 HANOI塔问题 形式化方法 非递归 par方法 循环不变式
下载PDF
形式推导支持的递归程序向非递归程序的转换 被引量:5
12
作者 化志章 揭安全 +1 位作者 李云清 薛锦云 《计算机工程与科学》 CSCD 2007年第10期145-147,F0003,共4页
本文提出一种递归消除的方法,适于一类基于递归数据结构的程序。该方法将递归程序作为初始规约,以求解过程的状态变迁序列作迭代模式;通过数据展开和变换实现初始规约向基于序列描述规约的变换,继而用PAR形式推导出序列规约的递推关系,... 本文提出一种递归消除的方法,适于一类基于递归数据结构的程序。该方法将递归程序作为初始规约,以求解过程的状态变迁序列作迭代模式;通过数据展开和变换实现初始规约向基于序列描述规约的变换,继而用PAR形式推导出序列规约的递推关系,并以之为核心近乎机械地构造出非递归算法。树和图的两个算法实例说明了本方法的有效性。 展开更多
关键词 算法推导 形式方法 递归程序变换 par方法
下载PDF
循环不变式开发技术研究 被引量:5
13
作者 万松松 薛锦云 谢武平 《计算机工程与科学》 CSCD 北大核心 2010年第9期84-88,94,共6页
高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也... 高可靠性软件是当今软件开发的热点问题。确保算法程序逻辑结构正确最理想的途径是算法程序的形式化推导和证明,而循环不变式是算法程序形式推导和证明的关键。循环不变式的开发一直是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文研究了众多现有循环不变式开发方法中较为典型的几种方法,指出了它们的基本原理、技术难点、特点及效果,旨在探寻循环不变式本质特征,从而为研究更简单、有效的生成方法提出指导。 展开更多
关键词 循环不变式 par方法 高可靠性软件 谓词抽象
下载PDF
最小生成树算法的PAR方法形式化推导 被引量:3
14
作者 孙凌宇 薛锦云 《计算机工程》 EI CAS CSCD 北大核心 2006年第21期85-87,共3页
采用PAR方法通过功能归约变换,形式化推导出可读性好、效率高的递推的最小生成树算法,简化了算法程序设计和正确性证明的过程,有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转... 采用PAR方法通过功能归约变换,形式化推导出可读性好、效率高的递推的最小生成树算法,简化了算法程序设计和正确性证明的过程,有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。 展开更多
关键词 par方法 形式化推导 归约变换 算法程序
下载PDF
一种基于Apla-Java可重用部件库的并行(并发)程序开发方法 被引量:5
15
作者 揭安全 薛锦云 《微电子学与计算机》 CSCD 北大核心 2006年第9期165-167,170,共4页
介绍了一种基于Apla-Java可重用部件库并行(并发)程序的开发方法,包括Apla-Java可重用部件的设计策略以及部件库并行并发机制的实现方法。并通过一个并行计算的实例验证了Apla-Java可重用部件库应用于并行(并发)程序设计的正确性。
关键词 par方法 Apla—Java 可重用部件 并行 并发
下载PDF
面向PAR平台的测试用例生成技术研究 被引量:3
16
作者 杨乐 薛锦云 万韵 《微计算机信息》 2009年第33期204-205,122,共3页
测试用例的设计是软件测试中一个具有关键作用的工作,如何用较少的测试用例达到比较高的覆盖度,是需要解决的主要技术问题。本文结合现代软件测试技术中的数据驱动测试和结构驱动测试设计技术,根据PAR平台转换工具的实际测试情况,设计... 测试用例的设计是软件测试中一个具有关键作用的工作,如何用较少的测试用例达到比较高的覆盖度,是需要解决的主要技术问题。本文结合现代软件测试技术中的数据驱动测试和结构驱动测试设计技术,根据PAR平台转换工具的实际测试情况,设计了一种基于路径的测试用例自动生成算法,并在PAR平台的转换工具中应用实施,科学合理的测试用例设计为PAR平台转换工具测试的进行提供基础,测试达到了预期目的。 展开更多
关键词 par平台 par方法 测试用例 APLA→JAVA
下载PDF
基于Web Service和多媒体数据库技术的PAR方法在线自学系统的设计与实现 被引量:3
17
作者 熊小舟 薛锦云 《江西师范大学学报(自然科学版)》 CAS 北大核心 2018年第3期291-297,共7页
设计并实现了一个PAR方法的在线自学系统.利用Web服务(Web Service)和多媒体数据库技术,将使用PAR方法开发算法程序设计的基本概念、算法设计语言Radl、抽象程序设计语言Apla以及设计和推导算法程序的方法学形象生动地呈现给学习者.最... 设计并实现了一个PAR方法的在线自学系统.利用Web服务(Web Service)和多媒体数据库技术,将使用PAR方法开发算法程序设计的基本概念、算法设计语言Radl、抽象程序设计语言Apla以及设计和推导算法程序的方法学形象生动地呈现给学习者.最后介绍了利用算法程序设计支撑平台生成可执行算法程序的过程,以及该算法程序运行产生的结果. 展开更多
关键词 par方法 par平台 WEB服务 多媒体数据库技术
下载PDF
基于PAR方法的并行最大和算法的推导 被引量:2
18
作者 邓笋根 王明文 《江西师范大学学报(自然科学版)》 CAS 2001年第2期121-127,共7页
在基于薛锦云提出的PAR(Partition and Recursion)方法的思想上 ,通过并行划分数据空间———自然地称之为并行分划递推 ,给出了在PRAM和超立方互联网络模型上的并行最大和最优算法 ,它们的时间复杂性为O(logN) .
关键词 par方法 并行算法 算法设计 并行分划递推
下载PDF
一种形式化开发非递归算法的方法 被引量:3
19
作者 石海鹤 石海鹏 薛锦云 《计算机应用研究》 CSCD 北大核心 2007年第11期203-205,共3页
提出了一种简单、统一的形式化开发非递归算法的方法。该方法直接面向非递归算法,在形式化方法PAR的指导下,使用循环不变式的开发新策略,在得到求解递归问题的循环不变式的同时,能直接得到易读、高效且可靠的非递归算法,并通过一个具体... 提出了一种简单、统一的形式化开发非递归算法的方法。该方法直接面向非递归算法,在形式化方法PAR的指导下,使用循环不变式的开发新策略,在得到求解递归问题的循环不变式的同时,能直接得到易读、高效且可靠的非递归算法,并通过一个具体实例进行了阐述。对使用形式化方法及循环不变式开发新策略开发非递归算法的方法作了较深入的实践和探讨。 展开更多
关键词 形式化方法 非递归 par 循环不变式 可靠性
下载PDF
形式化方法在高中算法教学中的应用研究 被引量:3
20
作者 苏昭 薛锦云 杨晨 《计算机与现代化》 2010年第7期87-92,共6页
国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介... 国家教育部制定的高中新课程标准将算法初步作为高中数学课程的必修内容,算法与程序设计也首次纳入到选修课之列。全国大部分普通高中均按新课标开展教学实验,不少省份还把算法内容纳入高考。同时现有算法初步和算法与程序设计教材在介绍算法与算法设计方法时,无法说清楚算法设计的过程;在教学实践中,这一问题更加突出。这给高中生学习、理解及掌握算法和算法设计方法带来很大的困难。本文从新课程实验教材中及数学高考题中选取两个问题,用支持算法程序形式化开发的PAR(Partition And Recur)方法与PAR平台,从待求解问题的精确功能描述出发,经过一系列等价数学变换,最后得到正确的算法和程序。实践说明PAR方法与PAR平台可以在高中算法教学及学生能力评测中发挥建设性作用。 展开更多
关键词 可信软件 形式化方法 par方法
下载PDF
上一页 1 2 4 下一页 到第
使用帮助 返回顶部