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

Обозначение 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 бесплатно:

стандарт общедоступен ^{[ 10 ]} с сайта ISO ITTF бесплатно и отдельно можно приобрести ^{[ 10 ]} с сайта ИСО;
техническое исправление доступно ^{[ 11 ]} с сайта ISO бесплатно.

Премия

В 1992 году вычислительная лаборатория Оксфордского университета и компания IBM были совместно награждены Королевской премией за технологические достижения «за разработку… нотации Z и ее применение в продукте IBM Customer Information Control System ( CICS )». ^{[ 12 ]}

См. также

Группа пользователей Z (ZUG)
Community Z Tools (CZT) Проект
Другие формальные методы (и языки, использующие формальные спецификации ):
- ВДМ-СЛ , основная альтернатива Z
- B-метод , разработанный Жаном-Раймоном Абриалем (создателем обозначения Z)
- Z++ и Object-Z , расширения объектов для нотации Z.
- Alloy — язык спецификаций, вдохновленный нотацией Z и реализующий принципы Object Constraint Language (OCL).
- Verus, запатентованный инструмент, созданный компанией Compion, Шампейн, Иллинойс (позже приобретенный Motorola) для использования в проекте многоуровневой безопасности UNIX, впервые разработанном ее подразделением Addamax.
Fastest — инструмент тестирования на основе моделей для нотации Z.
Unified Modeling Language — инструмент моделирования проектирования программных систем от Object Management Group.

Ссылки

^ Боуэн, Джонатан П. (2016). «Z-нотация: откуда причина и куда путь?» (PDF) . Инженерные надежные программные системы . Конспекты лекций по информатике . Том. 9506. Спрингер . стр. 103–151. дои : 10.1007/978-3-319-29628-9_3 . ISBN 978-3-319-29627-2 .
^ Абриал, Жан-Раймонд (1974), «Семантика данных», в Климби, JW; Коффеман, К.Л. (ред.), Материалы рабочей конференции ИФИП по управлению базами данных , Северная Голландия , стр. 1–59.
^ Хоар, Тони (2010). Поздравление Бертрану по случаю его шестидесятилетия (PDF) . Спрингер . п. 183. ИСБН 978-3-642-15187-3 . {{cite book}}: |work= игнорируется ( помогите )
^ Мейер, Бертран ; Бодуан, Клод (1980), Методы программирования (на французском языке), Эйроль
^ Абриаль, Жан-Раймон; Шуман, Стивен А; Мейер, Бертран (1980), «Язык спецификации», в Макнахтене, AM; Маккиг, Р.М. (ред.), «О построении программ» , Cambridge University Press , ISBN 0-521-23090-Х (описывает раннюю версию языка).
^ Хугебум, Хендрик Ян. «Формальные методы в разработке программного обеспечения» (PDF) . Нидерланды: Лейденский университет . Проверено 14 апреля 2017 г.
^ Боуэн, Джонатан (июль 2022 г.). «Группа пользователей Z: тридцать лет спустя» (PDF) . ФАКТЫ ФАКС . № 2022–2. БКС-ФАКС . стр. 50–56 . Проверено 3 августа 2022 г.
^ Спиви, Дж. Майкл (1992). Обозначение Z: Справочное руководство . Международная серия по информатике (2-е изд.). Хемел Хемпстед: Прентис Холл . ISBN 978-0139785290 .
^ Корпела, Юкка К. «Объяснение Unicode: интернационализация документов, программ и веб-сайтов» . unicode-search.net . Проверено 24 марта 2020 г.
^ Перейти обратно: ^а ^б ^с «ИСО/МЭК 13568:2002» . Информационные технологии — Нотация формальной спецификации Z — Синтаксис, система типов и семантика ( архивированный PDF-файл ) . ИСО. 1 июля 2002 г. 196 стр.
^ Перейти обратно: ^а ^б «ИСО/МЭК 13568:2002/Кор.1:2007». Информационные технологии — Обозначения формальной спецификации Z — Синтаксис, система типов и семантика — Техническое исправление 1 (PDF) . ИСО. 15 июля 2007. 12 с.
^ «Королевская премия за технологические достижения 1992 года» . Вычислительная лаборатория Оксфордского университета . Архивировано из оригинала 2 декабря 2008 года . Проверено 17 октября 2021 г.

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

