stringtranslate.com

Z-обозначение

Пример формальной спецификации (на испанском языке) с использованием нотации Z, с именованными блоками схемы, включая декларации и предикаты

Нотация Z / ˈ z ɛ d / — это формальный язык спецификаций, используемый для описания и моделирования вычислительных систем. [1] Он нацелен на четкую спецификацию компьютерных программ и компьютерных систем в целом.

История

В 1974 году Жан-Раймон Абриаль опубликовал «Семантику данных». [2] Он использовал нотацию, которая позже преподавалась в Университете Гренобля до конца 1980-х годов. Работая в EDF ( Électricité de France ), работая с Бертраном Мейером , Абриаль также работал над разработкой Z. [3] Нотация Z используется в книге 1980 года «Методы программирования» . [4]

Первоначально Z был предложен Абриалом в 1977 году с помощью Стива Шумана и Бертрана Мейера . [5] Он был доработан в группе исследований программирования в Оксфордском университете , где Абриал работал в начале 1980-х годов, прибыв в Оксфорд в сентябре 1979 года.

Абриаль сказал, что Z так назван, «потому что это высший язык!» [6], хотя название « Цермело » также связано с обозначением Z из-за использования в нем теории множеств Цермело–Френкеля .

В 1992 году была создана Группа пользователей Z (ZUG) для надзора за деятельностью, касающейся нотации Z, особенно за встречами и конференциями. [7]

Использование и обозначения

Z основан на стандартной математической нотации, используемой в аксиоматической теории множеств , лямбда-исчислении и логике предикатов первого порядка . [8] Все выражения в нотации Z типизированы , что позволяет избежать некоторых парадоксов наивной теории множеств . Z содержит стандартизированный каталог (называемый математическим инструментарием ) часто используемых математических функций и предикатов, определенных с использованием самой Z. Он дополнен блоками схем Z , которые можно комбинировать с использованием их собственных операторов, основанных на стандартных логических операторах, а также путем включения схем в другие схемы. Это позволяет встраивать спецификации Z в большие спецификации удобным образом.

Поскольку нотация Z (как и язык APL , задолго до него) использует много не- ASCII символов, спецификация включает предложения по отображению символов нотации Z в ASCII и в LaTeX . Существуют также кодировки Unicode для всех стандартных символов Z. [9]

Стандарты

ISO завершила работу по стандартизации Z в 2002 году. Этот стандарт [10] и техническая поправка [11] доступны бесплатно на сайте ISO:

Награда

В 1992 году Вычислительная лаборатория Оксфордского университета и IBM совместно были награждены Королевской премией за технологические достижения «за разработку... нотации Z и ее применение в продукте IBM Customer Information Control System ( CICS )». [12]

Смотрите также

Ссылки

  1. ^ Боуэн, Джонатан П. (2016). «Нотация Z: откуда причина и куда курс?» (PDF) . Инженерные надежные программные системы . Конспект лекций по информатике . Том 9506. Springer . С. 103–151. doi :10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2.
  2. ^ Абриаль, Жан-Раймонд (1974), «Семантика данных», в Климби, Дж. В.; Коффеман, К. Л. (ред.), Труды рабочей конференции IFIP по управлению базами данных , Северная Голландия , стр. 1–59
  3. ^ Хоар, Тони (2010). Поздравления Бертрану по случаю его шестидесятилетия (PDF) . Springer . стр. 183. ISBN 978-3-642-15187-3. {{cite book}}: |work=проигнорировано ( помощь )
  4. ^ Мейер, Бертран ; Бодуан, Клод (1980), Методы программирования (на французском языке), Eyrolles
  5. ^ Абриаль, Жан-Раймон; Шуман, Стивен А; Мейер, Бертран (1980), «Язык спецификаций», в Macnaghten, AM; McKeag, RM (ред.), О построении программ , Cambridge University Press , ISBN 0-521-23090-X(описывает раннюю версию языка).
  6. ^ Хугебум, Хендрик Ян. «Формальные методы в разработке программного обеспечения» (PDF) . Нидерланды: Лейденский университет . Проверено 14 апреля 2017 г.
  7. ^ Боуэн, Джонатан (июль 2022 г.). «Группа пользователей Z: тридцать лет спустя» (PDF) . ФАКТЫ FACS . № 2022–2. BCS-FACS . стр. 50–56 . Получено 3 августа 2022 г. .
  8. ^ Spivey, J. Michael (1992). Z Notation: A Reference Manual . International Series in Computer Science (2nd ed.). Hemel Hempstead: Prentice Hall . ISBN 978-0139785290.
  9. ^ Корпела, Юкка К. «Объяснение Unicode: интернационализация документов, программ и веб-сайтов». unicode-search.net . Получено 24 марта 2020 г. .
  10. ^ abc "ISO/IEC 13568:2002". Информационные технологии — Формальная спецификация нотации Z — Синтаксис, система типов и семантика ( Zipped PDF ) . ISO. 1 июля 2002 г. 196 стр.
  11. ^ ab "ISO/IEC 13568:2002/Cor.1:2007". Информационные технологии — Нотация формальной спецификации Z — Синтаксис, система типов и семантика — Техническое исправление 1 (PDF) . ISO. 15 июля 2007 г. 12 стр.
  12. ^ "The Queen's Award for Technological Achievement 1992". Oxford University Computing Laboratory . Архивировано из оригинала 2 декабря 2008 года . Получено 17 октября 2021 года .

Дальнейшее чтение