递归问题循环不变式开发新策略的研究与应用
|
摘要
软件形式化是提高软件可靠性和生产效率、实现软件自动化的有效途径。循环不变式在软件形式化方法中占有十分重要的地位，它是理解、证明和推导算法程序的基础和关键。因此目前许多算法和程序设计的著作和教材中，均广泛地使用了循环不变式的概念和技术。
然而循环不变式的理论和开发技术尚很不完备，这直接影响了循环不变式在算法程序形式化开发中作用的发挥，导致大量复杂算法程序缺乏令人信服的推导和证明，使得许多计算机科学工作者对Dijkstra，Hoare和Gries等著名计算机科学家积极倡导的算法程序形式化开发方法的可行性和实用性产生了怀疑。
为了克服已有循环不变式开发技术存在的局限性，薛锦云教授在两个国家自然科学基金课题“若干新的算法程序设计和证明方法研究”和“实用的软件形式化方法及其开发工具的研究”的资助下，对循环不变式的理论和方法进行了系统的研究，提出了关于循环不变式的新定义和新的开发策略，并在此基础上形成了一种实用的算法程序形式化开发方法(PAR方法)及其开发环境，在复杂算法程序及软件形式化开发中发挥了重要作用。本文是PAR方法及其开发环境研究的继续，也是薛锦云当前主持承担的国家自然科学基金项目“基于PAR方法的算法设计形式化和自动化研究”的重要研究内容。
本文研究的主要目标是利用薛教授在开发循环不变式的新策略中提出的递归定义思想，探索一类递归定义问题的循环不变式开发技术，并应用于涉及组合数据结构的复杂算法程序的形式化推导和证明。具体研究成果如下：
1．进一步深入研究了循环不变式在算法程序形式化方法中的地位和作用；
2．对现有的循环不变式开发技术进行了分析和比较，剖析了其难以实用的原因；
3．基于现有循环不变式开发技术中的递归定义思想，提出了开发复杂递归问题循环不变式的两种新策略；
4．利用抽象程序设计语言Apla精确描述了6个典型树、图等问题的程序规约和求解算法程序，用上述提出的两种新策略开发了循环不变式，实现了严格的形式化推导或证明，并用PAR方法提供的算法程序自动转换系统将得到的Apla算法程序转换成对应的Delphi和C~(++)程序，均得到了正确的运行结果，大幅度地提高了这类复杂算法程序的可靠性和开发效率。
总之，本文得到的结果可应用于一类复杂算法程序的形式化推导和证明，方法简单，应用方便，为实现算法设计的形式化和自动化作出了有益的贡献。
Formal method is efficient way which can improve reliability and productivity of software and implement software automation. The loop invariants take a very important role in the formal method. They are a key for understanding, proving and deriving an algorithmic program. At present, the loop invariants' concept and technique is widely used in many teaching materials and literatures.
However existing techniques for developing loop invariants are not very perfect which bring about lacking convincing derivation and proof in large of complex algorithmic program. This leads to that many computer scientists doubt the possibility and practicability of deriving or proving algorithmic programs by loop invariant which the famous computer scientists, Dijkstra, Hoare and Gries, advocated enthusiastic.
To conquer limitations of existing techniques for developing loop invariants, professor Xue Jinyun, who is imbursed under two National Nature Science Foundation of China, systematically research the theory and method of loop invariants and advanced the new definition and developing strategies for loop invariants. Based on above, he presented efficiency method of developing algorithmic program, Partition-and-Recur Approach, and its developing environment which bring into important play in formal method. This paper is inherit of Partition-and-Recur Approach and its developing environment research and is important study content of the National Nature Science Foundation project which Xue Jinyun is taking charge of.
Two new strategies for developing loop invariants on recursive problem and their application in formal derivation and proof of complex algorithmic program are presented in this paper by the idea of recursive definition which Professor Xue proposed. The main achievements include:
1. This paper further research the status and function of loop invariants in formal method.
2. An analysis and comparison is Given about the existing techniques for developing loop invariants and the reasons are presented why they are difficult to popularize.
3. Based on recursive definition idea in existing technique of developing loop invariants, two new strategies for developing loop invariants on complicated recursive problems are presented.
4. Using abstract programming language, such as Apia, the specification and derivation of the algorithmic program in six typical trees, graph problem is described. The standard proof and formal derivation is implemented by two above new strategies for developing loop invariants. The algorithm in Apia is transformed into corresponding program in Delphi and C++ by the automated algorithmic transformation system that Partition-and-Recur method provided and correct result is received. These improve reliability and developing efficiency of the kind of complex algorithm.
In summary, achievements in this paper can be applied to the proof and derivation of a kind of complex algorithmic program, which are easier to use and apply. There is beneficial contribution to formal ization and automation of algorithmic program.
然而循环不变式的理论和开发技术尚很不完备，这直接影响了循环不变式在算法程序形式化开发中作用的发挥，导致大量复杂算法程序缺乏令人信服的推导和证明，使得许多计算机科学工作者对Dijkstra，Hoare和Gries等著名计算机科学家积极倡导的算法程序形式化开发方法的可行性和实用性产生了怀疑。
为了克服已有循环不变式开发技术存在的局限性，薛锦云教授在两个国家自然科学基金课题“若干新的算法程序设计和证明方法研究”和“实用的软件形式化方法及其开发工具的研究”的资助下，对循环不变式的理论和方法进行了系统的研究，提出了关于循环不变式的新定义和新的开发策略，并在此基础上形成了一种实用的算法程序形式化开发方法(PAR方法)及其开发环境，在复杂算法程序及软件形式化开发中发挥了重要作用。本文是PAR方法及其开发环境研究的继续，也是薛锦云当前主持承担的国家自然科学基金项目“基于PAR方法的算法设计形式化和自动化研究”的重要研究内容。
本文研究的主要目标是利用薛教授在开发循环不变式的新策略中提出的递归定义思想，探索一类递归定义问题的循环不变式开发技术，并应用于涉及组合数据结构的复杂算法程序的形式化推导和证明。具体研究成果如下：
1．进一步深入研究了循环不变式在算法程序形式化方法中的地位和作用；
2．对现有的循环不变式开发技术进行了分析和比较，剖析了其难以实用的原因；
3．基于现有循环不变式开发技术中的递归定义思想，提出了开发复杂递归问题循环不变式的两种新策略；
4．利用抽象程序设计语言Apla精确描述了6个典型树、图等问题的程序规约和求解算法程序，用上述提出的两种新策略开发了循环不变式，实现了严格的形式化推导或证明，并用PAR方法提供的算法程序自动转换系统将得到的Apla算法程序转换成对应的Delphi和C~(++)程序，均得到了正确的运行结果，大幅度地提高了这类复杂算法程序的可靠性和开发效率。
总之，本文得到的结果可应用于一类复杂算法程序的形式化推导和证明，方法简单，应用方便，为实现算法设计的形式化和自动化作出了有益的贡献。
Formal method is efficient way which can improve reliability and productivity of software and implement software automation. The loop invariants take a very important role in the formal method. They are a key for understanding, proving and deriving an algorithmic program. At present, the loop invariants' concept and technique is widely used in many teaching materials and literatures.
However existing techniques for developing loop invariants are not very perfect which bring about lacking convincing derivation and proof in large of complex algorithmic program. This leads to that many computer scientists doubt the possibility and practicability of deriving or proving algorithmic programs by loop invariant which the famous computer scientists, Dijkstra, Hoare and Gries, advocated enthusiastic.
To conquer limitations of existing techniques for developing loop invariants, professor Xue Jinyun, who is imbursed under two National Nature Science Foundation of China, systematically research the theory and method of loop invariants and advanced the new definition and developing strategies for loop invariants. Based on above, he presented efficiency method of developing algorithmic program, Partition-and-Recur Approach, and its developing environment which bring into important play in formal method. This paper is inherit of Partition-and-Recur Approach and its developing environment research and is important study content of the National Nature Science Foundation project which Xue Jinyun is taking charge of.
Two new strategies for developing loop invariants on recursive problem and their application in formal derivation and proof of complex algorithmic program are presented in this paper by the idea of recursive definition which Professor Xue proposed. The main achievements include:
1. This paper further research the status and function of loop invariants in formal method.
2. An analysis and comparison is Given about the existing techniques for developing loop invariants and the reasons are presented why they are difficult to popularize.
3. Based on recursive definition idea in existing technique of developing loop invariants, two new strategies for developing loop invariants on complicated recursive problems are presented.
4. Using abstract programming language, such as Apia, the specification and derivation of the algorithmic program in six typical trees, graph problem is described. The standard proof and formal derivation is implemented by two above new strategies for developing loop invariants. The algorithm in Apia is transformed into corresponding program in Delphi and C++ by the automated algorithmic transformation system that Partition-and-Recur method provided and correct result is received. These improve reliability and developing efficiency of the kind of complex algorithm.
In summary, achievements in this paper can be applied to the proof and derivation of a kind of complex algorithmic program, which are easier to use and apply. There is beneficial contribution to formal ization and automation of algorithmic program.
引文
[1] E.M.CLARKE, Formal Methods:State of the Art and Future Directions, ACM Computing Surveys, Vol.28, No.4, December 1996
[2] Jinyun Xue, Two New Strategies for Developing Loop Invariants and Their Applications, J. of Comput. Sci.& Technol., Vol. 8, No.2
[3] Gries D., The Science of Programming, Springer Verlag, Now York, 1981
[4] Dijkstra E. W., A Discipline of Programming, Prentice-Hall, New Jersey, 1976
[5] Backhouse R., Program Construction and Verification, Prentice-Hall, 1986
[6] Helmut K.,Formal Method of Program Verification and Specification, Prentice-Hall,1982
[7] Gries D., A Note on a Standard Strategy for Developing Loop Invariants and Loops,Science of Compute Programming 2, 1982
[8] Jinyun Xue, Ruth Davis, A Simple Program Whose Derivation and Proof is Also, Proceedings of icfem'97,IEEE CS Press, 1997.11
[9] Jinyun Xue, A Unified Approach for Developing Efficient Algorithmic Prgrams, J. of Comput. Sci.& Technol., Vol. 12, No.4
[10] Gries D., Jinyun Xue, Generating a Random Cyclic Permutation, BIT 28,1988
[11] Jinyun Xue, Gries D., Developing a Linear Algorithm for Cubing a Cyclic Permutation, Science of Computer Programming 11,1988
[12] Jinyun Xue, Formal derivation of Graph Algorithmic Programs Using Partition--and--Recur, J. of Comput. Sci. & Technol., Vol. 13, No.6
[13] Jinyun Xue, Formal Derivation of a Generic Algorithmic Program for Solving General Path Problems, Proceedings of the 3rd ASCM, august 1988
[14] Jinyun Xue, A Practicable Approach for Formal Development of Algorithmic Programs, ISFST'99 ,in Nanjing
[15] Linger, R. C. Mills, H.D. and Witt,B.I. StructuredProgramming:Theory and Practice,Reading Mass, Addison-Wesley, 1979.
[16] Remmers, J. A Technique for Developing Loop Invariants Information Processing Letters 18(1984) 137-139
[17] Juan Bicarregui and Brian Ritchie Invariant, Frames and Postconditions:A Comparison of the VDM and B Notations, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL21,NO.2,1995
[18] Michael D. Ernst, Jake Cockrell, Dynamically Discovering Likely Program Invariants to
Support Program Evolution, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL 27,NO. 2,2001
[19] 朱冰，梅宏，杨芙清，软件开发过程中的形式化方法，计算机科学，1995 Vol．22．No．1
[20] 姜利，孙永强，形式化方法的发展及展望，计算机科学，1998 Vol．25，No．2
[21] 李景洲，董继润，李保栋，论结构化方法与形式化方法的结合，计算机科学，1995，Vol．22，No．1
[22] 周青，关于程序验证方法的讨论，计算机科学，1995 Vol．22，No．3
[23] 形式化方法与软件可靠性，http://lcs.ios.ac.cn/～zwh/misc/xshff.html
[24] 陈火旺，罗朝晖，马庆鸣，程序设计方法学基础，湖南科学技术出版社
[25] 冯树椿，徐天通，程序设计方法学，浙江大学出版社
[26] H.K.Berg著，宋国新等译，程序验证和规范的形式方法
[27] 严蔚敏，吴伟民，数据结构，清华大学出版社
[28] 施伯乐等，数据结构，复旦大学出版社
[29] 黄明和，周定康等，数据结构，江西教育出版社
[30] 李春葆，数据结构习题与解析，清华大学出版社
[31] 傅清祥，王晓东，算法与数据结构，电子工业出版社
[32] 薛锦云，论循环不变式及其开发技术，全国第四次软件工程研讨会论文集，1994，5
[33] 薛锦云，算法程序形式化开发研究，云南大学学报，1997，19
[34] 薛锦云，一种系统的算法程序设计和证明方法，理论计算机科学进展，1994，10
[35] 李云清，薛锦云，利用循环不变式理解和开发程序，计算机与现代化1996第二期
[36] 薛锦云，李云清，杨庆红，王洪发，程序设计方法，高等教育出版社，2001
[37] 徐家福，陈道蓄，吕建，王志坚等，软件自动化，清华大学出版社，1994，9
[38] 薛锦云，探索软件形式化开发的正确途径，计算机与现代化，增刊，1994
[39] 薛锦云，开发新的数据类型实现复杂算法的形式推导和证明，中国高校第九次人工智能学术研讨会论文集。
[40] 李云清，算法程序设计的思维工具—循环不变式，第五届全国青年计算机会议(NCYY'94)论文集，1994
[41] 都志辉，张乃孝，状态迁移理论——关于循环不变式的探讨
[42] 薛锦云，抽象程序设计语言Apla报告，江西师范大学计算机软件研究所技术报告，2001，
[43] 薛锦云，算法设计语言Radl报告，江西师范大学计算机软件研究所技术报告，2001
[44] 李云清，薛锦云，基于分划递推的程序设计方法，计算机科学，2000，Vol．27，No．11
[45] 杨庆红，薛锦云，提高Ada可重用部件可靠性的两种方法，计算机工程，2001，6
[46]杨庆红，李云清，一种基于程序正确性证明理论的程序开发方法，计算机应用研究，2001，2
[47]杨庆红，薛锦云，用PAR方法开发算法程序，计算机科学，2000，Vol．27，No．11
[48]杨庆红，肖燕娟，一种高效的算法程序设计方法，计算机与现代化，2000，12
[49]杨庆红，也谈循环不变式开发方法，江西师大学报，2000，12
[2] Jinyun Xue, Two New Strategies for Developing Loop Invariants and Their Applications, J. of Comput. Sci.& Technol., Vol. 8, No.2
[3] Gries D., The Science of Programming, Springer Verlag, Now York, 1981
[4] Dijkstra E. W., A Discipline of Programming, Prentice-Hall, New Jersey, 1976
[5] Backhouse R., Program Construction and Verification, Prentice-Hall, 1986
[6] Helmut K.,Formal Method of Program Verification and Specification, Prentice-Hall,1982
[7] Gries D., A Note on a Standard Strategy for Developing Loop Invariants and Loops,Science of Compute Programming 2, 1982
[8] Jinyun Xue, Ruth Davis, A Simple Program Whose Derivation and Proof is Also, Proceedings of icfem'97,IEEE CS Press, 1997.11
[9] Jinyun Xue, A Unified Approach for Developing Efficient Algorithmic Prgrams, J. of Comput. Sci.& Technol., Vol. 12, No.4
[10] Gries D., Jinyun Xue, Generating a Random Cyclic Permutation, BIT 28,1988
[11] Jinyun Xue, Gries D., Developing a Linear Algorithm for Cubing a Cyclic Permutation, Science of Computer Programming 11,1988
[12] Jinyun Xue, Formal derivation of Graph Algorithmic Programs Using Partition--and--Recur, J. of Comput. Sci. & Technol., Vol. 13, No.6
[13] Jinyun Xue, Formal Derivation of a Generic Algorithmic Program for Solving General Path Problems, Proceedings of the 3rd ASCM, august 1988
[14] Jinyun Xue, A Practicable Approach for Formal Development of Algorithmic Programs, ISFST'99 ,in Nanjing
[15] Linger, R. C. Mills, H.D. and Witt,B.I. StructuredProgramming:Theory and Practice,Reading Mass, Addison-Wesley, 1979.
[16] Remmers, J. A Technique for Developing Loop Invariants Information Processing Letters 18(1984) 137-139
[17] Juan Bicarregui and Brian Ritchie Invariant, Frames and Postconditions:A Comparison of the VDM and B Notations, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL21,NO.2,1995
[18] Michael D. Ernst, Jake Cockrell, Dynamically Discovering Likely Program Invariants to
Support Program Evolution, IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, VOL 27,NO. 2,2001
[19] 朱冰，梅宏，杨芙清，软件开发过程中的形式化方法，计算机科学，1995 Vol．22．No．1
[20] 姜利，孙永强，形式化方法的发展及展望，计算机科学，1998 Vol．25，No．2
[21] 李景洲，董继润，李保栋，论结构化方法与形式化方法的结合，计算机科学，1995，Vol．22，No．1
[22] 周青，关于程序验证方法的讨论，计算机科学，1995 Vol．22，No．3
[23] 形式化方法与软件可靠性，http://lcs.ios.ac.cn/～zwh/misc/xshff.html
[24] 陈火旺，罗朝晖，马庆鸣，程序设计方法学基础，湖南科学技术出版社
[25] 冯树椿，徐天通，程序设计方法学，浙江大学出版社
[26] H.K.Berg著，宋国新等译，程序验证和规范的形式方法
[27] 严蔚敏，吴伟民，数据结构，清华大学出版社
[28] 施伯乐等，数据结构，复旦大学出版社
[29] 黄明和，周定康等，数据结构，江西教育出版社
[30] 李春葆，数据结构习题与解析，清华大学出版社
[31] 傅清祥，王晓东，算法与数据结构，电子工业出版社
[32] 薛锦云，论循环不变式及其开发技术，全国第四次软件工程研讨会论文集，1994，5
[33] 薛锦云，算法程序形式化开发研究，云南大学学报，1997，19
[34] 薛锦云，一种系统的算法程序设计和证明方法，理论计算机科学进展，1994，10
[35] 李云清，薛锦云，利用循环不变式理解和开发程序，计算机与现代化1996第二期
[36] 薛锦云，李云清，杨庆红，王洪发，程序设计方法，高等教育出版社，2001
[37] 徐家福，陈道蓄，吕建，王志坚等，软件自动化，清华大学出版社，1994，9
[38] 薛锦云，探索软件形式化开发的正确途径，计算机与现代化，增刊，1994
[39] 薛锦云，开发新的数据类型实现复杂算法的形式推导和证明，中国高校第九次人工智能学术研讨会论文集。
[40] 李云清，算法程序设计的思维工具—循环不变式，第五届全国青年计算机会议(NCYY'94)论文集，1994
[41] 都志辉，张乃孝，状态迁移理论——关于循环不变式的探讨
[42] 薛锦云，抽象程序设计语言Apla报告，江西师范大学计算机软件研究所技术报告，2001，
[43] 薛锦云，算法设计语言Radl报告，江西师范大学计算机软件研究所技术报告，2001
[44] 李云清，薛锦云，基于分划递推的程序设计方法，计算机科学，2000，Vol．27，No．11
[45] 杨庆红，薛锦云，提高Ada可重用部件可靠性的两种方法，计算机工程，2001，6
[46]杨庆红，李云清，一种基于程序正确性证明理论的程序开发方法，计算机应用研究，2001，2
[47]杨庆红，薛锦云，用PAR方法开发算法程序，计算机科学，2000，Vol．27，No．11
[48]杨庆红，肖燕娟，一种高效的算法程序设计方法，计算机与现代化，2000，12
[49]杨庆红，也谈循环不变式开发方法，江西师大学报，2000，12
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |