科學出版社2015年6月，ISBN 978-7-03-044787-6。
Z語言是軟件工程中對軟件的需求、功能、規格進行精確無誤并且可以推理和證明的描述語言，它將事物的狀態和行為用數學符號來形式化地進行表達，為編寫計算機程序和驗證計算機程序的正確性提供邏輯和理論依據。所以，Z語言是軟件工程中編碼之前的規格說明語言。本書是根據作者自20世紀90年代初至今在國內外高校所從事的軟件工程教學和科研工作的經驗，結合在我國載人航天和深空探測工程中三維可視化系統的設計、研發、使用過程中的體會，針對軟件工程中的形式描述這一環節編寫而成。書中的第1章至第7章包括了Z語言的基本數學概念、集合、命題、模式、函數、謂詞、關系等內容；第8章介紹了使用Z語言的簡單實例；第9章介紹了常用的Z語言描述工具及其使用方法；第10章是關于生成Z語言形式描述文檔的一個工具及說明。書中的內容以最簡單的語言進行表達，并且對大量的數學概念和專業技術進行了通俗地說明。
本書適合做初學者的Z語言教材和軟件工程技術人員以及管理人員的參考工具書。
http://www.abook.cn/showproduct.asp?id=5453