【作者】 王森；

【导师】 薛锦云；

【作者基本信息】 江西师范大学 ， 计算机软件与理论， 2004， 硕士

【摘要】 软件系统的成功极大依赖软件需求工程的质量，而软件的可靠性难以保证和开发效率低一直是困扰软件产业的两大难题。而用形式化方法开发软件始终被认为是提高软件可靠性和软件生产率的重要途径，是实现软件开发自动化的关键。尽管已经提出了各种各样的软件形式化方法和开发技术，但目前这些技术还远没有广泛的被软件产业界所接受，原因在于许多方法的提倡者并没有真正研究软件开发者面临的实际问题，算法和程序研究脱节，缺乏系统的算法程序设计和证明方法，实际上有些方法以及这些方法为基础而建立的软件开发工具和自动生成系统只能处理和生成一些玩具式程序(toy-style program)。尚没有一种面向实际问题、简单可行、便于广大软件开发者接受的形式化方法及与该方法相配套的一系列配套的辅助工具来切实的解决这两个问题。 PAR方法基于分化、递推、扩充的量词变换规则、循环不变式的新技术和软件转换工具，充分利用数据抽象、功能抽象、软件重用、多态、类属、重载等成熟的程序设计技术，可以用统一的方法开发复杂算法。 本文首先对形式化方法的定义、分类、目前的发展状况等进行了介绍，同时对典型的形式化方法VDM、Z、B方法、RAISE等形式化语言和方法的产生、主要原理及特点作了介绍，并进行了分析比对；其次，本文还对PAR方法也做了较为详尽的介绍，进一步研究了它的特点，阐述了其哲学思想；最后，运用PAR方法开发了正整数素数分解问题、线性代数统一的算法——基准位置法等多个问题的算法程序，进一步验证了PAR方法在很多复杂数值算法中的应用。更多还原

【Abstract】 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.更多还原