Что такое формат файла VDM?
.vdm - это формат файла разработки, используемый для хранения исходного кода, написанного на языках спецификаций VDM-SL или VDM++. Файл .vdm является текстовым и может быть отредактирован в любом текстовом редакторе. Файлы VDM хранят формальные спецификации, описывающие модель вычислительной системы. Использование файлов спецификаций VDM позволяет проектировщикам получить высокоуровневое представление о системе - такое, которое труднее получить, просто изучая исходный код реализации. Файлы VDM также могут служить основой для генерации программных компонентов.
Vienna Development Method
Стандарт VDM был разработан в 1970-х годах в Венской лаборатории IBM и является одним из старейших формальных методов разработки компьютерных систем. VDM-SL был стандартизирован как ISO/IEC 13817-1 в 1996 году. Позже он был усовершенствован для поддержки объектно-ориентированного моделирования, что привело к появлению стандарта VDM++, который также использует файлы .vdm. Третий диалект, VDM-RT, расширяет VDM++ для систем реального времени и распределенных систем. Язык применяется в критически важных областях, включая проектирование операционных систем, компиляторов, программного обеспечения для авионики и систем управления медицинскими приборами.
Основным набором инструментов с открытым исходным кодом является Overture Tool - IDE на базе Eclipse, активно поддерживаемая сообществом и используемая в исследовательских и промышленных проектах ЕС. Некоторые инструменты используют альтернативные расширения .vdmsl и .vdmpp, чтобы различать два основных диалекта.
Безопасность и защита
РИСК: LOWФайлы исходного кода в текстовом формате; не содержат исполняемого контента. Известные векторы вредоносного ПО отсутствуют.
Детали формата
в двух словах- Файл макроса VEDIT (Greenview Data) - Файл скрипта/макроса для текстового редактора VEDIT (Greenview Data, Inc.); написан на языке макросов VDM для автоматизации задач редактирования текстовых, бинарных или EBCDIC-файлов. VEDIT - это нишевый, но все еще продаваемый редактор для Windows/DOS.
- Модуль определений вирусов Windows Defender - Исторически использовался Microsoft Windows Defender для модулей определений вирусов (файлы .vdm, содержащие сигнатуры известных вредоносных программ); современный Defender использует другой механизм обновления.
Программы, открывающие файлы VDM
Windows4 apps
VDMTools
Платно Открытие файлов .vdm для проверки типов и доказательств; устаревший инструмент, рекомендуется Overture.
VEDIT
Платно Только для макросов .vdm для VEDIT: откройте текстовый редактор VEDIT для запуска или редактирования макросов.
Overture Tool
Открытый код Импорт проекта → добавление файлов .vdm; проверка типов и анимация спецификаций через Overture IDE.
VS Code (with Overture extension)
Открытый код Сообщество Overture предоставляет поддержку языка для VS Code; откройте .vdm для подсветки синтаксиса. 
macOS2 apps
VDMTools
Free (academic) Открытие файлов .vdm для проверки типов и доказательств; устаревший инструмент, рекомендуется Overture.
Overture Tool
Открытый код Импорт проекта → добавление файлов .vdm; проверка типов и анимация спецификаций через Overture IDE. 
Linux2 apps
VDMTools
Free (academic) Открытие файлов .vdm для проверки типов и доказательств; устаревший инструмент, рекомендуется Overture.
Overture Tool
Открытый код Импорт проекта → добавление файлов .vdm; проверка типов и анимация спецификаций через Overture IDE. Технические подробности
глубокая спецификация| Кодировка файла | Простой текст - ASCII или UTF-8 |
| Диалекты | VDM-SL (модульный/плоский), VDM++ (объектно-ориентированный), VDM-RT (реального времени/распределенный) |
| Стандарт ISO | ISO/IEC 13817-1:1996 (VDM-SL) |
| Основа синтаксиса | Теория множеств, логика предикатов, алгебраические типы данных |
| Структура модуля (VDM-SL) | Ключевое слово `module` с разделами `types`, `values`, `functions`, `operations` |
| Структура класса (VDM++) | Ключевое слово `class` с переменными экземпляра, методами и инвариантами |
| Типичный размер файла | 1 КБ - 200 КБ |
| Поддержка ОС | Windows, Linux, macOS - платформонезависимый текстовый формат |
| Основной инструментарий | Overture Tool (на базе Eclipse, открытый исходный код); VDMTools (коммерческий, устаревший) |
| Альтернативные расширения | `.vdmsl` для исходников VDM-SL, `.vdmpp` и `.vpp` для исходников VDM++ |
| Генерация кода | Генерация Java и C++ из VDM++/VDM-RT поддерживается в Overture Tool |
| Области применения | Авионика, медицинские приборы, финансовые системы, проектирование компиляторов, критически важные встраиваемые системы |
| Выпущен | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Последняя версия | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Открыть стандартное | Да · без роялти |
| Спецификация | www.overturetool.org |
Конвертации VDM
Вопросы и ответы сообщества
спрошено пользователямиВопросов пока нет - станьте первым, кто спросит о файлах VDM.
