随着计算机技术的飞速发展,产生了越来越多的遗产系统,对这些系统进行维护和升级是软件工程师们经常要面对的问题。要对遗产系统进行维护和再工程,就需要用逆向工程技术对当前系统的结构和行为进行理解。作为软件工程中的一种新技术,逆向工程能够分析目标系统,确定系统的组件和它们之间的相互关系,并以另一种形式或者在更高的抽象级别上建立对系统的表示,从而帮助维护人员理解并重构软件系统。形式化方法对于软件的发展,尤其是正向工程方面提供了许多好处。形式化方法的一个优点是它的表示是精确的、可验证的,这样有助于使用自动化的处理。一种利用形式化方法优点的方式就是通过对现有程序代码进行逆向工程来得到形式化规约。本文描述的逆向工程中的形式化方法采用最强后置条件谓词转换技术和Hoare理论中有关程序语义的部分正确性模型,研究的重点是利用形式化技术和非形式化技术对程序代码进行逆向工程,以支持软件理解和维护。针对C程序的基本语法结构定义了赋值语句规则、选择语句规则、循环语句规则、顺序语句规则和函数调用规则,建立了一个最小的公理系统。介绍了以C-Minus语言(自定义的一种简化的C语言子集)为实例进行逆向工程的过程。在进行逆向分析的过程中,首先对源程序进行词法语法分析生成语法树,从结构化源程序中提取源程序的模板信息,并把模板信息用一个二叉树表示,之后按照设计的二叉树遍历算法,把二叉树转化为P A D(Problem Analysis Diagram)图,用以描述程序的结构,并作为可视化的人工理解辅助工具,便于我们从中方便的选出源代码的关键部分。在结构化分析的基础上,对关键性的源代码文件进行扫描,对每条语句进行分析,根据C程序语句中各种基本结构的最强后置条件形式化语义,对每条语句按照相应的规则进行转换,得到程序的形式规约。