Известные "Z обозначения" приложений?

Question

Я только что вспомнил свои университетские уроки и хотел узнать, использовал ли кто-нибудь здесь даже «Z-нотацию» в профессиональной среде. Я честно должен сказать, что это был самый скучный урок, который я когда-либо посещал в своей жизни. Может быть, из-за учителя, но в то время мы все думали, что это большая трата времени. Возможно, я был неправ, поэтому я хотел бы услышать вас об этом.

Если вы используете его или какой-либо производный язык (Z ++), я просто хотел бы знать, насколько это полезно для вас. Просто любопытно узнать некоторые общеизвестные приложения Z или ваше приложение.

Для тех, кто не знаком: http://staff.washington.edu/jon/z/z-examples.html

Answer 1

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

Одним из более крупных (общеизвестных) проектов, указанных с использованием нотации, был протокол, используемый в платформе смарт-карт Mondex. Недавно было пробуждение для определения правильности оригинальных ручных доказательств с механической проверкой несколькими группами, которые включали проверку оригинальных спецификаций Z . Неудивительно, что никаких новых фундаментальных ошибок обнаружено не было, хотя большинство команд показало, что ряд предположений неверен.

Агентство национальной безопасности Проект Tokeneer был указан в Z до реализации в подмножестве Spark Ada.

Учитывая выразительность обозначения, маловероятно, что оно будет расширено. Это также сделало бы доказательства более сложными и контрпродуктивными.

Answer 2

Стоит взглянуть на метод B (http://en.wikipedia.org/wiki/B-Method). Это немного более прагматичный потомок Z. Идея состоит в том, что вы можете фактически выполнить кучу доказательственных обязательств с помощью этапов уточнения (с помощью доказательства теоремы). который прячется за кулисами), а затем в конечном итоге генерировать код непосредственно из вашей спецификации. Я считаю, что он использовался в ряде проектов "реального мира".

Answer 3

Я впервые столкнулся с Z-нотацией, когда прочитал, что XCB (замена оригинального Xlib API в X11 ) был проверен на правильность с Z-нотацией .

Answer 4

Язык описания веб-сервисов (WSDL) был разработан с использованием нотации Z. Вы можете найти спецификацию с обозначением Z здесь: http://www.w3.org/TR/wsdl20/wsdl20-z.html. В спецификации указано, что

Нотация Z использовалась для улучшения качества нормативного текста, который определяет Компонентную модель, и для обеспечения того, чтобы набор тестов охватывал все важные правила, подразумеваемые Компонентной моделью.

Answer 5

'Z ++' называется object-Z . Я не был активным в Z с начала 90-х (работая частично над портом Windows CADiZ, который, похоже, исчез), поэтому не знаю, есть ли его текущее сообщество, но некоторые более свежие статьи были опубликованы на использование объекта Z для формализации UML .

Answer 6

Я должен был сделать Z обратно в универ! Возвращает воспоминания, если у вас есть удобная установка Linux, попробуйте это приложение CADiZ ...