论文部分内容阅读
随着现代社会的发展，计算机系统对人们的生活和工作所带来的影响越来越大，计算机软件系统的失误带来的潜在危险和损失也大大增加了。另一方面，软件的规模和复杂性不断扩大，使得传统的软件开发方法很难保证软件的正确性和开发效率。这些情况说明，软件开发需要从朴素的，非形式设计方法向更严格、更形式化的方向转变。
在本文中，我们尝试将“规范”和“精化”这两个具有清晰严格数学基础的概念引入到软件开发的过程中。于是，我们的软件开发流程可以变为：首先从一个具有严格语法和语义，完全描述了软件设计目标和任务的规范出发，通过一系列保证语义的精化步骤对规范进行变换，在精化过程中逐渐去掉规范中的抽象部分，构造出更多计算机可执行的细节代码，最终得到满足要求的可运行程序。
由于上述精化工作显得比较繁琐和冗长，为了能实际地使用这种开发方法，必须有辅助工具的支持。在本论文的工作中，我们尝试设计并实现了一个原型辅助系统，用于帮助人们采用上述形式化开发方法进行程序开发工作。