[1]古素梅,杨庆红*.2类数列问题循环不变式开发策略研究与应用[J].江西师范大学学报(自然科学版),2020,(03):307-312.[doi:10.16357/j.cnki.issn1000-5862.2020.03.15]
　GU Sumei,YANG Qinghong*.The Research and Application of Loop Invariant Development Strategy for Two Kinds of Sequence Problems[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(03):307-312.[doi:10.16357/j.cnki.issn1000-5862.2020.03.15]
点击复制

2类数列问题循环不变式开发策略研究与应用()
分享到：

《江西师范大学学报》（自然科学版）[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2020年03期
页码:
307-312
栏目:
信息科学与技术
出版日期:
2020-06-10

文章信息/Info

Title:
The Research and Application of Loop Invariant Development Strategy for Two Kinds of Sequence Problems
文章编号:
1000-5862(2020)03-0307-06
作者:
古素梅; 杨庆红*
江西师范大学计算机信息工程学院,江西 南昌 330022
Author(s):
GU Sumei; YANG Qinghong*
College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
数列问题;  循环不变式;  可信软件;  归纳推理
Keywords:
sequence problem;  loop invariant;  trustworthy software;  inductive reasoning
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2020.03.15
文献标志码:
A
摘要:
该文通过对组合数学中Catalan数列问题和Fibonacci数列问题进行深入研究,利用归纳推理、组合数学中的加法和乘法原理等方法得到问题求解函数,使用变量记录算法求解过程中子问题的解,并约束循环变量的变化范围,获得问题求解算法的循环不变式,由此得到了2类数列问题循环不变式的统一开发策略.以二叉树的形态数问题和阶梯问题为例,利用所提策略开发循环不变式,并基于循环不变式展示了这2类数列问题算法程序的形式化推导过程.
Abstract:
Based on the combination of mathematics in the Catalan sequence and the Fibonacci sequence problems in-depth study,using the method of inductive reasoning,and the methods of addition and multiplication principle of combinatorial mathematics problem solving function,the variable problem of neutron log algorithm process of solution and the change of constraint loop variable range are used,the loop invariant of problem solving algorithm is obtained,giving the problem of two kinds of sequence loop invariant of the unification of the development strategy.Taking binary tree morphological number problem and ladder problem as examples,the proposed strategy is used to develop loop invariants.

参考文献/References:

[1] 万松松,薛锦云,谢武平.循环不变式开发技术研究[J].计算机工程与科学,2010,32(9):84-88,94.
[2] 刘自恒,曾庆凯.一种自适应的循环不变式生成方法[J].计算机工程,2013,39(6):76-81.
[3] 王晓东,吴英杰,傅仰耿,等.算法归纳设计策略与循环不变式[J].福州大学学报:自然科学版,2004,32(4):387-392.
[4] 杨黄磊,薛锦云.一类单元赋值语句型循环不变式的开发方法研究[J].江西师范大学学报:自然科学版,2014,38(4):378-382.
[5] 潘建东,陈立前,黄达明,等.含有析取语义循环的不变式生成改进方法[J].软件学报,2016,27(7):1741-1756.
[6] 许欢,王以松.用daikon发现循环不变式[J].贵州大学学报:自然科学版,2012,29(4):77-81.
[7] Gries D.A note on a standard strategy for developing loop invariants and loops[J].Science of Compute Programming,1982,2(3):207-214.
[8] 黄小明.循环不变式自动探测[D].南昌:江西师范大学,2017.[9] Zhai Juan,Wang Hanfei,Zhao Jianhua.Post-condition-directed invariant inference for loops over data structures[EB/OL].[2019-05-11].https://ieeexplore.ieee.org/document/6901659.
[10] 王树义,邹伟松,刘恒.基于知识的循环不变式生成方法[C]∥中国计算机学会.2001全国软件技术研讨会论文集.大连:大连出版社,2001:38-40.
[11] 李彬,翟娟,汤震浩,等.自动合成数组不变式[J].软件学报,2018,29(6):1544-1565.
[12] Hou Chunyan,Wang Jinsong,Chen Chen,et al.Loop invariant generation for non-monotone loop structures[EB/OL].[2019-05-11].https://www.researchgate.net/publication/326103698_Loop_Invariant_Generation_for_Non-monotone_Loop_Structures.
[13] Janota M.Assertion-based loop invariant generation[EB/OL].[2019-05-11].http://hdl.handle.net/10344/2127.
[14] Xue Jinyun.Two new strategies for developing loop invariants and their applications[J].Journal of Computer Science and Technology,1993,8(2):147-154.
[15] 游颖.算法形式化方法在3类组合数学问题求解中的应用研究[D].南昌:江西师范大学,2017.

相似文献/References:

[1]王昌晶,贺江飞,罗海梅,等.模型驱动的Dafny程序形式化生成与自动验证[J].江西师范大学学报(自然科学版),2020,(04):378.[doi:10.16357/j.cnki.issn1000-5862.2020.04.09]
　WANG Changjing,HE Jiangfei,LUO Haimei,et al.The Model-Driven Dafny Program Generation and Automatic Verification[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(03):378.[doi:10.16357/j.cnki.issn1000-5862.2020.04.09]
[2]左正康,方 越,黄 箐,等.二叉树排序非递归算法推导及形式化证明[J].江西师范大学学报(自然科学版),2020,(06):625.[doi:10.16357/j.cnki.issn1000-5862.2020.06.14]
　ZUO Zhengkang,FANG Yue,HUANG Qing,et al.The Derivation and Formal Proof of Binary Tree Sorting Non-Recursive Algorithm[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(03):625.[doi:10.16357/j.cnki.issn1000-5862.2020.06.14]
[3]刘晓丹,胡 颖,左正康*.图搜索问题算法推导及形式化证明[J].江西师范大学学报(自然科学版),2021,(06):642.[doi:10.16357/j.cnki.issn1000-5862.2021.06.14]
　LIU Xiaodan,HU Ying,ZUO Zhengkang*.The Derivation and Formal Proof of Graph Search Algorithm[J].Journal of Jiangxi Normal University:Natural Science Edition,2021,(03):642.[doi:10.16357/j.cnki.issn1000-5862.2021.06.14]
[4]左正康,方 越,黄志鹏,等.二叉树队列关系问题非递归算法的推导及形式化证明[J].江西师范大学学报(自然科学版),2022,(01):49.[doi:10.16357/j.cnki.issn1000-5862.2022.01.07]
　ZUO Zhengkang,FANG Yue,HUANG Zhipeng,et al.The Derivation and Formal Proof of Non-Recursive Algorithm for Binary Tree Queue Relation Problems[J].Journal of Jiangxi Normal University:Natural Science Edition,2022,(03):49.[doi:10.16357/j.cnki.issn1000-5862.2022.01.07]

备注/Memo

备注/Memo:
收稿日期:2019-09-16
基金项目:国家自然科学基金(61662035)资助项目.
通信作者:杨庆红(1968-),女,江西南昌人,教授,主要从事软件形式化和智能教育软件的研究.E-mail:yangqh120@163.com
更新日期/Last Update: 2020-06-10