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

Пример формальной спецификации (на испанском языке) с использованием Z-нотации.

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.

использованная литература

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