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 бесплатно:
- стандарт общедоступен [10] с сайта ISO ITTF бесплатно и отдельно можно приобрести [10] с сайта ИСО;
- техническое исправление доступно [11] с сайта ISO бесплатно.
Награда [ править ]
В 1992 году вычислительная лаборатория Оксфордского университета была награждена Королевской премией за технологические достижения за совместную разработку с IBM в нотации Z. [12]
См. также [ править ]
- Группа пользователей Z (ZUG)
- Проект Community Z Tools (CZT)
- Другие формальные методы (и языки, использующие формальные спецификации ):
- ВДМ-СЛ , основная альтернатива Z
- B-метод , разработанный Жаном-Раймоном Абриалем (создателем обозначения Z)
- Z++ и Object-Z , расширения объектов для нотации Z.
- Alloy — язык спецификаций, вдохновленный нотацией Z и реализующий принципы Object Constraint Language (OCL).
- Verus, запатентованный инструмент, созданный компанией Compion, Шампейн, Иллинойс (позже приобретенный Motorola) для использования в проекте многоуровневой безопасности UNIX, впервые разработанном ее подразделением Addamax.
- Fastest — инструмент тестирования на основе моделей для нотации Z.
- Unified Modeling Language — инструмент моделирования проектирования программных систем от Object Management Group.
Ссылки [ править ]
- ^ Боуэн, Джонатан П. (2016). «Z-нотация: откуда причина и куда путь?» (PDF) . Инженерные надежные программные системы . Конспекты лекций по информатике . Том. 9506. Спрингер . стр. 103–151. дои : 10.1007/978-3-319-29628-9_3 . ISBN 978-3-319-29627-2 .
- ^ Абриал, Жан-Раймонд (1974), «Семантика данных», в Климби, JW; Коффеман, К.Л. (ред.), Материалы рабочей конференции ИФИП по управлению базами данных , Северная Голландия , стр. 1–59.
- ^ Хоар, Тони (2010). Поздравление Бертрану по случаю его шестидесятилетия (PDF) . Спрингер . п. 183. ИСБН 978-3-642-15187-3 .
{{cite book}}:|work=игнорируется ( помогите ) - ^ Мейер, Бертран ; Бодуан, Клод (1980), Методы программирования (на французском языке), Эйроль
- ^ Абриаль, Жан-Раймон; Шуман, Стивен А; Мейер, Бертран (1980), «Язык спецификации», в Макнахтене, AM; Маккиг, Р.М. (ред.), « О построении программ» , Cambridge University Press , ISBN 0-521-23090-Х (описывает раннюю версию языка).
- ^ Хугебум, Хендрик Ян. «Формальные методы в разработке программного обеспечения» (PDF) . Нидерланды: Лейденский университет . Проверено 14 апреля 2017 г.
- ^ Боуэн, Джонатан (июль 2022 г.). «Группа пользователей Z: тридцать лет спустя» (PDF) . ФАКТЫ ФАКС . № 2022–2. БКС-ФАКС . стр. 50–56 . Проверено 3 августа 2022 г.
- ^ Спиви, Дж. Майкл (1992). Обозначение Z: Справочное руководство . Международная серия по информатике (2-е изд.). Хемел Хемпстед: Прентис Холл . ISBN 978-0139785290 .
- ^ Корпела, Юкка К. «Объяснение Unicode: интернационализация документов, программ и веб-сайтов» . unicode-search.net . Проверено 24 марта 2020 г.
- ^ Перейти обратно: а б с «ИСО/МЭК 13568:2002» . Информационные технологии — Нотация формальной спецификации Z — Синтаксис, система типов и семантика ( архивированный PDF-файл ) . ИСО. 1 июля 2002 г. 196 стр.
- ^ Перейти обратно: а б «ИСО/МЭК 13568:2002/Кор.1:2007». Информационные технологии — Обозначения формальной спецификации Z — Синтаксис, система типов и семантика — Техническое исправление 1 (PDF) . ИСО. 15 июля 2007. 12 с.
- ^ «Королевская премия за технологические достижения 1992 года» . Вычислительная лаборатория Оксфордского университета . Архивировано из оригинала 2 декабря 2008 года . Проверено 17 октября 2021 г.
Дальнейшее чтение [ править ]
- Спайви, Джон Майкл (1992). Z-нотация: Справочное руководство . Международная серия по информатике (2-е изд.). Прентис Холл .
- Дэвис, Джим ; Вудкок, Джим (1996). Использование Z: спецификация, уточнение и доказательство . Международная серия по информатике. Прентис Холл. ISBN 0-13-948472-8 .
- Боуэн, Джонатан (1996). Формальная спецификация и документация с использованием Z: подход к тематическому исследованию . International Thomson Computer Press, International Thomson Publishing . ISBN 1-85032-230-9 .
- Джеки, Джонатан (1997). Путь Z: Практическое программирование формальными методами . Издательство Кембриджского университета . ISBN 0-521-55976-6 .
- Инс, округ Колумбия (1993). Введение в дискретную математику, формальную спецификацию системы и Z . Издательство Оксфордского университета . ISBN 9780198538370 .
ISO Стандарты по номеру стандарта |
|---|
| Базы данных органов управления : Национальные |
|---|
