Z語言

Z語言是一種用“數學文字”或“數學符號”來描述計算機系統的規範化語言，它不但能套用於計算機硬體系統，而且也特別適用於計算機軟體系統，Z語言描述“做什麼”而不涉及“怎么做”，只對目標軟體系統進行功能描述。實際上，Z語言僅僅是一套規定的數學符號，使用Z語言所寫的“程式”是對計算機軟體或硬體系統的一種抽象化設計。所以，利用Z語言寫出來的內容不是電腦程式，更不是可以編譯而生成能夠在計算機上運行的代碼。利用Z語言寫出來的內容不是讓計算機運行的，而是供人理解和分析的。用戶可以通過這些內容去理解計算機系統的模組、數據類型、過程、函式、對象、類等，進而對計算機系統的行為、結構、邏輯進行分析、驗證、改進、測試等。

形式化描述語言Z指的是著名數學家Zermelo，它是目前使用最廣泛的一種形式化描述語言，在軟體產業的一些大型項目中已經獲得成功的套用，Z以帶等詞的一階謂詞邏輯ZF（Zermelo-Fraenkel，蔡梅羅-弗蘭科爾）公理集合論為主要數學基礎。在Z中有兩種語言：數學語言和模式（Schema）語言。數學語言用來描述系統的各種特徵：對象及其之間的關係。模式語言是一種半圖形化的語言，它用來構造、組織形式化說明的描述、整理、封裝信息塊並對其命名以便可以重用這些信息塊。通常，形式化說明的可讀性都不太好，但由於Z採用半圖形化的模式語言，能用一種比較直觀、有條理的方式來表達形式化說明，這就改善了可讀性。

Z語言是由牛津大學程式設計研究小組開發的一種形式語言，之後該小組與IBM的Hursley實驗室合作，將Z語言用於IBM客戶信息控制系統(Customer Information and Control System,CICS)的開發，使得最終的產品質量得到了全面的提高，所監測出的錯誤數量大大減少，並且整體開發費用降低了9%。在ISO指導下的國際標準化Z工作於2002年完成。