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

Dissection of Schema in Z Specification Language

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.