Z语言（Z language），理学-计算机科学技术-计算机软件-软件语言与方法-软件语言，一种基于一阶谓词逻辑和集合论的形式规格说明语言，它适用于描述计算机软件系统，也可应用于计算机硬件系统。它采用严格的数学理论，可以产生简明、精确、无歧义且可证明的规格说明。Z语言（简称Z）本身是一种表示法，它用一套规定的数学符号按Z的语法来描述计算机系统，描述的是“做什么”而不涉及“怎么做”，只对目标系统进行功能描述。使用Z所写的形式规格说明是对计算机软件或硬件系统的一种抽象设计。所以，用它写出来的内容不是计算机程序，更不是可以编译而生成能够在计算机上运行的代码。它是供人理解和分析的。用户可以通过这些内容去理解计算机系统的模块、数据类型、过程、函数、对象等，进而对计算机系统的行为、结构、逻辑进行分析、证明、精化等。在Z中有两种语言：数学语言和模式（schema）语言。数学语言用各种数学符号来描述系统的各种特征：对象及其之间的关系。模式语言是一种半图形化的语言，用来构造、组织规格说明的描述，整理、封装信息块并对其命名，以便可以重用这些信息块。