¿Qué es el formato de archivo VDM?
.vdm es un formato de archivo de desarrollo utilizado para almacenar código fuente escrito en los lenguajes de especificación VDM-SL o VDM++. Un archivo .vdm es texto plano y puede editarse con cualquier editor de texto. Los archivos VDM almacenan especificaciones formales que describen un modelo de un sistema informático. El uso de archivos de especificación VDM permite a los diseñadores obtener una visión de alto nivel del sistema, algo que es más difícil de lograr examinando únicamente el código fuente de la implementación. Los archivos VDM también pueden servir como base para generar componentes de código.
Vienna Development Method
El estándar VDM fue desarrollado en la década de 1970 en el Laboratorio de Viena de IBM y es uno de los métodos formales más antiguos para el desarrollo de sistemas informáticos. VDM-SL fue estandarizado como ISO/IEC 13817-1 en 1996. Posteriormente se mejoró para admitir el modelado orientado a objetos, lo que dio lugar al estándar VDM++, que también utiliza archivos .vdm. Un tercer dialecto, VDM-RT, extiende VDM++ para sistemas distribuidos y en tiempo real. El lenguaje se aplica en dominios críticos para la seguridad, incluyendo el diseño de sistemas operativos, compiladores, software de aviónica y sistemas de control de dispositivos médicos.
El conjunto de herramientas de código abierto principal es Overture Tool, un IDE basado en Eclipse mantenido activamente por la comunidad y utilizado en proyectos industriales y de investigación de la UE. Algunas herramientas utilizan las extensiones alternativas .vdmsl y .vdmpp para distinguir los dos dialectos principales.
Seguridad y protección
RIESGO: LOWArchivos de código fuente en texto plano; sin contenido ejecutable. No es un vector de malware conocido.
Detalles del formato
en pocas palabras- Archivo de macro VEDIT (Greenview Data) - Archivo de script/macro para el editor de texto VEDIT (Greenview Data, Inc.); escrito en el lenguaje de macros VDM para automatizar tareas de edición en archivos de texto, binarios o EBCDIC. VEDIT es un editor para Windows/DOS de nicho que aún se comercializa.
- Módulo de definición de virus de Windows Defender - Utilizado históricamente por Microsoft Windows Defender para módulos de definición de virus (archivos .vdm que contienen firmas de malware conocidas); el Defender moderno utiliza un mecanismo de actualización diferente.
Programas que abren archivos VDM
Windows4 apps
VDMTools
Pago Abrir archivos .vdm para comprobación de tipos y pruebas; herramienta heredada, se prefiere Overture.
VEDIT
Pago Solo para archivos .vdm de macros de VEDIT: abra el editor de texto VEDIT y ejecute o edite las macros.
Overture Tool
Código abierto Importar proyecto → añadir archivos .vdm; comprobar tipos y animar especificaciones a través del IDE Overture.
VS Code (with Overture extension)
Código abierto La comunidad Overture proporciona soporte de lenguaje en VS Code para VDM; abra .vdm para resaltado de sintaxis. 
macOS2 apps
VDMTools
Free (academic) Abrir archivos .vdm para comprobación de tipos y pruebas; herramienta heredada, se prefiere Overture.
Overture Tool
Código abierto Importar proyecto → añadir archivos .vdm; comprobar tipos y animar especificaciones a través del IDE Overture. 
Linux2 apps
VDMTools
Free (academic) Abrir archivos .vdm para comprobación de tipos y pruebas; herramienta heredada, se prefiere Overture.
Overture Tool
Código abierto Importar proyecto → añadir archivos .vdm; comprobar tipos y animar especificaciones a través del IDE Overture. Detalles técnicos
especificación profunda| Codificación de archivo | Texto plano - ASCII o UTF-8 |
| Dialectos | VDM-SL (modular/plano), VDM++ (orientado a objetos), VDM-RT (tiempo real/distribuido) |
| Estándar ISO | ISO/IEC 13817-1:1996 (VDM-SL) |
| Base de la sintaxis | Teoría de conjuntos, lógica de predicados, tipos de datos algebraicos |
| Estructura de módulos (VDM-SL) | Palabra clave `module` con secciones de `types`, `values`, `functions`, `operations` |
| Estructura de clases (VDM++) | Palabra clave `class` con variables de instancia, métodos e invariantes |
| Tamaño de archivo típico | 1 KB - 200 KB |
| Soporte de SO | Windows, Linux, macOS - formato de texto independiente de la plataforma |
| Herramientas principales | Overture Tool (basado en Eclipse, código abierto); VDMTools (comercial, heredado) |
| Extensiones alternativas | `.vdmsl` para fuentes VDM-SL, `.vdmpp` y `.vpp` para fuentes VDM++ |
| Generación de código | Generación de Java y C++ desde VDM++/VDM-RT soportada por Overture Tool |
| Dominios de aplicación | Aviónica, dispositivos médicos, sistemas financieros, diseño de compiladores, sistemas embebidos críticos para la seguridad |
| Lanzado | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Última versión | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Estándar abierto | Sí · libre de regalías |
| Especificación | www.overturetool.org |
Conversiones de VDM
Preguntas y respuestas de la comunidad
preguntado por usuariosAún no hay preguntas; sea el primero en preguntar sobre los archivos VDM.
