形式化方法是软件开发方法合理的发展方向，软件开发自动化的发展影响着形式化方法的应用前途；而软件开发自动化的程度又相当依赖于求精自动化的程度。 结构化方法、面向对象方法和形式方法是目前软件开发中使用的三种主要方法。本文在分析了上述三种方法的基础上，取各家之长，互相结合，提出一个基于结构化方法、面向对象方法和形式方法相结合的新的软件开发方法，称之为结构化面向对象的形式方法SOFM(Structured Object-oriented Formal Method)。SOFM的核心思想是大结构、小对象。该方法的基本思想是：在构造一个软件系统时，使用基于数据流图的结构化方法和面向对象方法：在系统开发的整个过程，以一种比较实用的方式来应用形式方法；最后通过求精的方法产生所需要的代码。为了支持SOFM，我们提出了一个新的软件开发语言—结构化的Object-Z需求规格说明语言SOZRSL(Structured Obiect-Z Requirement Specification Language)。SOZRSL采用分层谓词数据流图嵌入Object-z来实现SOMF思想；分层谓词数据流图是对传统数据流图的改进并加以形式化。为了使SOZRSL更准确、严密，本文给出了其严格的公理化语义。 形式化的好处在于便于实现程序设计的自动化。为了使SOZRSL的规格说明能自动化程度较高地转换成具体编程语言，本文给出了SOZRSL规格说明的求精。文中将SOZRSL规格说明的求精分解为结构求精、数据求精和谓词求精三部分。结构求精中给出了SOZRSL的分层逐步分解的结构到具体目标语言能够支持的整体结构的对应方法；数据求精给出了把规格说明语言中数学化的抽象数据类型，求精成具体目标语言能够支持的、更加面向计算机的具体数据类型的具体方法与规则；谓词求精着重介绍了基于Tableau方法的、以定理证明为基础的程序综合求精变换，引入了扩充的Tableau方法的演绎规则—合并规则，并利用该规则给出了SOZRSL语言中模式的与、或操作的求精方法，从而简化了模式复合的求精；为了使Tableau方法能够用于SOZRSL语言的求精，本文定义了将SOZRSL语言的结构成分转化为Tableau方法所能接受的结构的规则。 求精工作的自动化程度越高，要求搜索到的规则匹配程度越高。提高求精效率的方法之一是提高规则的搜索、匹配速度。为了提高匹配规则的速度，优化人工干预，本文首次将遗传算法应用到软件求精中的规则匹配与选择中。遗传算法具有快速收敛于最优解，但越接近最优解时反而收敛变慢的特点，我们正是利用这个特点来提高求精效率：首先利用它的快速收敛特点较快地得到一组优化解，然后，由人工根据知识和经验指导求精继续进行下去。上海大学工学博士学位论文 最后，我们实现了一个具体的sozRsL求精系统和适用于sozRsL、objeet一Z、Z的可视化编辑器。