关于Z规格说明语言中模式的剖析  

Dissection of Schema in Z Specification Language

作　　者：高晓雷[1] 缪淮扣[1] 

机构地区：[1]上海大学计算机科学系,上海嘉定201800

出　　处：《计算机科学》1998年第6期24-27,共4页Computer Science

基　　金：国家自然科学基金(编号:69773038);上海市教委科技发展基金(编号:97A42)

摘　　要：1.引言形式规格说明语言一般是提供一套称为语法域的记号系统和一个称为语义域的对象集合,以及一组精确地定义哪些对象满足哪个规格说明的规则。规格说明是语法域中的句子。它用数学表示法精确地描述了软件系统必须具备的性质。 Z是目前比较流行的一种形式规格说明语言。This paper analys the state schema, operation schema. initial state schema and state invariant in Z language, instantiates their function, and shows the relation among them by way of an example. Finally it points out that the automatic extracting of state invariant is impossible.

关 键 词：规格说明语言 形式语言 Z语言 模式 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]