Z规格说明的系统不变式及其抽取

System Invariants and its Extracting in Z Specifications

系统状态转换空间的系统不变式是整个系统状态转换空间中保持不变的状态属性,系统不变式的精确描述及其抽取使规格说明简洁,合理且可读性更强,同时可以使规格说明到可执行软件代码的转换容易实践,本文在讨论系统不变式的描述的基础上,提出一种新的系统不变式抽取的方法.

System variants in system state transferring space are state conditions which must be kept in all states of the space, the accurate description and extracting of system variants can not only make specifications concise, more reasonable and more readable than it was ,but also make the transfer from specifications to executable program code easy .In this paper, we'll illustrate a new way about the extracting of system variants based on the discussion of the description of system variants through a simple example about a book system.