形式化推导

作品数：23被引量：32H指数：3
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：薛锦云王昌晶杨庆红李云清胡启敏更多>>
相关机构：江西师范大学中国科学院软件研究所江西省高性能计算技术重点实验室中国科学院研究生院更多>>
相关期刊：《计算机工程与设计》《计算机与现代化》《武汉大学学报（理学版）》《江西师范大学学报（自然科学版）》更多>>
相关基金：国家自然科学基金江西师范大学青年成长基金国家重点基础研究发展计划江西省教育厅科学技术研究项目更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
图广度优先遍历算法的形式化推导与机械验证方法
《江西师范大学学报(自然科学版)》2024年第5期472-478,共7页余楚凌 曹中雄 王唱唱 王昌晶 
江西省教育厅科学技术研究重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ220304)资助项目.
针对图广度优先遍历问题,该文提出了一种形式化推导与机械验证方法.首先,描述求解问题的形式化规约,使用分划递推得到统一的循环不变式并开发相应的Apla抽象程序;然后,在Isabelle中描述算法相关的数据类型、定义与基本函数,根据算法程...
关键词：图广度优先遍历 形式化推导 定理证明 循环不变式 
序列折半划分问题的形式化推导
《计算机工程与科学》2022年第6期1063-1071,共9页左正康 梁赞杨 苏崴 黄箐 王渊 王昌晶 
国家自然科学基金(61862033,61902162);江西省自然科学基金(20202BABL202026,20202BABL202025,20202BAB202015);江西省教育厅科学技术重点研究项目(GJJ210307)。
形式化推导是在程序正确性证明理论下所进行的程序开发,最终得到完全正确的算法程序。针对序列折半划分问题,现有的形式化推导方法将推导与证明交替进行,推导过程繁琐且大多无法直接获得可执行程序。为解决上述问题,提出了一种新的序列...
关键词：折半划分 形式化推导 分划递推 程序求精 
2类组合数学问题的算法形式化推导被引量：1
《江西师范大学学报（自然科学版）》2019年第4期402-408,共7页熊小超 杨庆红 
国家自然科学基金(61662035)资助项目
组合数学问题算法的研究是计算机科学的重要研究内容,但在许多相关文献中,许多组合数学问题的算法只是经过简单分析得到,并未给出算法程序的详细设计过程,导致读者无法理解算法本质,更无法保证算法程序的正确性.该文在以组合数学中连续...
关键词：形式化方法 程序规约 组合数学 递推技术 
算法的形式化推导与基于Isabelle的自动化验证被引量：2
《江西师范大学学报（自然科学版）》2018年第4期379-383,共5页齐蕾蕾 杨庆红 游颖 
国家自然科学基金(61363013)资助项目
可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化...
关键词：形式化方法 Isabelle定理证明器 自动化验证 形式化推导 
3个变形背包问题的形式化推导被引量：1
《江西师范大学学报（自然科学版）》2017年第2期116-121,共6页游颖 杨庆红 齐蕾蕾 
国家自然科学基金(61363013)资助项目
在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可...
关键词：形式化推导 0-1背包问题 二进制向量 程序规约 递推关系 
循环结构的形式化推导被引量：1
《微型机与应用》2014年第5期82-83,86,共3页李贤贞 吴茂念 杨静 
国家自然科学基金项目(61262029)
介绍了Dijkstra的形式化推导方法的主要思想、步骤及要点。该方法主张程序开发和程序证明同时进行,先确定好描述程序功能的断言,再通过形式化方法推导出正确的程序。选择具有代表性的循环结构的实例进行推导证明,并对循环结构的形式化...
关键词：形式化方法 程序正确性 循环不变式 界函数 
有关PAR在数学算法之中的应用探析
《才智》2013年第14期182-182,共1页陆克盛 杨丽娜 李熙春 
目前在高中课堂中,算法的应用也比较多,本文主要提出PAR作为高中阶段对算法学习的基础平台,对素数及多项式两个经典数学问题通过PAR形式化推导进行实现,说明PAR具有较好的程序设计及数学语言的透明性,其算法简单,容易理解,很大程度上也...
关键词：PAR 方法 平台 数学算法 形式化推导 
研究汉语韵母拼合顺序的形式化推导方法
《大连大学学报》2012年第5期78-81,共4页杨文波 
本文依照陆丙甫先生提出的形式化推导方法,对汉语普通话的韵母拼合顺序进行了探索,研究发现了韵母拼合顺序的优势序列和劣势序列,并用"音响顺序原则"进行了的解释。
关键词：普通话韵母 形式化推导 密集型因素归纳法 音响顺序原则 
循环条件的形式化推导在程序验证中的应用被引量：1
《计算机工程与设计》2010年第14期3193-3197,共5页雷富兴 张来顺 石荣刚 杨科 
提出了一种求解命令式程序中循环执行和终止条件的方法。该方法基于循环代码本身进行循环执行和终止条件的分析推导,可以定义一个原型工具进行自动化推导。现有的形式化方法依赖于形式化规范,而提出的方法适用于未被形式化的程序。提出...
关键词：循环执行 循环终止 形式化方法 自动化 程序验证 缺陷修正 
三个经典数学问题的形式化开发被引量：2
《计算机与现代化》2010年第8期1-4,共4页杨晨 薛锦云 苏昭 
国家自然科学基金资助项目(60773054);科技部合作项目(2008DFA11940)
计算机科学最高奖图灵奖获得者Knuth指出,算法是计算机科学的核心。算法的设计和理解对开发高效、正确的软件至关重要。本文选取平方数问题、几何级数求和问题和多项式求值这3个经典数学问题,使用支持算法程序形式化的PAR方法和PAR平台...
关键词：PAR方法 PAR平台 形式化推导 
全选清除导出
共3页<123>
检索报告 对象比较 聚类工具 使用帮助 返回顶部