Известные приложения "Z notation"?

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

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

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

Ответ 1

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

Ответ 2

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

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

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

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

Ответ 3

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

Ответ 4

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

Ответ 5

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

Ответ 6

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

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