O que é o formato de ficheiro VDM?
.vdm é um formato de arquivo de desenvolvimento usado para armazenar código-fonte escrito nas linguagens de especificação VDM-SL ou VDM++. Um arquivo .vdm é texto simples e pode ser editado usando qualquer editor de texto. Os arquivos VDM armazenam especificações formais que descrevem um modelo de um sistema de computação. O uso de arquivos de especificação VDM permite que os projetistas tenham uma visão de alto nível do sistema - uma que é mais difícil de obter apenas examinando o código-fonte da implementação. Os arquivos VDM também podem servir como base para a geração de componentes de código.
Vienna Development Method
O padrão VDM foi desenvolvido na década de 1970 no Laboratório de Viena da IBM e é um dos métodos formais mais antigos para o desenvolvimento de sistemas de computador. O VDM-SL foi padronizado como ISO/IEC 13817-1 em 1996. Foi posteriormente aprimorado para suportar modelagem orientada a objetos, resultando no padrão VDM++, que também utiliza arquivos .vdm. Um terceiro dialeto, VDM-RT, estende o VDM++ para sistemas de tempo real e distribuídos. A linguagem é aplicada a domínios críticos de segurança, incluindo design de sistemas operacionais, compiladores, aviônica e sistemas de controle de dispositivos médicos.
A principal ferramenta de código aberto é o Overture Tool, um IDE baseado em Eclipse mantido ativamente pela comunidade e usado em projetos industriais e de pesquisa da UE. Algumas ferramentas usam as extensões alternativas .vdmsl e .vdmpp para distinguir os dois dialetos principais.
Segurança e proteção
RISCO: LOWArquivos de código-fonte em texto simples; sem conteúdo executável. Nenhum vetor de malware conhecido.
Detalhes do formato
em resumo- Arquivo de Macro VEDIT (Greenview Data) - Arquivo de script/macro para o editor de texto VEDIT (Greenview Data, Inc.); escrito na linguagem de macro VDM para automatizar tarefas de edição em arquivos de texto, binários ou EBCDIC. O VEDIT é um editor de nicho para Windows/DOS ainda comercializado.
- Módulo de Definição de Vírus do Windows Defender - Historicamente usado pelo Microsoft Windows Defender para módulos de definição de vírus (arquivos .vdm contendo assinaturas de malware conhecidas); o Defender moderno usa um mecanismo de atualização diferente.
Programas que abrem arquivos VDM
Windows4 apps
VDMTools
Pago Abre arquivos .vdm para verificação de tipos e prova; ferramenta legada, prefira o Overture.
VEDIT
Pago Apenas para arquivos .vdm de macro VEDIT: abra o editor de texto VEDIT e execute/edite macros.
Overture Tool
Código aberto Importe o projeto → adicione arquivos .vdm; verifique tipos e anime especificações via IDE Overture.
VS Code (with Overture extension)
Código aberto A comunidade Overture fornece suporte de linguagem VS Code para VDM; abra .vdm para realce de sintaxe. 
macOS2 apps
VDMTools
Free (academic) Abre arquivos .vdm para verificação de tipos e prova; ferramenta legada, prefira o Overture.
Overture Tool
Código aberto Importe o projeto → adicione arquivos .vdm; verifique tipos e anime especificações via IDE Overture. 
Linux2 apps
VDMTools
Free (academic) Abre arquivos .vdm para verificação de tipos e prova; ferramenta legada, prefira o Overture.
Overture Tool
Código aberto Importe o projeto → adicione arquivos .vdm; verifique tipos e anime especificações via IDE Overture. Detalhes técnicos
especificação profunda| Codificação de arquivo | Texto simples - ASCII ou UTF-8 |
| Dialetos | VDM-SL (modular/plano), VDM++ (orientado a objetos), VDM-RT (tempo real/distribuído) |
| Padrão ISO | ISO/IEC 13817-1:1996 (VDM-SL) |
| Base da sintaxe | Teoria dos conjuntos, lógica de predicados, tipos de dados algébricos |
| Estrutura do módulo (VDM-SL) | palavra-chave `module` com seções `types`, `values`, `functions`, `operations` |
| Estrutura da classe (VDM++) | palavra-chave `class` com variáveis de instância, métodos e invariantes |
| Tamanho típico do arquivo | 1 KB - 200 KB |
| Suporte de SO | Windows, Linux, macOS - formato de texto independente de plataforma |
| Ferramental principal | Overture Tool (baseado em Eclipse, código aberto); VDMTools (comercial, legado) |
| Extensões alternativas | `.vdmsl` para fontes VDM-SL, `.vdmpp` e `.vpp` para fontes VDM++ |
| Geração de código | Geração de Java e C++ a partir de VDM++/VDM-RT suportada pelo Overture Tool |
| Domínios de aplicação | Aviônica, dispositivos médicos, sistemas financeiros, design de compiladores, sistemas embarcados críticos de segurança |
| Lançado | 1970s (VDM-SL); ISO/IEC 13817-1 published 1996 |
| Versão mais recente | VDM-SL (ISO/IEC 13817-1:1996); VDM++ (extension for OO, 2000s); VDM-RT (real-time extension) |
| Padrão aberto | Sim · livre de royalties |
| Especificação | www.overturetool.org |
Conversões de VDM
Perguntas e Respostas da Comunidade
perguntado por usuáriosAinda não há perguntas - seja o primeiro a perguntar sobre arquivos VDM.
