Обозначение Z - Z notation
Z обозначение / Z ɛ д / представляет собой формальный язык спецификаций используются для описания и моделирования вычислительных систем. Он нацелен на четкую спецификацию компьютерных программ и компьютерных систем в целом.
История
В 1974 году Жан-Раймон Абриаль опубликовал «Семантику данных». Он использовал нотацию, которая позже будет преподаваться в Университете Гренобля до конца 1980-х годов. Находясь в EDF ( Électricité de France ), Абриаль писал внутренние примечания по Z. Обозначение Z используется в книге 1980 года « Методы программирования» .
Z был первоначально предложен Абриалом в 1977 году с помощью Стива Шумана и Бертрана Мейера . Дальнейшее развитие он получил в исследовательской группе программирования в Оксфордском университете , где Абриаль работал в начале 1980-х, прибыв в Оксфорд в сентябре 1979 года.
Абриаль сказал, что Z назван так: «Потому что это высший язык!» хотя название « Цермело » также связано с обозначением Z благодаря использованию теории множеств Цермело – Френкеля .
Использование и обозначения
Z основан на стандартных математических обозначениях, используемых в аксиоматической теории множеств , лямбда-исчислении и логике предикатов первого порядка . Все выражения в обозначении Z являются типизированными , что позволяет избежать некоторых парадоксов наивной теории множеств . Z содержит стандартизированный каталог (называемый математическим инструментарием ) часто используемых математических функций и предикатов, определенных с помощью самого Z.
Поскольку в нотации Z (как и в языке APL задолго до него) используется множество символов, отличных от ASCII , спецификация включает предложения по отображению символов нотации Z в ASCII и LaTeX . Также существуют кодировки Unicode для всех стандартных Z-символов.
Стандарты
ИСО завершила работу по стандартизации Z в 2002 году. Этот стандарт и технические исправления доступны бесплатно в ISO:
- стандарт находится в открытом доступе на сайте ISO ITTF бесплатно и, отдельно, доступен для покупки на сайте ISO;
- технические исправления доступны на сайте ISO бесплатно.
Награда
В 1992 году « Ее Величество Королева [была] любезно рада утвердить рекомендацию премьер-министра о присуждении в этом году Премии Королевы за технологические достижения вычислительной лаборатории Оксфордского университета . Вычислительная лаборатория Оксфордского университета [получила] награду совместно с IBM United Kingdom Laboratories Limited за разработку метода программирования, основанного на элементарной теории множеств и логики, известного как нотация Z , и его применение в продукте IBM Customer Information Control System (CICS) . »
Смотрите также
- Группа пользователей 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.
использованная литература
дальнейшее чтение
- Спайви, Джон Майкл (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.