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

System Invariants and its Extracting in Z Specifications

作　　者：明继军[1] 朱关铭[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机工程与科学学院,上海201800

出　　处：《上海大学学报（自然科学版）》1999年第S1期135-141,共7页Journal of Shanghai University:Natural Science Edition

基　　金：国家自然科学基金(69773038);上海教委科技发展基金资助项目(97A12)

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

关 键 词：规格说明 系统不变式 系统状态空间 系统状态转换空间 操作空间 操作不变式 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]