期刊文献+
共找到20篇文章
< 1 >
每页显示 20 50 100
Apla中泛型约束机制研究 被引量:13
1
作者 左正康 薛锦云 《软件学报》 EI CSCD 北大核心 2015年第6期1340-1355,共16页
泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率.泛型约束机制是对泛型参数进行形式描述,并对其合法性进行检测及验证,从而保证泛型程序的可靠性和安全性.分析总结多种主流语言的泛型约束特性,存在难以描述及验证基于动态语... 泛型程序设计可大幅提高程序的可重用性、可靠性和开发效率.泛型约束机制是对泛型参数进行形式描述,并对其合法性进行检测及验证,从而保证泛型程序的可靠性和安全性.分析总结多种主流语言的泛型约束特性,存在难以描述及验证基于动态语义的复杂约束需求问题,与完整实现GP尚有距离;以抽象程序设计语言Apla为宿主语言,提出了基于代数结构及公理语义的泛型约束方法,给出了基本数据类型、自定义抽象数据类型和子程序的3类泛型约束机制,拓展了泛型程序设计约束的应用范围.同时,支持静态语法和动态语义层约束,提高了泛型约束的精确度;借助Isabelle定理证明器,设计了泛型约束匹配检测和验证算法;进一步设计了泛型约束机制在PAR平台的实现方案及其系统原型.实验部分给出了该泛型约束机制描述、检测及验证一系列复杂泛型约束问题的全过程,自动生成的C++模板程序的可靠性和安全性得到显著提高. 展开更多
关键词 泛型约束机制 APLA语言 代数结构 动态语义约束 安全性
下载PDF
虚拟现实软件系统开发方法研究 被引量:13
2
作者 周哲泓 薛锦云 黄捷文 《计算机工程与科学》 CSCD 北大核心 2019年第11期1968-1975,共8页
虚拟现实技术是一门综合性技术,涉及计算机图形学、多媒体技术、人机交互和人工智能等多个领域,在教育、医疗、娱乐、军事等众多领域有非常广泛的应用。所有这些技术和应用最终都要靠计算机软件来实现,这就使得虚拟现实系统的软件变得... 虚拟现实技术是一门综合性技术,涉及计算机图形学、多媒体技术、人机交互和人工智能等多个领域,在教育、医疗、娱乐、军事等众多领域有非常广泛的应用。所有这些技术和应用最终都要靠计算机软件来实现,这就使得虚拟现实系统的软件变得十分庞大和复杂,涉及许多多媒体数据。传统软件开发方法和程序设计技术侧重于处理文本数据,显然不能满足开发虚拟现实软件的需要。试图以所在团队研发成功的PAR方法和PAR平台为基础,根据虚拟现实软件系统的特征,探寻虚拟现实软件系统开发的新方法,进一步扩充和完善PAR平台中已有多媒体处理技术、形式化建模技术和C#等高级语言程序自动生成系统。 展开更多
关键词 虚拟现实 PAR平台 程序自动生成 C#语言
下载PDF
PAR平台中若干软件构件形式化验证技术研究 被引量:8
3
作者 胡启敏 薛锦云 +1 位作者 游珍 程着 《计算机工程与科学》 CSCD 北大核心 2018年第2期268-274,共7页
PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保... PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保其中软件构件的正确性和可靠性就显得十分重要。选取PAR平台中若干典型软件构件,用形式化方法对构件的语义进行形式化描述,并借助Coq定理证明系统,对构件的正确性进行形式化验证,大幅度提高了软件构件形式化验证的效率。 展开更多
关键词 软件构件 形式语义 定理证明 PAR平台 循环不变式
下载PDF
Hanoi塔非递归算法的形式化推导和正确性验证 被引量:5
4
作者 游珍 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2008年第z1期143-147,共5页
关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法... 关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性. 展开更多
关键词 HANOI塔 PAR方法 循环不变式 非递归算法 Dijkstra最弱前置谓词法
下载PDF
若干算法程序的形式化推导与生成技术研究 被引量:7
5
作者 胡启敏 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2008年第z1期148-153,共6页
PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于... PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序. 展开更多
关键词 PAR方法 形式化推导 算法程序 递推关系
下载PDF
多核集群系统上的混合编程模型研究 被引量:4
6
作者 张军 万剑怡 《计算机与现代化》 2009年第5期1-4,共4页
对采用多核处理器作为SMP集群系统的计算节点的系统上的一种混合编程模型─MPI+OpenMP混合编程模型进行了深入的研究。建立了两个矩阵乘的混合并行算法,在多核集群平台上与纯MPI算法分别进行了实验,并进行了性能方面的比较。试验表明,... 对采用多核处理器作为SMP集群系统的计算节点的系统上的一种混合编程模型─MPI+OpenMP混合编程模型进行了深入的研究。建立了两个矩阵乘的混合并行算法,在多核集群平台上与纯MPI算法分别进行了实验,并进行了性能方面的比较。试验表明,混合编程具有更好的性能。 展开更多
关键词 多核集群 混合编程模型 矩阵乘
下载PDF
一种基于Apla-Java可重用部件库的并行(并发)程序开发方法 被引量:5
7
作者 揭安全 薛锦云 《微电子学与计算机》 CSCD 北大核心 2006年第9期165-167,170,共4页
介绍了一种基于Apla-Java可重用部件库并行(并发)程序的开发方法,包括Apla-Java可重用部件的设计策略以及部件库并行并发机制的实现方法。并通过一个并行计算的实例验证了Apla-Java可重用部件库应用于并行(并发)程序设计的正确性。
关键词 PAR方法 Apla—Java 可重用部件 并行 并发
下载PDF
泛型编程扩展及其JAVA实现 被引量:4
8
作者 徐文胜 薛锦云 《计算机工程与科学》 CSCD 2007年第10期89-91,94,共4页
本文对泛型编程的核心思想和技术特征进行了较为深入的分析,介绍了泛型编程在语言实现上的现状与不足,着重论述了作者针对这些不足做出的改进工作,即对类型参数及其约束机制进行扩展以支持通用、高效的算法和数据结构的设计,并以Java语... 本文对泛型编程的核心思想和技术特征进行了较为深入的分析,介绍了泛型编程在语言实现上的现状与不足,着重论述了作者针对这些不足做出的改进工作,即对类型参数及其约束机制进行扩展以支持通用、高效的算法和数据结构的设计,并以Java语言作为实施例,详细介绍了如何通过现有对象技术来实现比较完整的泛型编程,是现有面向对象语言类泛型编程的首例。 展开更多
关键词 泛型编程 面向对象语言 类型参数 约束机制
下载PDF
并行遗传算法骨架的研究和实现 被引量:2
9
作者 朱咸坤 万剑怡 《计算机工程与设计》 CSCD 北大核心 2009年第20期4588-4591,共4页
通过对并行遗传算法的4种并行模型和基于骨架的编程模型的对比研究,设计并实现了一个并行遗传算法骨架,用以简化并行遗传算法应用程序的开发过程。透明的并行机制,使得用户只需编写个体适应度函数的顺序程序,再调用该算法骨架就可以完... 通过对并行遗传算法的4种并行模型和基于骨架的编程模型的对比研究,设计并实现了一个并行遗传算法骨架,用以简化并行遗传算法应用程序的开发过程。透明的并行机制,使得用户只需编写个体适应度函数的顺序程序,再调用该算法骨架就可以完成并行遗传算法程序开发;开放的算法骨架结构,可以吸收遗传算法研究领域众多优秀成熟的改进算法;多种编码方式的支持为用户提供的更自由的选择空间。该算法骨架通过调用现有的结构骨架实现具体的并行,从而与并行计算平台相独立,具有很高的重用性和灵活性。 展开更多
关键词 并行模型 结构骨架 并行遗传算法骨架 透明机制 加速比
下载PDF
软件模型检测新技术研究 被引量:3
10
作者 化志章 吴传孙 +1 位作者 揭安全 薛锦云 《微计算机信息》 北大核心 2007年第36期250-251,311,共3页
软件模型检测以其潜在的商业价值一直为学术界和工业界关注.本文通过剖析模型检测工具SLAM,探讨软件模型检测的机理、方法及若干核心技术,并总结出软件模型检测的一些新策略.
关键词 软件模型检测 形式验证 SLAM
下载PDF
基于骨架的结构化网格编程模型 被引量:3
11
作者 钟旭 万剑怡 万红艳 《计算机工程》 CAS CSCD 北大核心 2010年第2期266-268,271,共4页
为了解决网格编程中可编程性和性能之间的冲突,提出一种基于骨架的结构化网格编程模型。将结构骨架的性能预测模型引入到网格编程的早期阶段,使用远程求值的机制进行结构骨架参数的远程传递。实验结果证明,该模型可克服传统方法引起的... 为了解决网格编程中可编程性和性能之间的冲突,提出一种基于骨架的结构化网格编程模型。将结构骨架的性能预测模型引入到网格编程的早期阶段,使用远程求值的机制进行结构骨架参数的远程传递。实验结果证明,该模型可克服传统方法引起的性能问题,且能有效提高网格软件的开发效率和可重用性。 展开更多
关键词 可重用性 网格 结构骨架 性能预测
下载PDF
一种离焦模糊图像客观检测的新方法 被引量:3
12
作者 王正友 伍世虔 +4 位作者 徐升华 万常选 方志军 肖文 曾卫明 《中国图象图形学报》 CSCD 北大核心 2007年第6期1008-1013,共6页
为了更精确地进行离焦模糊图像检测,提出了一种针对一幅图的离焦模糊图像客观检测的新方法,其核心思想是由线扩展函数(LSF)得到离焦模糊图像的点扩展函数(PSF)。该方法首先假定图像中至少能检测到一条明显边缘,然后由此边缘构造LSF。由... 为了更精确地进行离焦模糊图像检测,提出了一种针对一幅图的离焦模糊图像客观检测的新方法,其核心思想是由线扩展函数(LSF)得到离焦模糊图像的点扩展函数(PSF)。该方法首先假定图像中至少能检测到一条明显边缘,然后由此边缘构造LSF。由于作用于空间域,无需复杂的傅里叶变换或迭代运算,因此该方法速度很快。此外,为使检测方法更具普遍性,还提出了离焦模糊检测的一般准则,这种准则适用于所有图像而不依赖于图像的内容。实验结果验证了该方法的精确性和有效性。 展开更多
关键词 离焦 点扩散函数 线扩散函数 模糊检测 边缘检测
下载PDF
一种自动的形式化验证技术——模型检测
13
作者 化志章 揭安全 薛锦云 《微计算机信息》 北大核心 2007年第33期254-256,222,共4页
模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比... 模型检测是针对有限状态系统行为的逻辑性质的一种自动验证技术,已有许多工业应用.其主要缺陷是空间爆炸问题.本文通过一简单实例介绍其基本思想、检测步骤和相关理论,给出一些处理状态空间爆炸问题的优化技术,并与其它验证方法进行了比较,最后简单介绍了软件模型检测的新进展. 展开更多
关键词 模型检测 形式验证 时态逻辑
下载PDF
关系代数派生算子语义表达式间等价性证明 被引量:2
14
作者 杨波 薛锦云 《计算机科学与探索》 CSCD 2008年第1期97-103,共7页
关系代数的派生算子在关系数据库查询语言中得到了广泛应用。它们的语义有两种常见的表示方式,一种是基于原始算子的表达式,一种是基于一阶逻辑的表达式。但有关的文献资料都没有给出这两种表达式等价性的严格证明。文章尝试通过一系列... 关系代数的派生算子在关系数据库查询语言中得到了广泛应用。它们的语义有两种常见的表示方式,一种是基于原始算子的表达式,一种是基于一阶逻辑的表达式。但有关的文献资料都没有给出这两种表达式等价性的严格证明。文章尝试通过一系列等价变换,证明派生算子语义的这两种表达式间的等价性。从派生算子(主要是除算子)语义的原始算子表达式出发,根据关系代数表达式的特点,通过一步步的等价变换,得到派生算子语义的一阶逻辑表达式。所使用的变换方法能为关系代数表达式的正确性证明打下基础。 展开更多
关键词 关系代数的派生算子 原始算子 一阶逻辑 除算子 等价变换
下载PDF
XML在并行骨架描述中的应用
15
作者 许淳 万剑怡 延飞波 《计算机与现代化》 2009年第5期51-53,56,共4页
在对并行骨架的思想、描述和应用进行深入研究的基础上,本文提出了一种基于XML的并行骨架描述方法,为基于骨架的并行编程系统中各种骨架描述提供了一种统一的处理模型,对提高并行骨架库的通用性、可扩展性和可移植性具有重要意义。
关键词 并行骨架 算法骨架 结构骨架 XML
下载PDF
Radl算法到Apla程序的生成系统 被引量:10
16
作者 谢武平 薛锦云 《计算机研究与发展》 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
一类单元赋值语句型循环不变式的开发方法研究 被引量:4
17
作者 杨黄磊 薛锦云 《江西师范大学学报(自然科学版)》 CAS 北大核心 2014年第4期378-382,共5页
依据现有循环不变式的定义和开发策略,阐述了一类单元赋值语句型循环不变式开发方法,同时使用Dijkstra最弱前置谓词方法确认了循环不变式的正确性.最后通过典型实例来说明该方法的应用.
关键词 单元赋值语句 循环不变式 开发策略 最弱前置谓词方法
下载PDF
安全信息管理系统生成器的研究 被引量:2
18
作者 张俊贤 《计算机与现代化》 2009年第11期92-95,共4页
基于生成式程序设计和领域工程的理论与方法对运行于PDA的安全类软件进行建模,本文介绍一种简单的领域建模语言GML,设计一个生成器解析GML文档并生成目标系统。
关键词 生成式程序设计 领域工程 GML语言 安全管理信息系统生成器
下载PDF
一类0-1背包问题算法程序的形式化推导 被引量:2
19
作者 王昌晶 薛锦云 《武汉大学学报(理学版)》 CAS CSCD 北大核心 2009年第6期674-680,共7页
0-1背包问题是经典的组合优化问题与NP完全问题,具有重要的应用价值与理论意义.本文使用PAR(Partition and Recurrence)方法形式化推导了0-1背包问题的高效动态规划算法程序.通过类比分析,该问题的若干变形问题的算法也可推导得到,算法... 0-1背包问题是经典的组合优化问题与NP完全问题,具有重要的应用价值与理论意义.本文使用PAR(Partition and Recurrence)方法形式化推导了0-1背包问题的高效动态规划算法程序.通过类比分析,该问题的若干变形问题的算法也可推导得到,算法通过PAR平台的自动生成系统转换成可执行语言程序并运行通过,保证了该类0-1背包问题算法的正确性和可靠性.本文主要的贡献是将PAR方法推广到能处理带约束条件的组合优化类问题,大大扩展了PAR方法的应用范围,为形式化开发高效高可信组合优化类算法开辟了一条新途径. 展开更多
关键词 形式化推导 高可信 组合优化 0-1背包问题
原文传递
PAR平台数据库查询优化方案 被引量:1
20
作者 汤沁 薛锦云 《计算机与现代化》 2013年第11期58-60,共3页
数据库系统的查询优化技术是提高数据库系统效率的重要技术。当今Java和C++等主流程序设计语言依靠SQL语句,造成数据库系统中查询复杂、繁琐、效率低下、可靠性得不到保证等。针对上述问题,在PAR(Partition And Recur)平台数据库关系代... 数据库系统的查询优化技术是提高数据库系统效率的重要技术。当今Java和C++等主流程序设计语言依靠SQL语句,造成数据库系统中查询复杂、繁琐、效率低下、可靠性得不到保证等。针对上述问题,在PAR(Partition And Recur)平台数据库关系代数实现机制基础上,提出和实现基于关系代数的查询优化规则设计方法。这种设计不仅提高了数据库查询效率,也为高可靠数据库的形式化开发提供了依据。 展开更多
关键词 查询优化 关系代数 PAR平台
下载PDF
上一页 1 下一页 到第
使用帮助 返回顶部