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. [12]

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

Рекомендации

  1. ^ Боуэн, Джонатан П. (2016). «Z-нотация: откуда причина и куда путь?» (PDF) . Инженерные надежные программные системы . Конспекты лекций по информатике . Том. 9506. Спрингер . стр. 103–151. дои : 10.1007/978-3-319-29628-9_3. ISBN 978-3-319-29627-2.
  2. ^ Абриал, Жан-Раймонд (1974), «Семантика данных», в Климби, JW; Коффеман, К.Л. (ред.), Материалы рабочей конференции ИФИП по управлению базами данных , Северная Голландия , стр. 1–59.
  3. ^ Хоар, Тони (2010). Поздравление Бертрану по случаю его шестидесятилетия (PDF) . Спрингер . п. 183. ИСБН 978-3-642-15187-3. {{cite book}}: |work=игнорируется ( помощь )
  4. ^ Мейер, Бертран ; Бодуан, Клод (1980), Методы программирования (на французском языке), Эйроль
  5. ^ Абриаль, Жан-Раймон; Шуман, Стивен А; Мейер, Бертран (1980), «Язык спецификации», в Макнахтене, AM; Маккиг, Р.М. (ред.), «О построении программ» , Cambridge University Press , ISBN 0-521-23090-Х(описывает раннюю версию языка).
  6. ^ Хугебум, Хендрик Ян. «Формальные методы в разработке программного обеспечения» (PDF) . Нидерланды: Лейденский университет . Проверено 14 апреля 2017 г.
  7. ^ Боуэн, Джонатан (июль 2022 г.). «Группа пользователей Z: тридцать лет спустя» (PDF) . ФАКТЫ ФАКС . № 2022–2. БКС-ФАКС . стр. 50–56 . Проверено 3 августа 2022 г.
  8. ^ Спиви, Дж. Майкл (1992). Обозначение Z: Справочное руководство . Международная серия по информатике (2-е изд.). Хемел Хемпстед: Прентис Холл . ISBN 978-0139785290.
  9. ^ Корпела, Юкка К. «Объяснение Unicode: интернационализация документов, программ и веб-сайтов». unicode-search.net . Проверено 24 марта 2020 г.
  10. ^ abc «ISO/IEC 13568:2002». Информационные технологии — Нотация формальной спецификации Z — Синтаксис, система типов и семантика ( архивированный PDF-файл ) . ИСО. 1 июля 2002 г. 196 стр.
  11. ^ ab «ISO/IEC 13568:2002/Cor.1:2007». Информационные технологии — Обозначения формальной спецификации Z — Синтаксис, система типов и семантика — Техническое исправление 1 (PDF) . ИСО. 15 июля 2007 г. 12 стр.
  12. ^ "Премия Королевы за технологические достижения 1992" . Вычислительная лаборатория Оксфордского университета . Архивировано из оригинала 2 декабря 2008 года . Проверено 17 октября 2021 г.

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