Спайви, Джон Майкл (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 .
Инс, округ Колумбия (1993). Введение в дискретную математику, формальную спецификацию системы и Z . Издательство Оксфордского университета . дои : 10.1093/oso/9780198538370.001.0001 . ISBN 9780198538370 .

[1] Боуэн, Джонатан П. (2016). «Z-нотация: откуда причина и куда путь?» (PDF) . Инженерные надежные программные системы . Конспекты лекций по информатике . Том. 9506. Спрингер . стр. 103–151. дои : 10.1007/978-3-319-29628-9_3 . ISBN 978-3-319-29627-2 .

[2] Абриал, Жан-Раймонд (1974), «Семантика данных», в Климби, JW; Коффеман, К.Л. (ред.), Материалы рабочей конференции ИФИП по управлению базами данных , Северная Голландия , стр. 1–59.

[3] Хоар, Тони (2010). Поздравление Бертрану по случаю его шестидесятилетия (PDF) . Спрингер . п. 183. ИСБН 978-3-642-15187-3 . {{cite book}}: |work= игнорируется ( помогите )

[4] Мейер, Бертран ; Бодуан, Клод (1980), Методы программирования (на французском языке), Эйроль

[5] Абриаль, Жан-Раймон; Шуман, Стивен А; Мейер, Бертран (1980), «Язык спецификации», в Макнахтене, AM; Маккиг, Р.М. (ред.), «О построении программ» , Cambridge University Press , ISBN 0-521-23090-Х (описывает раннюю версию языка).

[6] Хугебум, Хендрик Ян. «Формальные методы в разработке программного обеспечения» (PDF) . Нидерланды: Лейденский университет . Проверено 14 апреля 2017 г.

[zug22-7] Боуэн, Джонатан (июль 2022 г.). «Группа пользователей Z: тридцать лет спустя» (PDF) . ФАКТЫ ФАКС . № 2022–2. БКС-ФАКС . стр. 50–56 . Проверено 3 августа 2022 г.

[8] Спиви, Дж. Майкл (1992). Обозначение Z: Справочное руководство . Международная серия по информатике (2-е изд.). Хемел Хемпстед: Прентис Холл . ISBN 978-0139785290 .

[9] Корпела, Юкка К. «Объяснение Unicode: интернационализация документов, программ и веб-сайтов» . unicode-search.net . Проверено 24 марта 2020 г.

[Standard-10] Перейти обратно: ^а ^б ^с «ИСО/МЭК 13568:2002» . Информационные технологии — Нотация формальной спецификации Z — Синтаксис, система типов и семантика ( архивированный PDF-файл ) . ИСО. 1 июля 2002 г. 196 стр.

[Corrigendum-11] Перейти обратно: ^а ^б «ИСО/МЭК 13568:2002/Кор.1:2007». Информационные технологии — Обозначения формальной спецификации Z — Синтаксис, система типов и семантика — Техническое исправление 1 (PDF) . ИСО. 15 июля 2007. 12 с.

[12] «Королевская премия за технологические достижения 1992 года» . Вычислительная лаборатория Оксфордского университета . Архивировано из оригинала 2 декабря 2008 года . Проверено 17 октября 2021 г.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

v т и ISO Стандарты по номеру стандарта
List of ISO standards – ISO romanizations – IEC standards
1–9999	1 2 3 4 6 7 9 16 17 31 -0 -1 -3 -4 -5 -6 -7 -8 -9 -10 -11 -12 -13 68-1 128 216 217 226 228 233 259 261 262 302 306 361 500 518 519 639 -1 -2 -3 -5 -6 646 657 668 690 704 732 764 838 843 860 898 965 999 1000 1004 1007 1073-1 1073-2 1155 1413 1538 1629 1745 1989 2014 2015 2022 2033 2047 2108 2145 2146 2240 2281 2533 2709 2711 2720 2788 2848 2852 2921 3029 3103 3166 -1 -2 -3 3297 3307 3601 3602 3864 3901 3950 3977 4031 4157 4165 4217 4909 5218 5426 5427 5428 5725 5775 5776 5800 5807 5964 6166 6344 6346 6373 6385 6425 6429 6438 6523 6709 6943 7001 7002 7010 7027 7064 7098 7185 7200 7498 -1 7637 7736 7810 7811 7812 7813 7816 7942 8000 8093 8178 8217 8373 8501-1 8571 8583 8601 8613 8632 8651 8652 8691 8805/8806 8807 8820-5 8859 -1 -2 -3 -4 -5 -6 -7 -8 -8-I -9 -10 -11 -12 -13 -14 -15 -16 8879 9000/9001 9036 9075 9126 9141 9227 9241 9293 9314 9362 9407 9496 9506 9529 9564 9592/9593 9594 9660 9797-1 9897 9899 9945 9984 9985 9995
10000–19999	10006 10007 10116 10118-3 10160 10161 10165 10179 10206 10218 10279 10303 -11 -21 -22 -28 -238 10383 10585 10589 10628 10646 10664 10746 10861 10957 10962 10967 11073 11170 11172 11179 11404 11544 11783 11784 11785 11801 11889 11898 11940 (-2) 11941 11941 (TR) 11992 12006 12052 12182 12207 12234-2 12620 13211 -1 -2 13216 13250 13399 13406-2 13450 13485 13490 13567 13568 13584 13616 13816 13818 14000 14031 14224 14289 14396 14443 14496 -2 -3 -6 -10 -11 -12 -14 -17 -20 14617 14644 14649 14651 14698 14764 14882 14971 15022 15189 15288 15291 15398 15408 15444 -3 -9 15445 15438 15504 15511 15686 15693 15706 -2 15707 15897 15919 15924 15926 15926 WIP 15930 15938 16023 16262 16355-1 16485 16612-2 16750 16949 (TS) 17024 17025 17100 17203 17369 17442 17506 17799 18004 18014 18181 18245 18629 18916 19005 19011 19092 -1 -2 19114 19115 19125 19136 19407 19439 19500 19501 19502 19503 19505 19506 19507 19508 19509 19510 19600 19752 19757 19770 19775-1 19794-5 19831
20000–29999	20000 20022 20121 20400 20802 20830 21000 21001 21047 21122 21500 21827 22000 22275 22300 22301 22395 22537 23000 23003 23008 23009 23090-3 23092 23094-1 23094-2 23270 23271 23360 23941 24517 24613 24617 24707 24728 25178 25964 26000 26262 26300 26324 27000 series 27000 27001 27002 27005 27006 27729 28000 29110 29148 29199-2 29500
30000+	30170 31000 32000 37001 38500 39075 40500 42010 45001 50001 55000 56000 80000
Category

v т и стандарты МЭК
IEC	60027 60034 60038 60062 60063 60068 60112 60228 60269 60297 60309 60320 60364 60446 60559 60601 60870 60870-5 60870-6 60906-1 60908 60929 60958 61030 61131 61131-3 61131-9 61158 61162 61334 61355 61360 61400 61499 61508 61511 61784 61850 61851 61883 61960 61968 61970 62014-4 62026 62056 62061 62196 62262 62264 62304 62325 62351 62365 62366 62379 62386 62455 62680 62682 62700 63110 63119 63382
ISO/IEC	646 1989 2022 4909 5218 6429 6523 7810 7811 7812 7813 7816 7942 8613 8632 8652 8859 9126 9293 9496 9529 9592 9593 9899 9945 9995 10021 10116 10165 10179 10279 10646 10967 11172 11179 11404 11544 11801 12207 13250 13346 13522-5 13568 13816 13818 14443 14496 14651 14882 15288 15291 15408 15444 15445 15504 15511 15693 15897 15938 16262 16485 17024 17025 18004 18014 18181 19752 19757 19770 19788 20000 20802 21000 21827 22275 22537 23000 23003 23008 23270 23360 24707 24727 24744 24752 26300 27000 27000-series 27002 27040 29110 29119 33001 38500 39075 42010 80000 81346
Related	International Electrotechnical Commission