随着软件规模的不断扩大，驾驭软件开发的难度越来越大，开发正确、可靠的软件成为一个亟待解决的问题。软件工程虽然对消解软件危机起到很重要的作用，但它并不提供保证软件正确性的机制。形式化方法力图解决此问题，以开发正确可靠的软件为目标。 目前已经出现的形式化方法多种多样，不过一般来说，形式化方法包含形式规范和精化两大重点。形式规范是对系统的形式化描述，而精化是系统从抽象规范到具体实现的演化过程。 由于不同的形式化方法对形式规范的描述差别较大，规范的语义也各不相同，所以各种形式化方法在精化上都有各自的特点，从精化的定义、精化方式到精化规则等各方面有很大差别。一般来说，形式化方法的语义基础对精化方法有很重要的影响。比如，基于逻辑的方法采用的是公理语义，这类的形式化方法其精化就很类似，而基于模型的方法采用的是指称语义，它们的精化也有统一的模型。 本文讨论了基于逻辑的方法、基于模型的方法、代数方法和余代数方法等各自的精化理论，然后开发了一个实例，根据各种方法的特点在开发的不同阶段采用不同的方法。其中用余代数规范描述需求，根据余代数的精化方法对此规范做精化，然后转换到代数规范并做精化，继而转换到VDM规范，在对该VDM规范做数据精化后，将它转换到精化演算的规范语句，最后运用精化演算的精化规则推导出接近编程语言实现的程序代码。这种开发是一种尝试，同时也具有一般的意义。文章最后对这些形式化方法的精化理论进行了分析与比较，并且分析了形式化方法在精化方面今后可能的研究热点和方向。