摘要
该文通过对组合数学中Catalan数列问题和Fibonacci数列问题进行深入研究,利用归纳推理、组合数学中的加法和乘法原理等方法得到问题求解函数,使用变量记录算法求解过程中子问题的解,并约束循环变量的变化范围,获得问题求解算法的循环不变式,由此得到了2类数列问题循环不变式的统一开发策略.以二叉树的形态数问题和阶梯问题为例,利用所提策略开发循环不变式,并基于循环不变式展示了这2类数列问题算法程序的形式化推导过程.
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.
作者
古素梅
杨庆红
GU Sumei;YANG Qinghong(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China)
出处
《江西师范大学学报（自然科学版）》
CAS
北大核心
2020年第3期307-312,共6页
Journal of Jiangxi Normal University(Natural Science Edition)
基金
国家自然科学基金(61662035)资助项目.
关键词
数列问题
循环不变式
可信软件
归纳推理
sequence problem
loop invariant
trustworthy software
inductive reasoning
