Co to jest format pliku VDM?
.vdm to format pliku programistycznego używany do przechowywania kodu źródłowego napisanego w językach specyfikacji VDM-SL lub VDM++. Plik .vdm jest plikiem tekstowym i może być edytowany za pomocą dowolnego edytora tekstu. Pliki VDM przechowują formalne specyfikacje opisujące model systemu informatycznego. Korzystanie z plików specyfikacji VDM pozwala projektantom uzyskać wysokopoziomowy widok systemu - taki, który jest trudniejszy do uzyskania poprzez samo przeglądanie kodu źródłowego implementacji. Pliki VDM mogą również służyć jako podstawa do generowania komponentów kodu.
Vienna Development Method
Standard VDM został opracowany w latach 70. XX wieku w laboratorium IBM w Wiedniu i jest jedną z najstarszych formalnych metod tworzenia systemów komputerowych. VDM-SL został wystandaryzowany jako ISO/IEC 13817-1 w 1996 roku. Został on dalej rozbudowany w celu obsługi modelowania obiektowego, co zaowocowało standardem VDM++, który również wykorzystuje pliki .vdm. Trzeci dialekt, VDM-RT, rozszerza VDM++ o systemy czasu rzeczywistego i rozproszone. Język ten jest stosowany w domenach krytycznych dla bezpieczeństwa, w tym w projektowaniu systemów operacyjnych, kompilatorów, oprogramowania awionicznego i systemów sterowania urządzeniami medycznymi.
Podstawowym zestawem narzędzi open-source jest Overture Tool, IDE oparte na Eclipse, aktywnie utrzymywane przez społeczność i wykorzystywane w unijnych projektach badawczych oraz przemysłowych. Niektóre narzędzia używają alternatywnych rozszerzeń .vdmsl i .vdmpp, aby odróżnić dwa główne dialekty.
Bezpieczeństwo
RYZYKO: LOWPliki źródłowe w formacie czystego tekstu; brak zawartości wykonywalnej. Brak znanych wektorów złośliwego oprogramowania.
Szczegóły formatu
w pigułce- Plik makra VEDIT (Greenview Data) - Plik skryptu/makra dla edytora tekstu VEDIT (Greenview Data, Inc.); napisany w języku makr VDM w celu automatyzacji zadań edycyjnych na plikach tekstowych, binarnych lub EBCDIC. VEDIT to niszowy, ale wciąż sprzedawany edytor dla systemów Windows/DOS.
- Moduł definicji wirusów Windows Defender - Historycznie używany przez Microsoft Windows Defender dla modułów definicji wirusów (pliki .vdm zawierające sygnatury znanego złośliwego oprogramowania); nowoczesny Defender korzysta z innego mechanizmu aktualizacji.
Programy otwierające pliki VDM
Windows4 apps
VDMTools
Płatny Otwieranie plików .vdm w celu sprawdzania typów i dowodzenia; narzędzie archiwalne, zaleca się Overture.
VEDIT
Płatny Tylko dla plików .vdm makr VEDIT: otwórz edytor tekstu VEDIT, aby uruchamiać lub edytować makra.
Overture Tool
Open-source Importuj projekt → dodaj pliki .vdm; sprawdzaj typy i animuj specyfikacje za pomocą IDE Overture.
VS Code (with Overture extension)
Open-source Społeczność Overture zapewnia wsparcie językowe dla VS Code dla VDM; otwórz .vdm, aby uzyskać podświetlanie składni. 
macOS2 apps
VDMTools
Free (academic) Otwieranie plików .vdm w celu sprawdzania typów i dowodzenia; narzędzie archiwalne, zaleca się Overture.
Overture Tool
Open-source Importuj projekt → dodaj pliki .vdm; sprawdzaj typy i animuj specyfikacje za pomocą IDE Overture. 
Linux2 apps
VDMTools
Free (academic) Otwieranie plików .vdm w celu sprawdzania typów i dowodzenia; narzędzie archiwalne, zaleca się Overture.
Overture Tool
Open-source Importuj projekt → dodaj pliki .vdm; sprawdzaj typy i animuj specyfikacje za pomocą IDE Overture. Szczegóły techniczne
specyfikacja| Kodowanie pliku | Zwykły tekst - ASCII lub UTF-8 |
| Dialekty | VDM-SL (modułowy/płaski), VDM++ (obiektowy), VDM-RT (czasu rzeczywistego/rozproszony) |
| Standard ISO | ISO/IEC 13817-1:1996 (VDM-SL) |
| Podstawa składni | Teoria mnogości, logika predykatów, algebraiczne typy danych |
| Struktura modułu (VDM-SL) | słowo kluczowe `module` z sekcjami `types`, `values`, `functions`, `operations` |
| Struktura klasy (VDM++) | słowo kluczowe `class` ze zmiennymi instancji, metodami i niezmiennikami |
| Typowy rozmiar pliku | 1 KB - 200 KB |
| Obsługa systemów operacyjnych | Windows, Linux, macOS - niezależny od platformy format tekstowy |
| Główne narzędzia | Overture Tool (oparty na Eclipse, open source); VDMTools (komercyjny, archiwalny) |
| Alternatywne rozszerzenia | `.vdmsl` dla źródeł VDM-SL, `.vdmpp` i `.vpp` dla źródeł VDM++ |
| Generowanie kodu | Generowanie Java i C++ z VDM++/VDM-RT obsługiwane przez Overture Tool |
| Domeny zastosowań | Awionika, urządzenia medyczne, systemy finansowe, projektowanie kompilatorów, krytyczne systemy wbudowane |
| Wydano | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Najnowsza wersja | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Otwarty standard | Tak · bezpłatny (royalty-free) |
| Specyfikacja | www.overturetool.org |
Konwersje VDM
Pytania i odpowiedzi społeczności
pytania użytkownikówBrak pytań - bądź pierwszą osobą, która zapyta o pliki VDM.
