计算机论文：净室软件工程中的旋进策略

 　　为了得到高质量的软件,必须尽可能减少软件的失效和其他各种错误。其中测试是最常见的方法,静态排查是测试技术的一个重要方面,大量实践证明了其有效性。人们逐渐开始考虑是否可以证明程序部件的正确性,给出边界的约束条件和其它断言,并逐步将这些约束和断言分割到程序的每一个细节。从此各种有坚实数学基础的形式化方法取得了重大的成功。实际上有一些软件产品的可靠性是至关重要的,其整体或至少某个部分的失效是无法容忍的,或者是有广泛影响的。因此为了设计出无错的程序部件,净室软件工程有机结合了一些有坚实数学理论基础的严格的形式化规格说明、设计、验证工程方法。与其它方法不同之处在于它不是试图在完成设计后通过测试将软件中的错误检测出来,而是试图在被编译前至少在其进行测试前就通过数字证明,尽可能保证其正确性。
　　净室并不是一种专门的关键代码设计方法,它也不是表面上看上去的那样会增加成本。实际上,由于有效保障了质量,测试、排错,尤其是维护的成本会极大降低。净室软件工程的方法已经在许多工程应用中取得了成功。实践中,净室技术不仅是形式化方法,它还是若干成功的软件工程技术的有机结合,它不是某种单一的纯粹的形式化技术,而是一种降低成本,提高效费比的方法。在制造业的质量控制过程中,质量问题被尽可能地预先关注,而不是试图等到其引发某种后果,或依赖人为引发的某种后果来探察和排除问题来源。
　　可以说,质量自始至终被精心的度量和控制。净室方法就是以预防为优先的方法。经典的净室方法中,程序员在没有编译器的情况下进行程序设计,并以形式化的方法证明源代码的正确性。程序机制使用受到严格的限制,指针等被禁止使用。显然,对于很多非要害代码来说,采用这一方法的效率是非常低的。净室工程是以质量为核心的[1～3],围绕工程全过程的是其质量控制过程。其形式化的证明用于构造正确的设计,但这种正确是基于形式化断言间的一致性,它本身既不能确认代码与断言的一致,也不能确认断言与自然理解间的一致。另一方面,基于统计的质量控制过程的价值以被制造业大量验证。生产过程中的统计结果被直接用于工程过程的控制。
　　因而,基于测试统计的质量控制过程是十分必要的,尽管这种测试基本上是确认测试,而不是侦错测试。净室过程本身是旋进式的,质量控制的主体与形式化证明的主体应相互独立。即:需要独立的质量控制团队。严格的复核程序可以极大地提高软件的质量,这同样适用于净室方法。实践中可能有不同的具体形式,但净室工程中的各种一致性必须得到严格的复核。如黑盒与状态盒间的一致性等都须得到复核。形式化规格说明是净室工程至关重要的一环,它是一致性的基础。对于经典的净室方法,分析与设计必须采取形式化方法。实践中,形式化的程度可随具体项目而异。净室方法所用的结构描述工具主要有:黑盒、状态盒、白盒。