Z-нотация | это... Что такое Z-нотация? (original) (raw)

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

Z-нотацию первоначально предложил Жан-Реймон Абриаль (Jean-Raymond Abrial) в 1977 году при участии Стива Шумана (Steve Schuman) и Бертранда Мейера (Bertrand Meyer)[1]

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

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

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

Ссылки

  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
  3. ↑ Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics. — ISO/IEC 13568:2002. — P. 196.

Литература