附錄C（資料性附錄）Z語言示例

Z語言的基本單位是模式。它分成說明部分和謂詞部分。說明部分定義了一些狀態或模式變量；謂詞部分是一般的謂詞公式，它給出了變量間的限定關系。模式可定義系統的狀態空間、初始狀態和狀態變換。另外，在Z中要使用到一些全程變量和常量，也是通過聲明部分和謂詞部分加以定義。

下面以本標準7.2.1的AssignUser模式來舉例說明其含義。該模式名稱為AssignUser，其參數為來自域NAME的user和role。模式的第2行給出了變量的定義域和其需要滿足的約束條件，這構成了模式的說明部分。剩余的內容構成了模式的謂詞部分，它定義了在該模式執行前后，變量UA和assigned_users的新舊值之間各自需要滿足的約束。