[1]熊小超,杨庆红*.2类组合数学问题的算法形式化推导[J].江西师范大学学报(自然科学版),2019,(04):402-408.[doi:10.16357/j.cnki.issn1000-5862.2019.04.12]
　XIONG Xiaochao,YANG Qinghong*.The Formal Derivation for Two Kinds of Combinatorial Mathematical Problems[J].Journal of Jiangxi Normal University:Natural Science Edition,2019,(04):402-408.[doi:10.16357/j.cnki.issn1000-5862.2019.04.12]
点击复制

2类组合数学问题的算法形式化推导()
分享到：

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

卷:
期数:
2019年04期
页码:
402-408
栏目:
信息科学与技术
出版日期:
2019-08-10

文章信息/Info

Title:
The Formal Derivation for Two Kinds of Combinatorial Mathematical Problems
文章编号:
1000-5862(2019)04-0402-07
作者:
熊小超; 杨庆红*
江西师范大学计算机信息工程学院,江西 南昌 330022
Author(s):
XIONG Xiaochao; YANG Qinghong*
College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
形式化方法;  程序规约;  组合数学;  递推技术
Keywords:
formal method;  program specification;  combinatorial mathematics;  recursive technique
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2019.04.12
文献标志码:
A
摘要:
组合数学问题算法的研究是计算机科学的重要研究内容,但在许多相关文献中,许多组合数学问题的算法只是经过简单分析得到,并未给出算法程序的详细设计过程,导致读者无法理解算法本质,更无法保证算法程序的正确性.该文在以组合数学中连续子序列最大乘积和第2类斯特林数变形问题为例的基础上,通过形式化描述问题的程序规约,使用规约变换规则,对程序规约进行一系列等价变换,获得问题求解序列的递推式,并以此为基础得到问题求解的算法程序,清晰地展示了从问题的需求到算法程序的详细推导过程.通过对相关组合数学问题的进一步深入研究,提炼了2类组合数学问题的求解策略,为提高组合数学问题算法程序的正确性提供了有效途径.
Abstract:
The research of combinatorial mathematics problem algorithm is an important research content of computer science.However,in many related literatures,most of the algorithms for combining mathematics problems are obtained through simple analysis.The detailed design process of the algorithm program is not given,which leads the reader to fail to understand the essence of the algorithm.It is impossible to guarantee the correctness of the algorithm program.The maximum product of continuous subsequences and the deformation problem of the second type of Stirling numbers in combinatorial mathematics are taken as an example.Based on this example,a series of equivalent transformations are performed on the program specification to obtain the problem solving by formalizing the program specification of the problem,using the rule transformation rules.The recursive formula of the sequence,based on which the algorithm program of the problem solving is obtained,clearly shows the requirements from the problem to the detailed derivation process of the algorithm program,and through the further in-depth study of the related combinatorial mathematics,two types of combinations are extracted.The solution strategy of mathematical problems provides an effective way to improve the correctness of the algorithm program of combinatorial mathematics.

参考文献/References:

[1] 高逸人.组合数学在软件工程领域中的应用研究[J].科技与创新,2017(23):143-144.
[2] 布鲁迪.组合数学[M].冯速,译.5版.北京:机械工业出版社,2012.
[3] 孙凌宇.PAR方法在组合数学问题中的应用研究[D].南昌:江西师范大学,2005.
[4] 石海鹤,石海鹏,薛锦云.形式化开发若干组合数学问题的算法[J].江西师范大学学报:自然科学版,2006,30(5):423-427.
[5] 游颖.算法形式化方法在三类组合数学问题求解中的应用研究[D].南昌:江西师范大学,2017.
[6] 游颖,杨庆红,齐蕾蕾.3个变形背包问题的形式化推导[J].江西师范大学学报:自然科学版,2017,41(2):116-121.
[7] 张园,杨庆红,胡昊.基于递推技术的算法设计方法的应用研究[J].计算机与现代化,2012(6):37-39.
[8] 单学广.基于递推技术的算法程序设计方法的研究与应用[D].南昌:江西师范大学,2011.
[9] 刘峰涛,贺国光.基于L-Z方法的宏观交通运输系统复杂性测度[J].哈尔滨工业大学学报,2008,40(12):2058-2061.
[10] Larsen P G,Fitzgerald J.The evolution of VDM tools from the 1990s to 2015 and the influence of CAMILA[J].Journal of Logical and Algebraic Methods in Programming,2016,85(5):985-998.
[11] 丁湘陵,王志刚.基于B方法的体系结构描述语言的形式化研究[J].计算机工程与科学,2013,35(1):100-106.
[12] 黄昱,马殿富,赵永望,等.一种基于B方法的形式化开发方法[C]∥全国抗恶劣环境计算机第二十四届学术年会论文集.北京:北京航空航天大学出版社,2014:278-287.
[13] 胡启敏,薛锦云,游珍,等.PAR平台中若干软件构件形式化验证技术研究[J].计算机工程与科学,2018,40(2):268-274.
[14] 胡启敏,薛锦云.若干算法程序的形式化推导与生成技术研究[J].计算机研究与发展,2008,45(S1):148-153.
[15] You Zhen,Xue Jinyun,Zuo Zhengkang.Unified formal derivation and automatic verification of three binary-tree traversal non-recursive algorithms[J].Cluster Computing,2016,19(4):2145-2156.

相似文献/References:

[1]游 颖,杨庆红,齐蕾蕾.3个变形背包问题的形式化推导[J].江西师范大学学报(自然科学版),2017,(02):116.
　YOU Ying,YANG Qinghong,QI Leilei.The Formal Derivation of Three Forms of 0-1 Knapsack Problems[J].Journal of Jiangxi Normal University:Natural Science Edition,2017,(04):116.
[2]齐蕾蕾,杨庆红*,游 颖.算法的形式化推导与基于Isabelle的自动化验证[J].江西师范大学学报(自然科学版),2018,(04):379.[doi:10.16357/j.cnki.issn1000-5862.2018.04.10]
　QI Leilei,YANG Qinghong*,YOU Ying.The Formal Derivation of Algorithm and Automatic Verification Based on Isabelle[J].Journal of Jiangxi Normal University:Natural Science Edition,2018,(04):379.[doi:10.16357/j.cnki.issn1000-5862.2018.04.10]

备注/Memo

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