2类数列问题循环不变式开发策略研究与应用

该文通过对组合数学中Catalan数列问题和Fibonacci数列问题进行深入研究,利用归纳推理、组合数学中的加法和乘法原理等方法得到问题求解函数,使用变量记录算法求解过程中子问题的解,并约束循环变量的变化范围,获得问题求解算法的循环不变式,由此得到了2类数列问题循环不变式的统一开发策略.以二叉树的形态数问题和阶梯问题为例,利用所提策略开发循环不变式,并基于循环不变式展示了这2类数列问题算法程序的形式化推导过程.

The Research and Application of Loop Invariant Development Strategy for Two Kinds of Sequence Problems

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.