Z обозначение / Z ɛ д / представляет собой формальный язык спецификаций используются для описания и моделирования вычислительных систем. Он нацелен на четкую спецификацию компьютерных программ и компьютерных систем в целом.
История [ править ]
В 1974 году Жан-Раймон Абриаль опубликовал «Семантику данных». [1] Он использовал нотацию, которая позже будет преподаваться в Университете Гренобля до конца 1980-х годов. В то время как в EDF ( Électricité de France ), Абриаль писал внутренние заметки о Z. [ необходима ссылка ] Обозначение Z используется в книге 1980 года « Методы программирования» . [2]
Z был первоначально предложен Абриалом в 1977 году с помощью Стива Шумана и Бертрана Мейера . [3] Он получил дальнейшее развитие в исследовательской группе программирования в Оксфордском университете , где Абриаль работал в начале 1980-х, прибыв в Оксфорд в сентябре 1979 года.
Абриаль сказал, что Z назван так: «Потому что это высший язык!» [4], хотя название « Цермело » также связано с обозначением Z благодаря использованию теории множеств Цермело – Френкеля .
Использование и обозначения [ править ]
Z основан на стандартных математических обозначениях, используемых в аксиоматической теории множеств , лямбда-исчислении и логике предикатов первого порядка . Все выражения в Z-нотации являются типизированными , что позволяет избежать некоторых парадоксов наивной теории множеств . Z содержит стандартизированный каталог (называемый математическим инструментарием ) часто используемых математических функций и предикатов, определенных с помощью самого Z.
Поскольку в нотации Z (как и в языке APL задолго до него) используется множество символов, отличных от ASCII , спецификация включает предложения по отображению символов нотации Z в ASCII и LaTeX . Также существуют кодировки Unicode для всех стандартных Z-символов. [5]
Стандарты [ править ]
ISO завершила работу по стандартизации Z в 2002 году. Этот стандарт [6] и техническое исправление [7] доступны по ссылке бесплатно:
- стандарт находится в открытом доступе [6] на сайте ISO ITTF бесплатно и, отдельно, доступен для покупки [6] на сайте ISO;
- техническое исправление доступно [7] бесплатно на сайте ISO.
См. Также [ править ]
- Группа пользователей Z (ZUG)
- Проект Community Z Tools (CZT)
- Другие формальные методы (и языки, использующие формальные спецификации ):
- FDM (формальная методология разработки), основанная на подъязыках спецификации Ina Jo и Ina Flo, довольно популярная в 1980-х и 1990-х годах.
- VDM-SL , основная альтернатива Z
- B-метод , разработанный Жаном-Раймоном Абриалом (создателем Z-нотации)
- Z ++ и Object-Z : объектные расширения для обозначения Z
- Alloy , язык спецификаций, вдохновленный нотацией Z и реализующий принципы языка объектных ограничений (OCL).
- Verus, проприетарный инструмент, созданный Compion, Champaign, Illinois (позже приобретенный Motorola), для использования в проекте многоуровневой защиты UNIX, впервые разработанном его подразделением Addamax.
- Fastest - это инструмент тестирования на основе моделей для обозначения Z.
Ссылки [ править ]
- ^ Abrial, Жан-Раймон (1974), "Семантика данных", в Klimbie, JW; Коффеман К.Л. (ред.), Труды Рабочей конференции ИФИП по управлению базами данных , Северная Голландия , стр. 1–59.
- ^ Мейер, Бертран ; Бодуан, Клод (1980), Методы программирования (на французском языке), Eyrolles
- ^ Abrial, Жан-Раймон; Шуман, Стивен А; Мейер, Бертран (1980), «Язык спецификации», в Macnaghten, AM; Маккиг, RM (ред.), О построении программ , Cambridge University Press , ISBN 0-521-23090-X (описывает раннюю версию языка).
- ^ Hoogeboom, Хендрик Ян. «Формальные методы в разработке программного обеспечения» (PDF) . Нидерланды: Лейденский университет . Проверено 14 апреля 2017 года .
- ^ Корпела, Юкка К. «Объяснение Unicode: интернационализация документов, программ и веб-сайтов» . unicode-search.net . Проверено 24 марта 2020 года .
- ^ a b c «ISO / IEC 13568: 2002» . Информационные технологии - Нотация формальной спецификации Z - Синтаксис, система типов и семантика ( сжатый PDF-файл ) . ISO. 1 июля 2002 г. 196 с.
- ^ a b «ISO / IEC 13568: 2002 / Cor.1: 2007». Информационные технологии - Нотация формальной спецификации Z - Синтаксис, система типов и семантика - Техническое исправление 1 (PDF) . ISO. 15 июля 2007 г. 12 стр.
Дальнейшее чтение [ править ]
- Спайви, Джон Майкл (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.