Обозначение 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:
В 1992 году вычислительная лаборатория Оксфордского университета была награждена Королевской премией за технологические достижения за совместную разработку с IBM в нотации Z. [12]
{{cite book}}
: |work=
игнорируется ( помощь )