基于设计决定的逐步求精方法及环境

逐步描述、变换及证明的软件开发过程包含两个转换,一是从非形式的用户需求到形式描述,一是从形式描述到算法实现。开发过程中的关键是如何做出设计决定。为了更好地维护、重用软件以及程序证明,不仅仅要对软件的形式描述及实现做文档记录,也要记下开发过程中所做的每一步决定。我们用两个例子来说明如上这种逐步求精的方法以及设计决定在其中所起的作用,并且我们实现了一个包括spec、oomm、prot、veri几个子系统组成的环境来支持上述过程。