Известны "Z обозначения" приложений?
Я просто вспоминал свои университетские уроки и хотел знать, использовал ли кто-нибудь здесь даже "Z-нотацию" в профессиональной среде. Я честно должен сказать, что это был самый скучный урок, который я когда-либо посещал в своей жизни. Может быть, из-за учителя, но в то время мы все думали, что это большая трата времени. Я мог ошибаться, поэтому я хотел бы услышать вас об этом.
Если вы используете его или какой-либо производный язык (Z++), я просто хотел бы знать, как это полезно для вас. Просто любопытно узнать некоторые общеизвестные приложения Z или ваше приложение.
Для тех, кто не знаком: http://staff.washington.edu/jon/z/z-examples.html
6 ответов
Z - (как вы указали) обозначение спецификации, а не язык программирования, предназначенный для облегчения формальной проверки.
Одним из более крупных (общеизвестных) проектов, указанных с использованием нотации, был протокол, используемый в платформе смарт-карт Mondex. Недавно было возрождено определение правильности оригинальных ручных доказательств с механической проверкой несколькими командами, которая включала проверку оригинальных спецификаций Z. Неудивительно, что никаких новых фундаментальных ошибок обнаружено не было, хотя большинство предположений показало, что ряд предположений оказался неверным.
Проект Tokeneer Агентства национальной безопасности был указан в Z до реализации в подмножестве Spark Ada.
Учитывая выразительность обозначения, маловероятно, что оно будет расширено. Это также сделало бы доказательства более сложными и контрпродуктивными.
Стоит посмотреть на метод B ( http://en.wikipedia.org/wiki/B-Method). Это немного более прагматичный потомок Z. Идея состоит в том, что вы можете фактически выполнить кучу обязательств по доказательству через этапы уточнения (с помощью средства доказательства теорем, которое скрывается за кулисами), а затем в конечном итоге генерировать код непосредственно из вашей спецификации. Я считаю, что он был использован в ряде проектов "реального мира".
Я впервые столкнулся с Z-нотацией, когда прочитал, что XCB (замена оригинального Xlib API в X11) оказался верным с Z-нотацией.
Язык описания веб-сервисов (WSDL) был разработан с использованием нотации Z. Вы можете найти спецификацию с обозначением Z здесь: http://www.w3.org/TR/wsdl20/wsdl20-z.html. В спецификации говорится, что
Нотация Z использовалась для улучшения качества нормативного текста, определяющего Компонентную модель, и для обеспечения того, чтобы набор тестов охватывал все важные правила, подразумеваемые Компонентной моделью.
Я должен был сделать Z обратно в универе! Возвращает воспоминания, если у вас есть удобная установка Linux, попробуйте это приложение CADiZ...
"Z++" называется object-Z. Я не был активен в Z с начала 90-х (работая частично над портом Windows CADiZ, который, похоже, исчез), поэтому не знаю, есть ли его текущее сообщество, но некоторые более свежие статьи были опубликованы на использование объекта Z для формализации UML.