期刊文献+
共找到31篇文章
< 1 2 >
每页显示 20 50 100
形式三角矩阵环的导子和自同构 被引量:13
1
作者 谢乐平 曹佑安 《数学杂志》 CSCD 北大核心 2006年第2期165-170,共6页
本文研究了形式上三角矩阵环Tri(A,M,B)的导子和自同构,利用与单位元相乘的方法,获得了形式上三角矩阵环Tri(A,M,B)的导子和自同构的结构形式.
关键词 形式上三角矩阵环 导子 自同构
下载PDF
逐步求精的一种模型 被引量:7
2
作者 钟珞 管昌生 +1 位作者 赵愚 潘昊 《武汉工业大学学报》 CSCD 1995年第3期52-57,共6页
提出一种支持程序开发的结构化方法.该方法以一种简单的问题分解策略为基础,比Wirth-Dijkstra的自顶向下逐步求精方法更利于面向目标的程序设计.由该方法可知,一个程序可经一系列求精而开发出来,每一步求精都能为相... 提出一种支持程序开发的结构化方法.该方法以一种简单的问题分解策略为基础,比Wirth-Dijkstra的自顶向下逐步求精方法更利于面向目标的程序设计.由该方法可知,一个程序可经一系列求精而开发出来,每一步求精都能为相应的最弱前置条件序列建立后置条件.这种策略使情况分析减少到极限,简化了结构化程序的证明,并保证了程序结构和数据结构之间的对应. 展开更多
关键词 面向目标 后置条件 软件开发 逐步求精
原文传递
形式化开发若干组合数学问题的算法 被引量:7
3
作者 石海鹤 石海鹏 薛锦云 《江西师范大学学报(自然科学版)》 CAS 北大核心 2006年第5期423-427,共5页
计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最... 计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最终可得到简洁、易理解、可靠性高的算法程序.对形式化方法开发组合算法做了积极的探索,有利于促进组合算法设计自动化的研究及形式化开发方法的推广应用. 展开更多
关键词 形式化推导 PAR方法 算法程序
下载PDF
若干算法程序的形式化推导与生成技术研究 被引量:7
4
作者 胡启敏 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2008年第z1期148-153,共6页
PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于... PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序. 展开更多
关键词 PAR方法 形式化推导 算法程序 递推关系
下载PDF
PAR平台从规约出发的算法推导与自动生成 被引量:5
5
作者 王昌晶 薛锦云 《计算机工程与应用》 CSCD 北大核心 2007年第2期41-42,59,共3页
简要介绍PAR方法及其支撑平台,使用PAR方法及其平台从规约出发形式化推导并生成了两个典型的算法程序。PAR方法及其平台使用一阶谓词逻辑表示功能规约,分划与递推来进行算法形式推导,各种转换系统来自动生成算法程序。这显著地提高了算... 简要介绍PAR方法及其支撑平台,使用PAR方法及其平台从规约出发形式化推导并生成了两个典型的算法程序。PAR方法及其平台使用一阶谓词逻辑表示功能规约,分划与递推来进行算法形式推导,各种转换系统来自动生成算法程序。这显著地提高了算法程序的正确性和开发效率,也有助于深刻地理解算法设计思想。 展开更多
关键词 PAR方法 PAR平台 规约 形式推导
下载PDF
基于算法框架的可重用部件设计与实现 被引量:2
6
作者 李云清 《计算机工程与应用》 CSCD 北大核心 2001年第23期136-138,156,共4页
对算法程序的功能规约进行等价变换,可以自然而且方便地得到求解问题设计思想的精确表达,即循环不变式。抽象算法又可以通过循环不变式获得。对算法程序中的算子进行提取、抽象就可以得到算法框架,而算法框架可以设计出可重用部件。文... 对算法程序的功能规约进行等价变换,可以自然而且方便地得到求解问题设计思想的精确表达,即循环不变式。抽象算法又可以通过循环不变式获得。对算法程序中的算子进行提取、抽象就可以得到算法框架,而算法框架可以设计出可重用部件。文章通过对数组段极值问题的求解,展示了形式化推导不仅可以得到正确、高效的算法程序,而且具有软件重用的功能,并进一步给出了利用可重用部件求解数组段极值问题的C++实现。 展开更多
关键词 循环不变式 算法结构 可重用部件 软件重用 软件工程 计算机
下载PDF
荷兰国旗问题的形式化推导及其多态性实现 被引量:3
7
作者 李云清 《计算机工程与设计》 CSCD 2002年第8期72-74,77,共4页
讨论了程序功能规约变换和算法程序的形式化技术。通过功能规约变换,可以较自然地获得问题求解的递推关系,对荷兰国旗问题的求解过程显示了形式化推导在获得高效和正确的算法程序中的作用。最后,给出了问题求解的多态性实现。
关键词 形式化技术 问题求解 算法 规约 程序功能 显示 变换 推导 递推关系 正确
下载PDF
最小生成树算法的PAR方法形式化推导 被引量:3
8
作者 孙凌宇 薛锦云 《计算机工程》 EI CAS CSCD 北大核心 2006年第21期85-87,共3页
采用PAR方法通过功能归约变换,形式化推导出可读性好、效率高的递推的最小生成树算法,简化了算法程序设计和正确性证明的过程,有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转... 采用PAR方法通过功能归约变换,形式化推导出可读性好、效率高的递推的最小生成树算法,简化了算法程序设计和正确性证明的过程,有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。 展开更多
关键词 PAR方法 形式化推导 归约变换 算法程序
下载PDF
算法形式化推导及其在软件重用中的应用 被引量:1
9
作者 李云清 《计算机工程》 CAS CSCD 北大核心 2003年第9期22-23,共2页
将形式化技术和软件复用结合是非常有意义的工作。利用规约进行变换,寻找递推关系,可以比较容易得到抽象算法。在变换中,尽可能地将有关操作抽象表示,将操作细节延迟,以适合现代软件工程的软件开发需要,对一个具体问题将得到包含... 将形式化技术和软件复用结合是非常有意义的工作。利用规约进行变换,寻找递推关系,可以比较容易得到抽象算法。在变换中,尽可能地将有关操作抽象表示,将操作细节延迟,以适合现代软件工程的软件开发需要,对一个具体问题将得到包含抽象操作的抽象算法。利用面向对象程序设计语言中的多态性等机制,将抽象操作用虚函数表示,如此设计的类可以作为可重用部件使用。 展开更多
关键词 形式化 软件重用 算法 多态性
下载PDF
PAR在数学算法中的应用 被引量:3
10
作者 杨晨 《电脑知识与技术》 2010年第3期1641-1644,共4页
针对算法走进高中课堂的现状,提出使用PAR作为高中学习算法开发的主要平台,通过PAR形式化推导实现多项式和素数两个经典数学问题,表明PAR具有良好的数学和程序设计语言透明性,得到算法简短易于理解的同时也可以同时保证算法的正确性,理... 针对算法走进高中课堂的现状,提出使用PAR作为高中学习算法开发的主要平台,通过PAR形式化推导实现多项式和素数两个经典数学问题,表明PAR具有良好的数学和程序设计语言透明性,得到算法简短易于理解的同时也可以同时保证算法的正确性,理论分析和试验表明,PAR是学习算法开发的一个有效平台。 展开更多
关键词 PAR方法 PAR平台 形式化推导 算法
下载PDF
算法的形式化推导与基于Isabelle的自动化验证 被引量:2
11
作者 齐蕾蕾 杨庆红 游颖 《江西师范大学学报(自然科学版)》 CAS 北大核心 2018年第4期379-383,共5页
可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化... 可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性. 展开更多
关键词 形式化方法 Isabelle定理证明器 自动化验证 形式化推导
下载PDF
分布式操作系统形式化生成系统模型的研究 被引量:2
12
作者 何炎祥 夏循斌 《小型微型计算机系统》 EI CSCD 北大核心 1995年第12期18-23,共6页
分布式操作系统形式化系统模型DOSFS主要由文法DOSFSG和语义DOSFSS两部分组成。其中文法部分采用了上下文无关文法,语义部分则是一个带操作集的语义系统。DOSFS按照抽象、描述、细化三个过程自动模拟生成分布式... 分布式操作系统形式化系统模型DOSFS主要由文法DOSFSG和语义DOSFSS两部分组成。其中文法部分采用了上下文无关文法,语义部分则是一个带操作集的语义系统。DOSFS按照抽象、描述、细化三个过程自动模拟生成分布式操作系统。本文主要介绍了文法DOSFSG的定义、性质,语义系统DOSFSS的设计思想、相关的数据结构、操作及其定义等。 展开更多
关键词 操作系统 形式语义 DOSFSS 分布式操作系统
下载PDF
三个经典数学问题的形式化开发 被引量:2
13
作者 杨晨 薛锦云 苏昭 《计算机与现代化》 2010年第8期1-4,共4页
计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台... 计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台,从待求解问题的精确功能描述出发,使用PAR方法和PAR平台的推理和变换规则,经过一系列等价变换,最后得到正确的算法程序。这一系列形式化推演的过程揭示了这3个经典数学问题的奥妙,事实说明PAR方法和PAR平台在算法程序设计过程中可以发挥更大的作用。 展开更多
关键词 PAR方法 PAR平台 形式化推导
下载PDF
一类0-1背包问题算法程序的形式化推导 被引量:2
14
作者 王昌晶 薛锦云 《武汉大学学报(理学版)》 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背包问题
原文传递
自洽法算复合材料有效性能重要公式的推导
15
作者 霍凯成 《武汉理工大学学报》 CAS CSCD 2001年第8期42-44,共3页
导出了文献 [4~ 6 ]中用自洽法计算弹性复合材料有效性能的修正的
关键词 复合材料 有效性能 自洽方法 Green公式 有效强性模量 平均场量控制方程
下载PDF
Formal Derivation of the Combinatorics Problems with PAR Method
16
作者 Lingyu SUN Yatian SUN 《Journal of Software Engineering and Applications》 2009年第3期195-199,共5页
Partition-and-Recur (PAR) method is a simple and useful formal method. It can be used to design and testify algo-rithmic programs. In this paper, we propose that PAR method is an effective formal method on solving com... Partition-and-Recur (PAR) method is a simple and useful formal method. It can be used to design and testify algo-rithmic programs. In this paper, we propose that PAR method is an effective formal method on solving combinatorics problems. Furthermore, we formally derive combinatorics problems by PAR method, which cannot only simplify the process of algorithmic program's designing, but also improve its automatization, standardization and correctness. We develop algorithms for two typical combinatorics problems, the number of string scheme and the number of error per-mutation scheme. Lastly, we obtain accurate C++ programs which are transformed by automatic transforming system of PAR platform. 展开更多
关键词 PAR Method formal derivation COMBINATORICS Algorithmic PROGRAMS
下载PDF
序列折半划分问题的形式化推导
17
作者 左正康 梁赞杨 +3 位作者 苏崴 黄箐 王渊 王昌晶 《计算机工程与科学》 CSCD 北大核心 2022年第6期1063-1071,共9页
形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列... 形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列折半划分问题的形式化推导方法。该方法基于分划递推的核心思想,应用规约变换技术对问题规约进行变换并严格保证一致性,使得在推导过程中无需交替证明,进而导出递推关系式并得到高可靠性抽象算法程序Apla,最终通过转换工具自动生成可执行程序。实现了从程序规约到具体可执行程序的完整程序求精过程。以2个序列算法为例,验证了该方法的有效性和可行性,对相关问题的形式化推导具有指导意义。 展开更多
关键词 折半划分 形式化推导 分划递推 程序求精
下载PDF
3个变形背包问题的形式化推导 被引量:1
18
作者 游颖 杨庆红 齐蕾蕾 《江西师范大学学报(自然科学版)》 CAS 北大核心 2017年第2期116-121,共6页
在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可... 在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可将采用的推导方法在子集和问题、船装载等问题中加以推广应用. 展开更多
关键词 形式化推导 0-1背包问题 二进制向量 程序规约 递推关系
下载PDF
Huffman算法程序的形式化推导 被引量:1
19
作者 王昌晶 罗海梅 +1 位作者 左正康 薛锦云 《计算机工程》 CAS CSCD 北大核心 2010年第5期49-51,共3页
使用PAR方法形式化推导了解决最优编码问题的Huffman算法。推导过程充分利用最优编码树的特性,在对原问题进行分划归约为子问题时,引入一个新元素来取代原来的2个或多个元素,使用一套接近数学语言的抽象记号表示集合、二叉树等,推导过... 使用PAR方法形式化推导了解决最优编码问题的Huffman算法。推导过程充分利用最优编码树的特性,在对原问题进行分划归约为子问题时,引入一个新元素来取代原来的2个或多个元素,使用一套接近数学语言的抽象记号表示集合、二叉树等,推导过程简洁且能生成正确的算法。该Huffman算法能在PAR平台上通过自动生成系统转换成可执行语言程序,并正常运行。 展开更多
关键词 PAR方法 形式化推导 最优编码 HUFFMAN算法
下载PDF
研究汉语韵母拼合顺序的形式化推导方法
20
作者 杨文波 《大连大学学报》 2012年第5期78-81,共4页
本文依照陆丙甫先生提出的形式化推导方法,对汉语普通话的韵母拼合顺序进行了探索,研究发现了韵母拼合顺序的优势序列和劣势序列,并用"音响顺序原则"进行了的解释。
关键词 普通话韵母 形式化推导 密集型因素归纳法 音响顺序原则
下载PDF
上一页 1 2 下一页 到第
使用帮助 返回顶部