基于PAR方法开发算法程序的研究
|
摘要
软件系统的成功极大依赖软件需求工程的质量，而软件的可靠性难以保证和开发效率低一直是困扰软件产业的两大难题。而用形式化方法开发软件始终被认为是提高软件可靠性和软件生产率的重要途径，是实现软件开发自动化的关键。尽管已经提出了各种各样的软件形式化方法和开发技术，但目前这些技术还远没有广泛的被软件产业界所接受，原因在于许多方法的提倡者并没有真正研究软件开发者面临的实际问题，算法和程序研究脱节，缺乏系统的算法程序设计和证明方法，实际上有些方法以及这些方法为基础而建立的软件开发工具和自动生成系统只能处理和生成一些玩具式程序(toy-style program)。尚没有一种面向实际问题、简单可行、便于广大软件开发者接受的形式化方法及与该方法相配套的一系列配套的辅助工具来切实的解决这两个问题。
PAR方法基于分化、递推、扩充的量词变换规则、循环不变式的新技术和软件转换工具，充分利用数据抽象、功能抽象、软件重用、多态、类属、重载等成熟的程序设计技术，可以用统一的方法开发复杂算法。
本文首先对形式化方法的定义、分类、目前的发展状况等进行了介绍，同时对典型的形式化方法VDM、Z、B方法、RAISE等形式化语言和方法的产生、主要原理及特点作了介绍，并进行了分析比对；其次，本文还对PAR方法也做了较为详尽的介绍，进一步研究了它的特点，阐述了其哲学思想；最后，运用PAR方法开发了正整数素数分解问题、线性代数统一的算法——基准位置法等多个问题的算法程序，进一步验证了PAR方法在很多复杂数值算法中的应用。
Success of software system mostly depends on the quality of demand engineering, but liability and efficiency of software are always two difficult problems disturbed software enterprise. Formal method is always thought the significant way to solve such problems and the key to realize the automatic design. Although nowadays variety of software formal methods and explode technology have been proposed, there are still far way to be widely accepted by software enterprise. It lies in many advocators of different methods haven't done real research on the problems which designers encounter, the disconnection between algorithm and program in study, lack of systematic algorithmic program design and proof method, hi actually, some methods , software explore tools established on above methods and automatic generating system can only deal with or generate toy-style program.. It still havenot a formal method which is oriented to practical problems, simple and variable, convenient to be accepted by software designers, and
a series matched compliment tools, used to solve the problems above.
The PAR method, the variation principles of divided, increased, and expanded measure words, loop invariants, and other mew techniques and software variation methods are applied to design complex algorithm, which runs through the whole process of the software development. The PAR method, describing the algorithm in a novel way, defines Radl, which is more simple, precise and comprehensible than ordinary computer language, procedure charts and the method of program description.
The thesis starts with comprehensive introduction of the formal method and language, including its definition and classify .Then explains the prime number deduction and works out algorithm procedure and involves the advantages of the method and the quantity of calculation core of matrix algebra and widely used it, The standard location method can be applied to many aspects of matrix algebra such as determinant, the rank of matrix and vector. At last, the thesis involves the dynamic design of the algorithm program.
PAR方法基于分化、递推、扩充的量词变换规则、循环不变式的新技术和软件转换工具，充分利用数据抽象、功能抽象、软件重用、多态、类属、重载等成熟的程序设计技术，可以用统一的方法开发复杂算法。
本文首先对形式化方法的定义、分类、目前的发展状况等进行了介绍，同时对典型的形式化方法VDM、Z、B方法、RAISE等形式化语言和方法的产生、主要原理及特点作了介绍，并进行了分析比对；其次，本文还对PAR方法也做了较为详尽的介绍，进一步研究了它的特点，阐述了其哲学思想；最后，运用PAR方法开发了正整数素数分解问题、线性代数统一的算法——基准位置法等多个问题的算法程序，进一步验证了PAR方法在很多复杂数值算法中的应用。
Success of software system mostly depends on the quality of demand engineering, but liability and efficiency of software are always two difficult problems disturbed software enterprise. Formal method is always thought the significant way to solve such problems and the key to realize the automatic design. Although nowadays variety of software formal methods and explode technology have been proposed, there are still far way to be widely accepted by software enterprise. It lies in many advocators of different methods haven't done real research on the problems which designers encounter, the disconnection between algorithm and program in study, lack of systematic algorithmic program design and proof method, hi actually, some methods , software explore tools established on above methods and automatic generating system can only deal with or generate toy-style program.. It still havenot a formal method which is oriented to practical problems, simple and variable, convenient to be accepted by software designers, and
a series matched compliment tools, used to solve the problems above.
The PAR method, the variation principles of divided, increased, and expanded measure words, loop invariants, and other mew techniques and software variation methods are applied to design complex algorithm, which runs through the whole process of the software development. The PAR method, describing the algorithm in a novel way, defines Radl, which is more simple, precise and comprehensible than ordinary computer language, procedure charts and the method of program description.
The thesis starts with comprehensive introduction of the formal method and language, including its definition and classify .Then explains the prime number deduction and works out algorithm procedure and involves the advantages of the method and the quantity of calculation core of matrix algebra and widely used it, The standard location method can be applied to many aspects of matrix algebra such as determinant, the rank of matrix and vector. At last, the thesis involves the dynamic design of the algorithm program.
引文
[1] Xue Jinyun. Two New Strategies for. Developing LoopLnvariantsand Its Applications. JOURNAL COMPUTER SCIENCE AND TECHNOLOGIES. No. 3, 1993. 4
[2] Xue Jinyun. A Unified Approach For Developing Efficient Algorithmic Program. Journal of Computer Science and Technologies, 1997, 12(4).
[3] Xue Jiuyun, D. Gries 1988.11. Developing A Linear Algorithm For Cubing a Cyclic Pormutation. SCIENCE OF COMPUTER PROGRAMMING, VOL. 11(12),161_165.
[4] D. Gries, Xue Jinyun, 1988.10.Generating A Random Permutation, Bit28,569_572.
[5] 薛锦云．杂算法程序的规范证明和形式推导．中国计算机学会第八届年会论文集．1982．8．
[6] 薛锦云．论循环不变式及其开发技术，《全国第四次软件工程研讨会论文集》，270-276，1991年10月．
[7] 皱盛荣 郑国梁．B语言和方法与Z、VDM的比较，计算机科学 2002Vol．29No．10．
[8] Luqi and J. A. Goguen. Formal Methods: Promises and Problems. IEEE Software, pp. 73-85, January/February 1997.
[9] Gries. D. The Science of Programming. Springer Verlag. New York. 1981.
[10] Remmers. J. A Technipue for Developing Loop Invariants information Processing Letters 18(1984) 137-139.
[11] Linger. R. C. Mills. H. D. and Witt. B. I. Structured Programming: Theory and Practice. Reading Mass, Addison-Wesley, 1979.
[12] Dijstra. E. W. A discipline of Programming, Pretice Hall, Englewood Cliffs, 1976.
[13] Djistra. E. W. and Van Gasteren, A. J. M. A Simple Fixppoint Argument Without the Restriction to Continuity, Acta Information 23, 1-7(1986).
[14] Gries. D. A Note on A Standard Stategy for developing Loop Invariants and Loops Scienceof Computer Programming 2,207-214(1982).
[15] Willianm Stallings, Cryptgraphy and Network Security: Principles and Practice Second Edition, ISBN 7-5053-6604-1.
[16] 冯登国，密码分析学．清华大学出版社，ISBN 7-302-03976-3．
[17] 卢开澄，组合数学。清华大学出版社，ISBN 7-302-00851-5／TP．307．
[18] 胡运权 郭耀煌《运筹学教程》清华大学出版社 1998．6．
[19] 潘金贵等 《现代计算机常用数据结构和算法》南京大学出版社 1994．3．
[20] 解可新 韩立兴 林友联《最优化方法》天津大学出版社 1997．1．
[21] D. Coleman et al. Object-Oriented Devolopment: The Fusion Method. Prentice Hall Object-Oriented Series, 1993.
[22] P. Etique and J. Hubaux and X. Logeon. Service Specification and Validation for the Intelligent Netwok. Baltzer Icn, Special Issue on Telecommunication Services, Jan. 1998.
[23] E. K. Anders. Telelogic Tau 3.2 Reference Manual—The SOMT method. Telelogic, Malmo, Sweden, March 1997.
[24] D. Amoyot, Specification and Validation of Telecommun-
ications Systems with Use Case Maps and LOTOS. Ph. D. thesis, SITE, Univercity of Ottawa, Canada, September 2001.
[25] A. Eberlein, Requirements Acquisition and Specification for Telcommunication Services. PhD Thesis, Univercity of Wales, Swansea, UK. 1997.
[26] A. Eberlein, M. Crowther and F. Halsall, RATS: A Soft Tool to aid the Transition from Service Idea to Service Implementation. In: Proceeding of the 1996 IEEE Global Telecommunications Conference (GLOBALCOM'96), London, UK, 1996.
[27] J. M. Spivey. The Z Notion: A Reference Manual, Prentice Hall International, second edition, 1993.
[2] Xue Jinyun. A Unified Approach For Developing Efficient Algorithmic Program. Journal of Computer Science and Technologies, 1997, 12(4).
[3] Xue Jiuyun, D. Gries 1988.11. Developing A Linear Algorithm For Cubing a Cyclic Pormutation. SCIENCE OF COMPUTER PROGRAMMING, VOL. 11(12),161_165.
[4] D. Gries, Xue Jinyun, 1988.10.Generating A Random Permutation, Bit28,569_572.
[5] 薛锦云．杂算法程序的规范证明和形式推导．中国计算机学会第八届年会论文集．1982．8．
[6] 薛锦云．论循环不变式及其开发技术，《全国第四次软件工程研讨会论文集》，270-276，1991年10月．
[7] 皱盛荣 郑国梁．B语言和方法与Z、VDM的比较，计算机科学 2002Vol．29No．10．
[8] Luqi and J. A. Goguen. Formal Methods: Promises and Problems. IEEE Software, pp. 73-85, January/February 1997.
[9] Gries. D. The Science of Programming. Springer Verlag. New York. 1981.
[10] Remmers. J. A Technipue for Developing Loop Invariants information Processing Letters 18(1984) 137-139.
[11] Linger. R. C. Mills. H. D. and Witt. B. I. Structured Programming: Theory and Practice. Reading Mass, Addison-Wesley, 1979.
[12] Dijstra. E. W. A discipline of Programming, Pretice Hall, Englewood Cliffs, 1976.
[13] Djistra. E. W. and Van Gasteren, A. J. M. A Simple Fixppoint Argument Without the Restriction to Continuity, Acta Information 23, 1-7(1986).
[14] Gries. D. A Note on A Standard Stategy for developing Loop Invariants and Loops Scienceof Computer Programming 2,207-214(1982).
[15] Willianm Stallings, Cryptgraphy and Network Security: Principles and Practice Second Edition, ISBN 7-5053-6604-1.
[16] 冯登国，密码分析学．清华大学出版社，ISBN 7-302-03976-3．
[17] 卢开澄，组合数学。清华大学出版社，ISBN 7-302-00851-5／TP．307．
[18] 胡运权 郭耀煌《运筹学教程》清华大学出版社 1998．6．
[19] 潘金贵等 《现代计算机常用数据结构和算法》南京大学出版社 1994．3．
[20] 解可新 韩立兴 林友联《最优化方法》天津大学出版社 1997．1．
[21] D. Coleman et al. Object-Oriented Devolopment: The Fusion Method. Prentice Hall Object-Oriented Series, 1993.
[22] P. Etique and J. Hubaux and X. Logeon. Service Specification and Validation for the Intelligent Netwok. Baltzer Icn, Special Issue on Telecommunication Services, Jan. 1998.
[23] E. K. Anders. Telelogic Tau 3.2 Reference Manual—The SOMT method. Telelogic, Malmo, Sweden, March 1997.
[24] D. Amoyot, Specification and Validation of Telecommun-
ications Systems with Use Case Maps and LOTOS. Ph. D. thesis, SITE, Univercity of Ottawa, Canada, September 2001.
[25] A. Eberlein, Requirements Acquisition and Specification for Telcommunication Services. PhD Thesis, Univercity of Wales, Swansea, UK. 1997.
[26] A. Eberlein, M. Crowther and F. Halsall, RATS: A Soft Tool to aid the Transition from Service Idea to Service Implementation. In: Proceeding of the 1996 IEEE Global Telecommunications Conference (GLOBALCOM'96), London, UK, 1996.
[27] J. M. Spivey. The Z Notion: A Reference Manual, Prentice Hall International, second edition, 1993.