检索结果-南通市图书馆

图广度优先遍历算法的形式化推导与机械验证方法

在线全文

学校读者我要写书评

暂无评论

江西师范大学学报(自然科学版) 2024年

作者：余楚凌曹中雄王唱唱王昌晶江西师范大学数字产业学院江西师范大学计算机信息工程学院江西师范大学管理科学与工程研究中心

针对图广度优先遍历问题，该文提出了一种形式化推导与机械验证方法.首先，描述求解问题的形式化规约，使用分划递推得到统一的循环不变式并开发Apla抽象程序;然后，在Isabelle中描述算法相关的数据类型、定义与基本函数，根据算法程序... 详细信息

针对图广度优先遍历问题，该文提出了一种形式化推导与机械验证方法.首先，描述求解问题的形式化规约，使用分划递推得到统一的循环不变式并开发Apla抽象程序;然后，在Isabelle中描述算法相关的数据类型、定义与基本函数，根据算法程序正确性证明的验证条件，证明抽象算法正确;最后，通过Apla→C++自动生成器生成可执行代码，验证了该方法的有效性.

关键词：图广度优先遍历形式化推导定理证明循环不变式

在线全文

同方期刊数据库

学校读者我要写书评

暂无评论

3个变形背包问题的形式化推导

江西师范大学学报（自然科学版） 2017年第2期41卷 116-121页

作者：游颖杨庆红齐蕾蕾江西师范大学计算机信息工程学院江西南昌330022

在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可... 详细信息

在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可将采用的推导方法在子集和问题、船装载等问题中加以推广应用.

关键词：形式化推导 0-1背包问题二进制向量程序规约递推关系

算法的形式化推导与基于Isabelle的自动化验证

在线全文

学校读者我要写书评

暂无评论

江西师范大学学报（自然科学版） 2018年第4期42卷 379-383页

作者：齐蕾蕾杨庆红游颖江西师范大学计算机信息工程学院江西南昌330022

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化... 详细信息

可信软件的不断发展进一步推动了形式化方法的深入研究.结合实际应用中的2个问题,采用基于递推关系的算法形式化方法,演示了算法的形式化推导过程,并运用Isabelle定理证明器结合Dijkstra最弱前置谓词方法,对得到的算法程序进行了自动化验证,避免了手工验证过程繁琐和易出错等问题.研究表明:基于递推关系的算法形式化方法不仅可以提高开发算法的效率,而且通过数学变换保证推导过程的正确性,从而有效保证了算法和程序的正确性.

关键词：形式化方法 Isabelle定理证明器自动化验证形式化推导

算法的形式化推导与基于Isabelle的自动化验证

在线全文

学校读者我要写书评

暂无评论

算法的形式化推导与基于Isabelle的自动化验证

作者：齐蕾蕾江西师范大学

学位级别：硕士

可信软件的不断发展,进一步推动了形式化方法的深入研究。形式化方法具有严格的数学语言和精确的逻辑语义,从而保证软件在开发过程中的正确性。形式化方法主要包括形式化推导和形式化验证两个部分。形式化推导是通过对问题程序规约进行... 详细信息

