Нотация Z: Формальное описание вычислительных систем
Z notation
Z-нотация: формальный язык спецификаций для моделирования компьютерных систем. Разработан Ж.-Р. Абриалем, применяется для чёткого описания программ и систем.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Формальный язык спецификации, используемый для описания и моделирования вычислительных систем.
Formal specification language used for describing and modelling computing systems
Z-нотация (/z//ɛ//d/) — это формальный язык спецификации, применяемый для описания и моделирования вычислительных систем. Он предназначен для четкой спецификации компьютерных программ и компьютерных систем в целом.
The Z notation '/z//ɛ//d/ is a formal specification language used for describing and modelling computing systems. It is targeted at the clear specification of computer programs and computer based systems in general.
История
В 1974 году Жан Рэймонд Абриал опубликовал книгу "Семантика данных". Он использовал нотацию, которая впоследствии преподавалась в Университете Гренобля до конца 1980-х годов. Работая в EDF (Électricité de France) совместно с Бертраном Мейером, Абриал также занимался разработкой Z. Нотация Z используется в книге "Méthodes de programmation", опубликованной в 1980 году. Впервые Z была предложена Абриалом в 1977 году при участии Стива Шумана и Бертрана Мейера. Дальнейшая разработка Z велась в исследовательской группе программирования Оксфордского университета, где Абриал работал в начале 1980-х годов, переехав в Оксфорд в сентябре 1979 года. Абриал утверждал, что Z получила свое название "потому, что это окончательный язык!", хотя имя "Зермело" также связано с Z-нотацией благодаря использованию теории множеств Зермело — Френкеля. В 1992 году была создана Группа пользователей Z (ZUG) для координации деятельности, связанной с Z-нотацией, в частности, организации встреч и конференций.
In 1974, Jean Raymond Abrial published "Data Semantics". He used a notation that would later be taught in the University of Grenoble until the end of the 1980s. While at EDF (Électricité de France), working with Bertrand Meyer, Abrial also worked on developing Z. The Z notation is used in the 1980 book Méthodes de programmation. Z was originally proposed by Abrial in 1977 with the help of Steve Schuman and Bertrand Meyer. It was developed further at the Programming Research Group at Oxford University, where Abrial worked in the early 1980s, having arrived at Oxford in September 1979. Abrial has said that Z is so named "Because it is the ultimate language!" although the name "Zermelo" is also associated with the Z notation through its use of Zermelo–Fraenkel set theory. In 1992, the Z User Group (ZUG) was established to oversee activities concerning the Z notation, especially meetings and conferences.
Использование и обозначение
Z основывается на стандартной математической нотации, используемой в аксиоматической теории множеств, лямбда-исчислении и логике предикатов первого порядка. Все выражения в нотации Z имеют тип, что позволяет избежать некоторых парадоксов наивной теории множеств. Z содержит стандартизированный каталог (называемый математическим инструментарием) часто используемых математических функций и предикатов, определенных средствами самого Z. Он расширен Z-схемами, которые можно комбинировать с помощью собственных операторов, основанных на стандартных логических операторах, а также путем включения схем внутрь других схем. Это позволяет создавать большие Z-спецификации удобным образом. Поскольку нотация Z (как и язык APL, задолго до него) использует множество символов, не входящих в ASCII, спецификация содержит рекомендации по представлению символов Z в ASCII и LaTeX. Также существуют кодировки Unicode для всех стандартных символов Z.
Z is based on the standard mathematical notation used in axiomatic set theory, lambda calculus, and first order predicate logic. All expressions in Z notation are typed, thereby avoiding some of the paradoxes of naive set theory. Z contains a standardized catalogue (called the mathematical toolkit) of commonly used mathematical functions and predicates, defined using Z itself. It is augmented with Z schema boxes, which can be combined using their own operators, based on standard logical operators, and also by including schemas within other schemas. This allows Z specifications to be built up into large specifications in a convenient manner. Because Z notation (just like the APL language, long before it) uses many non ASCII symbols, the specification includes suggestions for rendering the Z notation symbols in ASCII and in LaTeX. There are also Unicode encodings for all standard Z symbols.