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

1.引言形式规格说明语言一般是提供一套称为语法域的记号系统和一个称为语义域的对象集合,以及一组精确地定义哪些对象满足哪个规格说明的规则。规格说明是语法域中的句子。它用数学表示法精确地描述了软件系统必须具备的性质。 Z是目前比较流行的一种形式规格说明语言,它以一阶谓词逻