Z-нотация

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

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

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

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

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

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

ПримечанияПравить

↑ 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
↑ GoldenWeb.it — Free True Type Fonts download — Zed.ttf (неопр.). Дата обращения: 7 ноября 2008. Архивировано 13 ноября 2007 года.
↑ Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (англ.). — ISO/IEC 13568:2002. — 2002. — P. 196.
↑ Duke, R. , & Rose, G. (2000). Formal object oriented specification using object-z. Cornerstones of Computing. Macmillan.

ЛитератураПравить

J. Michael Spivey. The Z Notation: a reference manual (неопр.). — 2nd edition. — Prentice Hall International Series in Computer Science, 1992. Архивная копия от 9 октября 2008 на Wayback Machine
Jim Davies and Jim Woodcock. Using Z: Specification, Refinement and Proof (англ.). — Prentice Hall International Series in Computer Science, 1996. — ISBN 0-13-948472-8. Архивная копия от 27 июня 2009 на Wayback Machine
Jonathan Bowen. Formal Specification and Documentation using Z: A Case Study Approach (англ.). — International Thomson Computer Press, 1996. — ISBN 1-85032-230-9. Архивная копия от 9 апреля 2010 на Wayback Machine
Jonathan Jacky. The Way of Z: Practical Programming with Formal Methods (англ.). — Cambridge University Press, 1997. — ISBN 0-521-55976-6.

[1] 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

[2] GoldenWeb.it — Free True Type Fonts download — Zed.ttf (неопр.). Дата обращения: 7 ноября 2008. Архивировано 13 ноября 2007 года.

[3] Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics (англ.). — ISO/IEC 13568:2002. — 2002. — P. 196.

[4] Duke, R. , & Rose, G. (2000). Formal object oriented specification using object-z. Cornerstones of Computing. Macmillan.

[1]

[2]

[3]

[4]