Z-нотация

Не следует путать с z-преобразованием — (свёртка временно́го сигнала в частотную область).

Z-нота́ция (англ. Z notation, произносится /zɛd/) — формальный язык спецификации, используемый для описания и моделирования программ и их формальной верификации.

Предложена Жан-Реймоном Абриалем (Jean-Raymond Abrial) в 1977 году, в разработке участвовали Стив Шуман (Steve Schuman) и Бертран Мейер (Bertrand Meyer)^[1].

Основана на стандартной математической нотации, используемой в аксиоматической теории множеств, лямбда-исчислении и логике предикатов первого порядка. Допустимые выражения в Z-нотации подобраны таким образом, чтобы избегать парадоксов аксиоматической теории множеств. Также содержит стандартизированный каталог часто используемых математических функций и предикатов.

Хотя в нотации используется много символов вне набора ASCII, спецификация допускает запись выражений целиком в ASCII или посредством LaTeX, существует специализированный шрифт для её поддержки (Z ttf font)^[2].

В 2002 году Международная организация по стандартизации завершила процесс по стандартизации Z-нотации^[3].

Существует объектно-ориентированное расширение Object-Z^{[англ.][4]}.