Abstract: Proof and test are two ways to check specification, and they are complementary. Aiming at the problem that specification is difficult to be proofed, this paper proposes the theory of completeness test of states space. The concepts of constructed function and constrained states space are used. The test approach used to detect the existing of initial state in Z specifications language is discussed, and the feasibility of this approach is proved by application example.

Key words: Z specification, constrained state space, initial state, invariant

摘要： 证明和测试是验证规格说明是否正确的2种方法，两者互为补充。针对软件规格说明难以证明的问题，提出对状态空间进行完备性测试的理论。采用构造函数和受限状态空间的概念，讨论用于测试Z规格说明语言初始状态存在性的方法，通过实例证明该方法的可行性。

关键词: Ｚ规格说明, 受限状态空间, 初始状态, 不变式

CLC Number: 

• TP301.6