可信软件的不断发展,进一步推动了形式化方法的深入研究。形式化方法具有严格的数学语言和精确的逻辑语义,从而保证软件在开发过程中的正确性。形式化方法主要包括形式化推导和形式化验证两个部分。形式化推导是通过对问题程序规约进行精确变换,最终得到算法程序。形式化验证是在对软件进行规约的基础上,验证软件是否具有所期望的性质。形式化方法对保证软件正确性和可靠性具有十分重要的意义。本文从形式化推导和自动化验证两方面研究提高算法程序正确性的有效途径。在形式化推导方面,采用基于递推技术的算法形式化方法开发算法程序,通过程序规约变换技术对形式化程序规约进行等价变换,得到问题求解的递推关系和循环不变式,以此为基础得到算法程序。该方法不仅清晰地展示了算法的设计思路与过程,而且有效保证了算法程序的正确性。在自动化验证方面,选择Isabelle定理证明器为工具。Isabelle传统应用领域为数学定理证明,本文结合验证需要在对其内置类型库和规则库进行扩充的基础上,探索将它应用于算法程序自动化验证以及问题求解序列递推关系自动化验证的有效方法。论文从三个层面深入剖析了Isabelle定理证明器,从三个部分展示了Isabelle的理论证明过程。结合本文两方面验证工作的需要,对Isabelle的类型库和规则库进行了扩充,完成了新添加规则的内部形式转换和正确性验证,以及新类型的嵌入;然后以此扩充的Isabelle类型库和规则库为基础,采用后推证明方式,结合Dijkstra最弱前置谓词方法,给出了算法程序自动化验证的基本流程,并对若干问题的算法程序进行了自动化验证;同时,为了避免手工推导递推关系带来的人为性错误,基于以上扩充的Isabelle规则库,对本文实例中推导得到的递推关系实现了进一步自动化验证。研究表明,上述工作有效提高了算法程序正确性证明和问题求解序列递推关系正确性验证的效率。

关键词：形式化推导自动化验证递推关系 Isabelle 证明规则库类型库

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

最小生成树算法的PAR方法形式化推导

计算机工程 2006年第21期32卷 85-87页

作者：孙凌宇薛锦云江西师范大学计算机信息工程学院

采用PAR方法通过功能归约变换,形式化推导出可读性好、效率高的递推的最小生成树算法,简化了算法程序设计和正确性证明的过程,有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转... 详细信息

采用PAR方法通过功能归约变换,形式化推导出可读性好、效率高的递推的最小生成树算法,简化了算法程序设计和正确性证明的过程,有效提高了算法程序设计自动化、规范化的程度及其正确性。该文给出的相关算法在PAR平台通过自动转换系统转换成可执行语言程序并运行通过。

关键词： PAR方法形式化推导归约变换算法程序

在线全文

学校读者我要写书评

暂无评论

一类0-1背包问题算法程序的形式化推导

武汉大学学报（理学版） 2009年第6期55卷 674-680页

作者：王昌晶薛锦云江西师范大学江西省高性能计算技术重点实验室江西南昌330022 中国科学院软件研究所北京100190 中国科学院研究生院北京100049

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背包问题

在线全文

学校读者我要写书评

暂无评论

Huffman算法程序的形式化推导

计算机工程 2010年第5期36卷 49-51页

作者：王昌晶罗海梅左正康薛锦云江西师范大学高性能计算技术重点实验室南昌330022 中国科学院软件研究所北京100190 中国科学院研究生院北京100190 江西师范大学物理与通讯电子学院南昌330022

使用PAR方法形式化推导了解决最优编码问题的Huffman算法。推导过程充分利用最优编码树的特性,在对原问题进行分划归约为子问题时,引入一个新元素来取代原来的2个或多个元素,使用一套接近数学语言的抽象记号表示集合、二叉树等,推导过... 详细信息

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

关键词： PAR方法形式化推导最优编码 Huffman算法

在线全文

学校读者我要写书评

暂无评论

若干算法程序的形式化推导与生成技术研究

计算机研究与发展 2008年第z1期45卷 148-153页

作者：胡启敏薛锦云中国科学院软件研究所计算机科学重点实验室江西师范大学瑶湖校区计算机信息工程学院南昌330022 江西省高性能计算技术重点实验室南昌330022

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于... 详细信息

PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序.

关键词： PAR方法形式化推导算法程序递推关系

在线全文

学校读者我要写书评

暂无评论

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

计算机应用研究 2008年第3期25卷 681-683页

作者：王昌晶薛锦云中国科学院软件研究所

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

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

关键词：分划递推方法形式化推导时间复杂度递归方程式