Che cos'è il formato di file VDM?
.vdm è un formato di file di sviluppo utilizzato per memorizzare il codice sorgente scritto nei linguaggi di specifica VDM-SL o VDM++. Un file .vdm è in formato testo semplice e può essere modificato con qualsiasi editor di testo. I file VDM memorizzano specifiche formali che descrivono un modello di un sistema informatico. L'uso dei file di specifica VDM consente ai progettisti di ottenere una visione di alto livello del sistema - una visione più difficile da ottenere consultando solo il codice sorgente dell'implementazione. I file VDM possono anche servire come base per la generazione di componenti di codice.
Vienna Development Method
Lo standard VDM è stato sviluppato negli anni '70 presso il laboratorio IBM di Vienna ed è uno dei più antichi metodi formali per lo sviluppo di sistemi informatici. VDM-SL è stato standardizzato come ISO/IEC 13817-1 nel 1996. È stato ulteriormente potenziato per supportare la modellazione orientata agli oggetti, dando vita allo standard VDM++, che utilizza anch'esso file .vdm. Un terzo dialetto, VDM-RT, estende VDM++ per i sistemi in tempo reale e distribuiti. Il linguaggio viene applicato a domini critici per la sicurezza, tra cui la progettazione di sistemi operativi, compilatori, software per l'avionica e sistemi di controllo per dispositivi medici.
Il set di strumenti open-source principale è Overture Tool, un IDE basato su Eclipse mantenuto attivamente dalla comunità e utilizzato in progetti di ricerca e industriali dell'UE. Alcuni strumenti utilizzano le estensioni alternative .vdmsl e .vdmpp per distinguere i due dialetti principali.
Sicurezza e incolumità
RISCHIO: LOWFile di codice sorgente in testo semplice; nessun contenuto eseguibile. Nessun vettore di malware noto.
Dettagli del formato
in sintesi- File Macro VEDIT (Greenview Data) - File script/macro per l'editor di testo VEDIT (Greenview Data, Inc.); scritto nel linguaggio macro VDM per automatizzare le attività di modifica su file di testo, binari o EBCDIC. VEDIT è un editor per Windows/DOS di nicchia ma ancora in vendita.
- Modulo di definizione dei virus di Windows Defender - Storicamente utilizzato da Microsoft Windows Defender per i moduli di definizione dei virus (file .vdm contenenti firme di malware note); il moderno Defender utilizza un meccanismo di aggiornamento diverso.
Programmi che aprono file VDM
Windows4 apps
VDMTools
A pagamento Apre i file .vdm per il controllo dei tipi e la dimostrazione; strumento legacy, si preferisce Overture.
VEDIT
A pagamento Solo per i file .vdm macro di VEDIT: aprire l'editor di testo VEDIT ed eseguire/modificare le macro.
Overture Tool
Open-source Importare il progetto → aggiungere i file .vdm; controllare i tipi e animare le specifiche tramite l'IDE Overture.
VS Code (with Overture extension)
Open-source La comunità Overture fornisce supporto linguistico per VS Code per VDM; aprire .vdm per l'evidenziazione della sintassi. 
macOS2 apps
VDMTools
Free (academic) Apre i file .vdm per il controllo dei tipi e la dimostrazione; strumento legacy, si preferisce Overture.
Overture Tool
Open-source Importare il progetto → aggiungere i file .vdm; controllare i tipi e animare le specifiche tramite l'IDE Overture. 
Linux2 apps
VDMTools
Free (academic) Apre i file .vdm per il controllo dei tipi e la dimostrazione; strumento legacy, si preferisce Overture.
Overture Tool
Open-source Importare il progetto → aggiungere i file .vdm; controllare i tipi e animare le specifiche tramite l'IDE Overture. Dettagli tecnici
specifiche approfondite| Codifica del file | Testo semplice - ASCII o UTF-8 |
| Dialetti | VDM-SL (modulare/piatto), VDM++ (orientato agli oggetti), VDM-RT (tempo reale/distribuito) |
| Standard ISO | ISO/IEC 13817-1:1996 (VDM-SL) |
| Base della sintassi | Teoria degli insiemi, logica dei predicati, tipi di dati algebrici |
| Struttura del modulo (VDM-SL) | Parola chiave `module` con sezioni `types`, `values`, `functions`, `operations` |
| Struttura della classe (VDM++) | Parola chiave `class` con variabili di istanza, metodi e invarianti |
| Dimensione tipica del file | 1 KB - 200 KB |
| Supporto OS | Windows, Linux, macOS - formato di testo indipendente dalla piattaforma |
| Strumentazione principale | Overture Tool (basato su Eclipse, open source); VDMTools (commerciale, legacy) |
| Estensioni alternative | `.vdmsl` per sorgenti VDM-SL, `.vdmpp` e `.vpp` per sorgenti VDM++ |
| Generazione di codice | Generazione Java e C++ da VDM++/VDM-RT supportata da Overture Tool |
| Domini di applicazione | Avionica, dispositivi medici, sistemi finanziari, progettazione di compilatori, sistemi embedded critici per la sicurezza |
| Rilasciato | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Ultima versione | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Standard aperto | Sì · royalty-free |
| Specifica | www.overturetool.org |
Conversioni VDM
Domande e risposte della community
chiesto dagli utentiAncora nessuna domanda - sii il primo a chiedere informazioni sui file VDM.
