Известный “Z нотация” приложения?
Некоторый контекст: Недавно для аспирантуры я исследовал инструменты UML для удобства использования и понимания UML в целом для независимого проекта. Я также модель/архитектор для жизни.
предыдущие сообщения имеют слишком много ответов и недостаточно вопросов. Распространенное заблуждение - то, что UML о создании схем. Несомненно, схемы важны, но действительно Вы создаете модель. Вот вопросы, на которые нужно ответить, поскольку каждый продукт/решение поставщика делает некоторые вещи лучше, чем другие. Примечание: перечисленные ответы являются моим представлением как лучшим, даже если другие продукты поддерживают данную функцию или потребность.
- Вы моделируете или тянете? (Тянущий - ArgoUML, бесплатные реализации, и Visio)
- Вы будете моделировать в будущем? (Для основного моделирования - выпуски Сообщества продуктов платы)
- Вы хотите формализовать свое моделирование через профили или метамодели? OCL? ( Sparx, RSM, Визуальная Парадигма )
- Вы обеспокоены мобильностью модели, поддержкой XMI? ( GenMyModel, Sparx, Визуальная Парадигма , Altova)
- у Вас есть существующий набор документов, с которыми необходимо работать? (Зависит от документов)
- , Вы хотели бы генерировать тупики кода или полный функционирующий код? ( GenMyModel, Визуальная Парадигма , Sparx, Altova)
- Вам нужны более зрелые процессы, такие как управление вариантом использования, создание шаблона, создание актива, интеграция RUP, и т.д.? (RSA/RSM/IBM Рациональные продукты)
Подробные Примеры: IBM, когда дело доходит до которой Рациональный Архитектор программного обеспечения не реализовал UML 2.0 полностью, понимает отношения типа при создании профиля UML, но Visual Paradigm и Sparx разобрались в нем.
хорошо, который был слишком детализирован, таким образом, более простой пример будет ArgoUML, который не имеет никаких функций генерации кода и внимания на рисование больше, чем аспект моделирования UML.
Sparx и Визуальная Парадигма делает UML действительно хорошо и генерирует код хорошо, однако, сцепляясь в жизненные циклы проекта, и другой процесс состоит в том, где RSM/RSA силен.
Не упускают закрытый или продукт определенные процессы генерации кода или платформы, поскольку Вы могли закончить застрявшие в том продукте.
Это - прямая "разгрузка мозга", таким образом, пара деталей не может быть прекрасной, однако, это должно предоставить общую карту вопросам и решения изучения.
НОВЫЙ - Найденный хорошим списком многих инструментов UML с описаниями. Wiki Список Инструмента UML
5 ответов
Мне пришлось сделать Z обратно в uni! Возвращает воспоминания. Если у вас есть установленный Linux, попробуйте это приложение CADiZ ...
Я впервые столкнулся с Z-нотацией, когда прочитал, что XCB (замена исходного API Xlib в X11 ) был доказан корректно с Z-записью .
Стоит взглянуть на метод B ( http://en.wikipedia.org/wiki/B-Method ). Это немного более прагматичный потомок Z. Идея состоит в том, что вы можете фактически выполнить кучу обязательств по доказательству с помощью шагов уточнения (с помощью средства доказательства теорем, которое скрывается за кулисами), а затем в конечном итоге сгенерировать код прямо из вашей спецификации. Я считаю, что он использовался в ряде проектов «реального мира».
Z является (как вы указали) нотацией спецификации, а не языком программирования, предназначенным для облегчения формальной проверки.
Одним из более крупных (общеизвестных) проектов, указанных с помощью нотации, был протокол, используемый в платформе смарт-карт Mondex.Недавно было возрождение для определения правильности оригинальных ручных доказательств с механической проверкой несколькими командами, которые включали проверку оригинальных спецификаций Z. Неудивительно, что никаких новых фундаментальных ошибок обнаружено не было, хотя ряд предположений был признан недействительным большинством команд.
Проект Агентства национальной безопасности Tokeneer был указан в Z перед реализацией в подмножестве Spark Ada.
Учитывая выразительность нотации, маловероятно, что она будет расширена. Это также сделало бы доказательства более сложными и контрпродуктивными.
«Z ++» называется объект-Z . Я не был активен в Z с начала 90-х (частично работал над портом CADiZ для Windows, который, похоже, исчез), поэтому понятия не имею, есть ли его текущее сообщество, но некоторые более свежие статьи были опубликованы на использование объекта Z для формализации UML .