摘 要：本文主要介绍了形式化技术的一些基本的理论，重点对形式化技术在软件工程和数学理论基础领域的作用进行研究。分析了形式化技术在软件工程领域的一些优势和局限性。并且指明了形式化技术在以后的发展中可能的方向，并且对形式化技术在软件工程中的作用进行了评价。
【关键词】软件工程 形式化技术 理论基础
1 形式化技术
形式化技术就是将使用由一定的语法规则组成的公式或者符号来代表一定的含义。在软件工程中，这种形式化技术被广泛的使用，但是它们却没有进行精确的定义，仅仅是根据人们的使用习惯，因此现存的可能有很多版本的形式化技术方法。形式化技术是利用数学的方法来解决软件工程中的问题和计算机科学理论研究的一种工具，程序设计语言理论、数理逻辑、集合论、代数理论、构造类型论等这些数学理论都为形式化技术垫定了比较坚实的理论基础。形式化技术最重要的理论工具是数理逻辑。从数理逻辑的角度来看，集合和数理逻辑可建立任何复杂的数学结构，因此它们成为了构造形式化技术比较重要的理论基础。形式化技术形成了不同的软件规约形式语言。
2 软件工程各阶段的规约描述
软件的开发周期有需求分析、详细设计、测试、可行性分析、体系结构设计和编码六个部分。形式化技术贯穿于软件开发周期的六个部分，形式化时基于参数化的数学理论形式化定义语义。下面从可行性分析、需求分析、体系结构设计和详细设计几个方法进行说明。
2.1 可行性分析
软件生命周期的第一个阶段是可行性分析阶段，在这一阶段要通过大量的数据资料来说明系统的开发是否是可行的。指出项目的建议、风险预测、可行性，为项目的决策提供参考依据。在此阶段，通过将实际问题转化为可行性的研究，形成一定的文档材料，规定专业的属于，说明软件系统进行开发的处理流程、数据流程、输入输出、运行环境和开发环境等等。当前来说，专门用于可行性分析这一阶段的形式化技术还非常少，主要的原因是无法将形式化的符号和自然的语言很好的结合起来，确保使用本软件的用户可以非常清楚明白的理解形式化技术所要描述的意义。Z语言是目前一种不可执行的半形式化语言，它短小且容易阅读，采用非形式化的英语对软件的规约进行解释。
2.2 需求分析
需求分析分为信息处理和分信息预处理两个阶段，将可行性分析报告作为输入。元语言是形式化语言中的一种，它是基于集合论的证明规则和谓词演算，给出抽象机状态确定模型，从而生成文档。这种形式化语言，对于程序员来说，容易实现原型而且可读性好，容易掌握。语义的设计是形式化技术中需求分析阶段主要要进行的工作之一。在需求分析这一阶段，ER图是从可行性分析的实际问题中导出来的。通过ER图给出SXL语言的事实和对象，SXL语言有助于开发团队理解和交流。SXL语言、RAISE语言和VDM元语言都是应用于需求分析阶段的比较常用的形式化技术。
2.3 体系结构设计
软件设计的第三个阶段是体系结构的设计，在这一阶段是将需求分析转换为要实现的目标软件，并进行各种方案的分析和比较，最终选择较好的方案。在体系结构设计阶段采用过程代数形式化的攻击进行输入、输出的行为描述。TLG语言适合体系结构设计阶段不强调如何做仅仅说明做什么。采用形式化的说明把自然的语言融入到逻辑程序设计范型和数学函数中，这样更容易证明用户需求的一致性。GLIDE是一种半形式化的SSFL，GLIDE的好处是应用范围广，而且抽象的级别比较高，不过也有一定的局限性就是使用的时候需要适当的进行扩充和修改。
2.4 详细设计
软件设计的第四个阶段就是详细设计，在详细设计阶段，要与软件系统的形式化描述一致。在详细设计阶段，要为软件系统的各个模块设计相应的内部数据结构和算法，确定最终系统实现的一个精确的描述。Larch语言是用于说明程序功能，可以适当的增强详细设计阶段的处理能力和描述能力。形式化的Trace语言作为软件详细设计阶段的形式化工具，采用将模块实现的抽象数据作为自动机说明每个模块的接口需求。Trace语言与SSFL语言不同的特点是程序自动的生成和验证在同一形式的系统内进行。
3 形式化技术的评价
形式化技术在软件工程中有效的提高了开发的效率、改进了软件开发的质量、减少了开发费用。形式化的技术容易在软件的规约上取得一致性，它属于一种非常有效的交流方式。在软件工程中，形式化技术的优势在于语法定义准确、问题抽象、表达无二义性、语义清晰可操纵、描述简洁规范。形式化技术在非功能性的要求上比如安全性、保密性、结构性上利用数学工具更容易进行核查。虽然形式化技术在软件工程的各个阶段已经取得了不错的成就，但是还是存在着一定的局限性，比如缺乏在实际项目中应用的有效工具。程序功能的正确性有时候难以证明，因为形式化技术缺乏定理证明机制的支持。形式化技术的下一个发展方向应该是尽量的把形式化的语言表达的形式进行简单化，让其趋于自然语言，增强它的可理解能力。
4 总结
在软件工程中，形式化技术极有好处也有弊端，有很多人支持这种技术，也有人对它持反对态度。在软件工程发展的过程中，形式化的技术也起到了相当大的作用。在四十多年对形式化技术的研究中，很多成功的案例也证明了形式化技术的巨大作用，但是我们也需要清醒的认识到它在实践和工业的应用中所存在的缺陷和困难。
参考文献
[1]陈火旺，罗朝晖，马庆鸣.程序设计方法学基础[M].长沙：湖南科学技术出版社，1987.
[2]陆汝钤.计算机语言的形式语义[M].北京：科学出版社，1992.
[3]李未.数理逻辑基本原理与形式推演[M].北京：科学出版社，2007.
[4]陈意云.程序设计语言理论[M].北京：高等教育出版社，2004.
[5]屈延文.形式语义学基础与形式说明[M].北京：科学出版社，2010.
[6]郑红军，张乃孝.软件开发中的形式化方法[J].计算机科学，2011.
[7]朱冰，梅宏，杨芙清.软件开发过程中的形式化方法[J].计算机科学，2006.
[8]廖常初.PLC编程及应用[M].北京：机械工业出版社，2008.
[9]崔坚.西门子工业网络通信指南（下册）[M].北京：机械工业出版社，2005.
