Из Википедии, бесплатной энциклопедии
Перейти к навигации Перейти к поиску
Пример формальной спецификации (на испанском языке) с использованием обозначения Z.

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.

Ссылки [ править ]

  1. ^ Abrial, Жан-Раймон (1974), "Семантика данных", в Klimbie, JW; Коффеман К.Л. (ред.), Труды Рабочей конференции ИФИП по управлению базами данных , Северная Голландия , стр. 1–59.
  2. ^ Мейер, Бертран ; Бодуан, Клод (1980), Методы программирования (на французском языке), Eyrolles
  3. ^ Abrial, Жан-Раймон; Шуман, Стивен А; Мейер, Бертран (1980), «Язык спецификации», в Macnaghten, AM; Маккиг, RM (ред.), О построении программ , Cambridge University Press , ISBN 0-521-23090-X (описывает раннюю версию языка).
  4. ^ Hoogeboom, Хендрик Ян. «Формальные методы в разработке программного обеспечения» (PDF) . Нидерланды: Лейденский университет . Проверено 14 апреля 2017 года .
  5. ^ Корпела, Юкка К. «Объяснение Unicode: интернационализация документов, программ и веб-сайтов» . unicode-search.net . Проверено 24 марта 2020 года .
  6. ^ a b c «ISO / IEC 13568: 2002» . Информационные технологии - Нотация формальной спецификации Z - Синтаксис, система типов и семантика ( сжатый PDF-файл ) . ISO. 1 июля 2002 г. 196 с.
  7. ^ 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.