A Rigorous Specification Technique for High Quality Software

摘要

Too many software projects fail. One important reason, though not the only one, is the absence of a good specification. Specifications should be complete, consistent, comprehensible, and correct. Correctness can only be demonstrated if the specification is formal (so that reasoning can be supported); but the associated use of a formal language seriously reduces user comprehension, so there is a conflict between these two properties. We contend that formal methods should be used but that their use should be totally concealed and automated, so that users are unaware of the underlying formality. We have constructed a specification toolset, called CREATIV, which embodies this approach. The use of formal methods mandates a scientific approach. One possible approach is to formalise specification knowledge as an axiomatic system. The CREATIV toolset uses a new model and a new definition of the specification process, together with an axiomatic theory to support specification knowledge. All operations in the system are provable and traceable; we have built the reasoning component of the CREATIV toolset on the basis of this theory. We have used the toolset for specification on a range of projects. More recently, we have used it on a small number of government projects. We report on some of the advantages of its use, and offer some preliminary comments on a comparative specification exercise.