El Método de Desarrollo de Viena ( VDM ) es uno de los métodos formales más antiguos para el desarrollo de sistemas informáticos. Originado en el trabajo realizado en el Laboratorio IBM de Viena [1] en la década de 1970, ha crecido para incluir un grupo de técnicas y herramientas basadas en un lenguaje de especificación formal: el lenguaje de especificación VDM (VDM-SL). Tiene una forma extendida, VDM ++, [2] que admite el modelado de objetos orientadosy sistemas concurrentes. El soporte para VDM incluye herramientas comerciales y académicas para analizar modelos, incluido el soporte para probar y probar propiedades de modelos y generar código de programa a partir de modelos VDM validados. Existe una historia de uso industrial de VDM y sus herramientas y un creciente cuerpo de investigación en el formalismo ha llevado a contribuciones notables a la ingeniería de sistemas críticos, compiladores , sistemas concurrentes y en lógica para ciencias de la computación .
Los sistemas informáticos se pueden modelar en VDM-SL a un nivel de abstracción más alto que el que se puede lograr utilizando lenguajes de programación, lo que permite el análisis de diseños y la identificación de características clave, incluidos defectos, en una etapa temprana del desarrollo del sistema. Los modelos que han sido validados se pueden transformar en diseños de sistemas detallados a través de un proceso de refinamiento. El lenguaje tiene una semántica formal, lo que permite probar las propiedades de los modelos con un alto nivel de seguridad. También tiene un subconjunto ejecutable, de modo que los modelos se pueden analizar mediante pruebas y se pueden ejecutar a través de interfaces gráficas de usuario, de modo que los modelos puedan ser evaluados por expertos que no necesariamente están familiarizados con el lenguaje de modelado en sí.
Los orígenes de VDM-SL se encuentran en el IBM Laboratorio en Viena , donde la primera versión del lenguaje se denomina V ienna D efinición L anguage (VDL). [3] El VDL se utilizó esencialmente para proporcionar descripciones de semántica operativa en contraste con el VDM - Meta-IV que proporcionaba semántica denotacional [4]
«Hacia finales de 1972, el grupo de Viena volvió a centrar su atención en el problema de desarrollar sistemáticamente un compilador a partir de una definición de lenguaje. El enfoque general adoptado se ha denominado el "método de desarrollo de Viena" ... El metalenguaje realmente adoptado ("Meta-IV") se utiliza para definir las partes principales de PL / 1 (como se da en ECMA 74 - curiosamente un "formal documento de normas redactado como intérprete de resúmenes ") en BEKIČ 74.» [5]
No hay conexión entre Meta-IV , [6] y el lenguaje Meta-II de Schorre , o su sucesor Tree Meta ; se trataba de sistemas compilador-compilador en lugar de ser adecuados para descripciones formales de problemas.
Así que Meta-IV se "usó para definir partes importantes" del lenguaje de programación PL / I. Otros lenguajes de programación descritos retrospectivamente, o parcialmente descritos, usando Meta-IV y VDM-SL incluyen el lenguaje de programación BASIC , FORTRAN , el lenguaje de programación APL , ALGOL 60, el lenguaje de programación Ada y el lenguaje de programación Pascal . Meta-IV evolucionó en varias variantes, generalmente descritas como escuelas danesas, inglesas e irlandesas.