Z-нота́ция (, произносится /zɛd/) — формальный язык спецификации, используемый для описания и моделирования программ и их формальной верификации.
Предложена Жан-Реймоном Абриалем (Jean-Raymond Abrial) в 1977 году, в разработке участвовали Стив Шуман (Steve Schuman) и Бертран Мейер (Bertrand Meyer)Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer: A Specification Language, in On the Construction of Programs, Cambridge University Press, eds. A. M. Macnaghten and R. M. McKeag, 1980 (describes early version of the language). ISBN 0-521-23090-X.
Основана на стандартной математической нотации, используемой в аксиоматической теории множеств, лямбда-исчислении и логике предикатов первого порядка. Допустимые выражения в Z-нотации подобраны таким образом, чтобы избегать парадоксов аксиоматической теории множеств. Также содержит стандартизированный каталог часто используемых математических функций и предикатов.
Хотя в нотации используется много символов вне набора ASCII, спецификация допускает запись выражений целиком в ASCII или посредством LaTeX, существует специализированный шрифт для её поддержки (Z ttf font).
В 2002 году Международная организация по стандартизации завершила процесс по стандартизации Z-нотации.
Существует объектно-ориентированное расширение Duke, R. , & Rose, G. (2000). Formal object oriented specification using object-z. Cornerstones of Computing. Macmillan..
Примечания
Литература
Категория:Языки спецификаций