繆淮扣、陳怡海編寫的《軟件形式規格說明語言—Z》是普通高等教育“十一五”***規劃教材。教材共分**2章，內容包括：緒論，一階邏輯與集合論，Z的類型與構造單元，關繫和函數，模式和規格說明，序列和包，規格說明的實例，Z規格說明的形式推理，Z規格說明的若干推理實例，從規格說明到程序，Object—Z規格說明語言，形式方法及其工具。
本書各章都配有習題。附錄A給出了Z的語法；附錄B給出了Object—Z的語法；附錄C給出了部分習題解答。

形式方法是一種基於數學的軟件開發方法。形式規格說明是形式方法最 基本的部分，它精確描述用 戶需求和計算機軟件繫統的功能，並用於軟件驗證和精化。Z是目前頗受歡 迎且使用較廣泛的一種形式 規格說明語言。繆淮扣、陳怡海編寫的《軟件形式規格說明語言—Z》旨在 討論軟件工程中形式方法的概念、方法和表示法，並詳細介紹Z的類型繫統 、數 學語言和公理定義、通用式定義、模式等結構，還討論了Z規格說明的推理 和求精方法。《軟件形式規格說明語言—Z》還介紹了面 向對像的規格說明語言Object—Z和其他形式方法表示和工具。全書結構合 理、內容豐富、實例詳盡多樣。 各章配有習題。 《軟件形式規格說明語言—Z》可作為計算機、軟件工程、信息安全和 信息管理等專業本科生和研究生的教材，也可作為大專院 校有關專業的教師參考書，還可作為從事軟件工程、軟件開發和軟件應用的 研究人員和技術人員的參考 資料。

第1章 緒論
第2章 一階邏輯與集合論
第3章 Z的類型與構造單元
第4章 關繫和函數
第5章 模式和規格說明
第6章 序列和包
第7章 規格說明的實例
第8章 Z規格說明的形式推理
第9章 Z規格說明的若干推理實例
**0章 從規格說明到程序
**1章 Object—Z規格說明語言
**2章 形式方法及其工具
附錄A Z語法
附錄B Z語言術語
附錄C Object—Z語法
附錄D 部分習題解答
參考文獻