Z-нотация

Поделись знанием:
Перейти к: навигация, поиск

Z-нота́ция (англ. Z notation, произносится /zɛd/) — формальный язык спецификации, используемый для описания и моделирования программ и их формальной верификации.

Z-нотацию первоначально предложил Жан-Реймон Абриаль (Jean-Raymond Abrial) в 1977 году при участии Стива Шумана (Steve Schuman) и Бертранда Мейера (Bertrand Meyer)[1]

Z-нотация основана на стандартной математической нотации, используемой в аксиоматической теории множеств, лямбда-исчислении и логике предикатов первого порядка. Допустимые выражения в Z-нотации подобраны таким образом, чтобы избегать парадоксов аксиоматической теории множеств. Также Z-нотация содержит стандартизированный каталог часто используемых математических функций и предикатов.

Хотя Z-нотация использует много символов вне набора ASCII, спецификация допускает запись выражений целиком в ASCII или посредством LaTeX. Z ttf font[2] — специализированный шрифт для Z-нотации.

В 2002 году Международная организация по стандартизации завершила процесс по стандартизации Z-нотации[3].

Для Z создано объектно-ориентированное расширение, Object-Z (англ.).[4]

Напишите отзыв о статье "Z-нотация"



Ссылки

  1. Jean-Raymond Abrial, Stephen A. Schuman and Bertrand Meyer: A Specification Language, in On the Construction of Programs, Cambridge University Press, eds. A. M. Macnaghten and R. M. McKeag, 1980 (describes early version of the language). ISBN 0-521-23090-X
  2. [fonts.goldenweb.it/pan_file/l/en/font2/Zed.ttf/d2/Freeware_fonts/c/z/default.html GoldenWeb.it — Free True Type Fonts download — Zed.ttf]
  3. [standards.iso.org/ittf/PubliclyAvailableStandards/c021573_ISO_IEC_13568_2002(E).zip Information Technology — Z Formal Specification Notation — Syntax, Type System and Semantics]. — [www.iso.ch/iso/en/CatalogueDetailPage.CatalogueDetail?CSNUMBER=21573 ISO/IEC 13568:2002]. — P. 196.
  4. Duke, R. , & Rose, G. (2000). Formal object oriented specification using object-z. Cornerstones of Computing. Macmillan.

Литература

  • J. Michael Spivey. [spivey.oriel.ox.ac.uk/mike/zrm/ The Z Notation: a reference manual]. — 2nd edition. — Prentice Hall International Series in Computer Science, 1992.
  • Jim Davies and Jim Woodcock. [www.usingz.com/text/online/ Using Z: Specification, Refinement and Proof]. — Prentice Hall International Series in Computer Science, 1996. — ISBN 0-13-948472-8.
  • Jonathan Bowen. [www.zuser.org/zbook/ Formal Specification and Documentation using Z: A Case Study Approach]. — International Thomson Computer Press, 1996. — ISBN 1-85032-230-9.
  • Jonathan Jacky. [staff.washington.edu/jon/z-book/ The Way of Z: Practical Programming with Formal Methods]. — Cambridge University Press, 1997. — ISBN 0-521-55976-6.


Отрывок, характеризующий Z-нотация

– Разбойник! Неблагодарная тварь!… изрублю собаку… не с папенькой… обворовал… – и т. д.
Потом эти люди с неменьшим удовольствием и страхом видели, как молодой граф, весь красный, с налитой кровью в глазах, за шиворот вытащил Митеньку, ногой и коленкой с большой ловкостью в удобное время между своих слов толкнул его под зад и закричал: «Вон! чтобы духу твоего, мерзавец, здесь не было!»
Митенька стремглав слетел с шести ступеней и убежал в клумбу. (Клумба эта была известная местность спасения преступников в Отрадном. Сам Митенька, приезжая пьяный из города, прятался в эту клумбу, и многие жители Отрадного, прятавшиеся от Митеньки, знали спасительную силу этой клумбы.)
Жена Митеньки и свояченицы с испуганными лицами высунулись в сени из дверей комнаты, где кипел чистый самовар и возвышалась приказчицкая высокая постель под стеганным одеялом, сшитым из коротких кусочков.
Молодой граф, задыхаясь, не обращая на них внимания, решительными шагами прошел мимо них и пошел в дом.
Графиня узнавшая тотчас через девушек о том, что произошло во флигеле, с одной стороны успокоилась в том отношении, что теперь состояние их должно поправиться, с другой стороны она беспокоилась о том, как перенесет это ее сын. Она подходила несколько раз на цыпочках к его двери, слушая, как он курил трубку за трубкой.
На другой день старый граф отозвал в сторону сына и с робкой улыбкой сказал ему:
– А знаешь ли, ты, моя душа, напрасно погорячился! Мне Митенька рассказал все.
«Я знал, подумал Николай, что никогда ничего не пойму здесь, в этом дурацком мире».
– Ты рассердился, что он не вписал эти 700 рублей. Ведь они у него написаны транспортом, а другую страницу ты не посмотрел.
– Папенька, он мерзавец и вор, я знаю. И что сделал, то сделал. А ежели вы не хотите, я ничего не буду говорить ему.
– Нет, моя душа (граф был смущен тоже. Он чувствовал, что он был дурным распорядителем имения своей жены и виноват был перед своими детьми но не знал, как поправить это) – Нет, я прошу тебя заняться делами, я стар, я…
– Нет, папенька, вы простите меня, ежели я сделал вам неприятное; я меньше вашего умею.
«Чорт с ними, с этими мужиками и деньгами, и транспортами по странице, думал он. Еще от угла на шесть кушей я понимал когда то, но по странице транспорт – ничего не понимаю», сказал он сам себе и с тех пор более не вступался в дела. Только однажды графиня позвала к себе сына, сообщила ему о том, что у нее есть вексель Анны Михайловны на две тысячи и спросила у Николая, как он думает поступить с ним.