Qu'est-ce que le format de fichier VDM ?
.vdm est un format de fichier de développement utilisé pour stocker du code source écrit dans les langages de spécification VDM-SL ou VDM++. Un fichier .vdm est en texte brut et peut être édité à l'aide de n'importe quel éditeur de texte. Les fichiers VDM stockent des spécifications formelles qui décrivent un modèle d'un système informatique. L'utilisation de fichiers de spécification VDM permet aux concepteurs d'obtenir une vue de haut niveau du système - une vue plus difficile à obtenir en parcourant uniquement le code source de l'implémentation. Les fichiers VDM peuvent également servir de base à la génération de composants de code.
Vienna Development Method
La norme VDM a été développée dans les années 1970 au laboratoire de Vienne d'IBM et constitue l'une des plus anciennes méthodes formelles pour le développement de systèmes informables. VDM-SL a été normalisé sous le nom de ISO/IEC 13817-1 en 1996. Il a ensuite été amélioré pour prendre en charge la modélisation orientée objet, ce qui a donné la norme VDM++, qui utilise également des fichiers .vdm. Un troisième dialecte, VDM-RT, étend VDM++ pour les systèmes temps réel et distribués. Le langage est appliqué à des domaines critiques pour la sécurité, notamment la conception de systèmes d'exploitation, les compilateurs, l'avionique et les systèmes de contrôle de dispositifs médicaux.
L'ensemble d'outils open-source principal est Overture Tool, un IDE basé sur Eclipse activement maintenu par la communauté et utilisé dans des projets de recherche et industriels de l'UE. Certains outils utilisent les extensions alternatives .vdmsl et .vdmpp pour distinguer les deux principaux dialectes.
Sécurité et sûreté
RISQUE : LOWFichiers de code source en texte brut ; aucun contenu exécutable. Aucun vecteur de logiciel malveillant connu.
Détails du format
en bref- Fichier Macro VEDIT (Greenview Data) - Fichier de script/macro pour l'éditeur de texte VEDIT (Greenview Data, Inc.) ; écrit dans le langage macro VDM pour automatiser les tâches d'édition sur des fichiers texte, binaires ou EBCDIC. VEDIT est un éditeur Windows/DOS de niche mais toujours commercialisé.
- Module de définition de virus Windows Defender - Historiquement utilisé par Microsoft Windows Defender pour les modules de définition de virus (fichiers .vdm contenant des signatures de logiciels malveillants connus) ; le Defender moderne utilise un mécanisme de mise à jour différent.
Programmes qui ouvrent les fichiers VDM
Windows4 apps
VDMTools
Payant Ouvrir les fichiers .vdm pour la vérification de type et la preuve ; outil hérité, préférez Overture.
VEDIT
Payant Pour les fichiers .vdm de macros VEDIT uniquement : ouvrez l'éditeur de texte VEDIT et exécutez/éditez les macros.
Overture Tool
Open-source Importer le projet → ajouter les fichiers .vdm ; vérifier le type et animer les spécifications via l'IDE Overture.
VS Code (with Overture extension)
Open-source La communauté Overture fournit un support de langage VS Code pour VDM ; ouvrez .vdm pour la coloration syntaxique. 
macOS2 apps
VDMTools
Free (academic) Ouvrir les fichiers .vdm pour la vérification de type et la preuve ; outil hérité, préférez Overture.
Overture Tool
Open-source Importer le projet → ajouter les fichiers .vdm ; vérifier le type et animer les spécifications via l'IDE Overture. 
Linux2 apps
VDMTools
Free (academic) Ouvrir les fichiers .vdm pour la vérification de type et la preuve ; outil hérité, préférez Overture.
Overture Tool
Open-source Importer le projet → ajouter les fichiers .vdm ; vérifier le type et animer les spécifications via l'IDE Overture. Détails techniques
spécifications approfondies| Encodage du fichier | Texte brut - ASCII ou UTF-8 |
| Dialectes | VDM-SL (modulaire/plat), VDM++ (orienté objet), VDM-RT (temps réel/distribué) |
| Norme ISO | ISO/IEC 13817-1:1996 (VDM-SL) |
| Base de la syntaxe | Théorie des ensembles, logique des prédicats, types de données algébriques |
| Structure du module (VDM-SL) | Mot-clé `module` avec les sections `types`, `values`, `functions`, `operations` |
| Structure de classe (VDM++) | Mot-clé `class` avec variables d'instance, méthodes et invariants |
| Taille de fichier typique | 1 Ko - 200 Ko |
| Systèmes d'exploitation supportés | Windows, Linux, macOS - format texte indépendant de la plateforme |
| Outils principaux | Overture Tool (basé sur Eclipse, open source) ; VDMTools (commercial, hérité) |
| Extensions alternatives | `.vdmsl` pour les sources VDM-SL, `.vdmpp` et `.vpp` pour les sources VDM++ |
| Génération de code | Génération Java et C++ à partir de VDM++/VDM-RT supportée par Overture Tool |
| Domaines d'application | Avionique, dispositifs médicaux, systèmes financiers, conception de compilateurs, systèmes embarqués critiques pour la sécurité |
| Publié | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Dernière version | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Standard ouvert | Oui · libre de droits |
| Spécification | www.overturetool.org |
Conversions VDM
Q&R de la communauté
posées par les utilisateursPas encore de questions - soyez le premier à poser une question sur les fichiers VDM.
