循环不变式

作品数：51被引量：83H指数：5
导出分析报告
相关领域：自动化与计算机技术更多>>
相关作者：薛锦云杨庆红左正康石海鹤游珍更多>>
相关机构：江西师范大学中国科学院软件研究所中国科学技术大学南京大学更多>>
相关期刊：《计算机与数字工程》《计算机与现代化》《西北师范大学学报（自然科学版）》《福州大学学报（自然科学版）》更多>>
相关基金：国家自然科学基金江西省自然科学基金江西省教育厅科学技术研究项目国家重点基础研究发展计划更多>>
-
在结果中检索

检索结果分析

结果分析中...
共 条 记 录，以下是1-10
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
图广度优先遍历算法的形式化推导与机械验证方法
《江西师范大学学报(自然科学版)》2024年第5期472-478,共7页余楚凌 曹中雄 王唱唱 王昌晶 
江西省教育厅科学技术研究重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ220304)资助项目.
针对图广度优先遍历问题,该文提出了一种形式化推导与机械验证方法.首先,描述求解问题的形式化规约,使用分划递推得到统一的循环不变式并开发相应的Apla抽象程序;然后,在Isabelle中描述算法相关的数据类型、定义与基本函数,根据算法程...
关键词：图广度优先遍历 形式化推导 定理证明 循环不变式 
基于循环不变式的循环结构教学研究
《电脑知识与技术》2023年第6期121-122,143,共3页曹文平 谷琼 宁彬 
湖北文理学院教学研究项目(JY2022028)。
以梳理程序设计基础课程教学存在的问题为出发点,围绕循环结构教学内容,分析了逻辑思维和计算思维能力培养的必要性。文章从计算思维、逻辑思维、信息与数据的关系等方面剖析了循环结构教学内容的教学要点,设计了以循环不变式为基础的...
关键词：循环不变式 循环结构 计算思维 逻辑思维 程序设计 
基于数据分类的循环不变式自动生成
《计算机应用与软件》2023年第1期30-37,共8页路红 王承毅 黄皓 
江苏省高等学校自然科学研究面上项目(18KJB520022);江苏高校“青蓝工程”项目;南京理工大学紫金学院2021年度科研项目(2021ZRKX0401002);南京理工大学紫金学院2020年度科研项目(2020ZRKX0401001)。
生成循环不变式是实现程序验证的关键步骤,但人工撰写循环不变式不仅步骤繁琐且容易出错。为此,提出一种基于数据分类的循环不变式生成方法,可直接为C程序的循环语句自动生成循环不变式。该方法生成循环程序的后置条件,并构造其Hoare三...
关键词：循环不变式 数据分类 软件验证 静态分析 
面向深度学习算子的循环不变式外提算法
《计算机科学与探索》2023年第1期127-139,共13页梁佳利 华保健 吕雅帅 苏振宇 
中国科学技术大学研究生教育创新计划项目(2020ycjc41)。
TVM是一个深度学习编译器,支持将TVM的领域专用语言即张量表达式定义的算子编译生成目标平台的代码,并在高级中间表示TVM IR上进行一系列优化。张量表达式对算子执行循环变换,产生与循环迭代变量相关的复杂表达式的计算,在多层嵌套循环...
关键词：深度学习编译器 领域专用语言 循环不变量外提 中间表示 
二叉树队列关系问题非递归算法的推导及形式化证明被引量：2
《江西师范大学学报（自然科学版）》2022年第1期49-58,共10页左正康 方越 黄志鹏 黄箐 王昌晶 
国家自然科学基金(61862033,61902162);江西省教育厅科技重点课题(GJJ210307);江西省自然科学基金(20202BAB202015)资助项目.
该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类...
关键词：二叉树队列递推关系 循环不变式 Dijkstra-Gries标准程序证明法 Apla到C++程序自动生成系统 非线性数据结构 
图搜索问题算法推导及形式化证明
《江西师范大学学报（自然科学版）》2021年第6期642-651,共10页刘晓丹 胡颖 左正康 
国家自然科学基金(61862033,61762049,61902162);江西省教育厅科学技术研究(GJJ210307);江西省教育厅研究生创新基金(YC2021-S306);江西省自然科学基金(20202BABL202026,20202BABL202025,20202BAB202015)资助项目.
用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问...
关键词：图搜索问题 循环不变式 递归定义 形式化证明 
二叉树排序非递归算法推导及形式化证明被引量：6
《江西师范大学学报（自然科学版）》2020年第6期625-632,共8页左正康 方越 黄箐 廖云燕 王渊 王昌晶 
国家自然科学基金(61862033,61762049,61902162);江西省自然科学基金(20202BABL202026,2020BABL202025,20202BAB202015);国家留学基金(202008360094)资助项目.
非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变...
关键词：二叉树类非递归算法 循环不变式 PAR平台 Dijkstra-Gries标准程序证明法 非线性数据结构 
模型驱动的Dafny程序形式化生成与自动验证被引量：1
《江西师范大学学报（自然科学版）》2020年第4期378-384,共7页王昌晶 贺江飞 罗海梅 左正康 许帆 
国家自然科学基金(61762049,11804133,61862033);江西省科技厅课题(2020BABL202025,2020BABL202026,2018BAB206034)资助项目.
Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl...
关键词：模型驱动 Dafny程序 循环不变式 形式化生成 自动验证 
2类数列问题循环不变式开发策略研究与应用被引量：1
《江西师范大学学报（自然科学版）》2020年第3期307-312,共6页古素梅 杨庆红 
国家自然科学基金(61662035)资助项目.
该文通过对组合数学中Catalan数列问题和Fibonacci数列问题进行深入研究,利用归纳推理、组合数学中的加法和乘法原理等方法得到问题求解函数,使用变量记录算法求解过程中子问题的解,并约束循环变量的变化范围,获得问题求解算法的循环不...
关键词：数列问题 循环不变式 可信软件 归纳推理 
PAR平台中若干软件构件形式化验证技术研究被引量：8
《计算机工程与科学》2018年第2期268-274,共7页胡启敏 薛锦云 游珍 程着 
国家自然科学基金(61462041;61472167;61662036);江西省自然科学基金(20171BAB202008);江西省教育厅科技项目(160329)
PAR平台是本团队研制成功的支撑软件形式化和自动化开发的软件平台。该平台充分体现了功能抽象和数据抽象的优越性,使得软件开发变得便捷和可靠,达到这一性能的关键要素是一批可重用软件构件。为保证整个软件平台的正确性和可靠性,确保...
关键词：软件构件 形式语义 定理证明 PAR平台 循环不变式 
全选清除导出
共6页<123456>
检索报告 对象比较 聚类工具 使用帮助 返回顶部