Método de desarrollo de Viena

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. Tiene su origen en el trabajo realizado en el Laboratorio IBM de Viena ^[1] en la década de 1970 y ha crecido hasta 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 sistemas orientados a objetos y concurrentes. El soporte para VDM incluye herramientas comerciales y académicas para analizar modelos, incluido el soporte para probar y demostrar 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 la ciencia informática .

Los sistemas informáticos pueden modelarse en VDM-SL a un nivel de abstracción más alto que el que se puede lograr con lenguajes de programación, lo que permite el análisis de diseños y la identificación de características clave, incluidos los defectos, en una etapa temprana del desarrollo del sistema. Los modelos que se han validado se pueden transformar en diseños de sistemas detallados mediante 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 pueden 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 Laboratorio IBM en Viena , donde la primera versión del lenguaje se llamó Vienna Definition Language (VDL). ^[3] El VDL se utilizó esencialmente para dar descripciones semánticas operacionales en contraste con el VDM – Meta -IV que proporcionaba semánticas denotacionales ^[4]

«A finales de 1972, el grupo de Viena volvió a centrarse en el problema de desarrollar sistemáticamente un compilador a partir de una definición de lenguaje. El enfoque general adoptado se denominó "Método de desarrollo de Viena"... El metalenguaje realmente adoptado ("Meta-IV") se utiliza para definir partes importantes de PL/1 (como se indica en ECMA 74, curiosamente un "documento de normas formales escrito como un intérprete abstracto") en BEKIČ 74.» ^[5]

No existe conexión entre Meta-IV , ^{[6] y el lenguaje} META II de Schorre , o su sucesor Tree Meta ; estos eran sistemas compilador-compilador en lugar de ser adecuados para descripciones formales de problemas.

Por lo tanto, Meta-IV se "utilizó para definir partes importantes" del lenguaje de programación PL/I . Otros lenguajes de programación descritos retrospectivamente, o parcialmente, utilizando 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 las escuelas danesa, inglesa e irlandesa.

La "Escuela Inglesa" se deriva del trabajo de Cliff Jones sobre los aspectos de VDM no relacionados específicamente con la definición del lenguaje y el diseño del compilador (Jones 1980, 1990). Hace hincapié en el modelado de estados persistentes ^[7] mediante el uso de tipos de datos construidos a partir de una rica colección de tipos base. La funcionalidad se describe típicamente a través de operaciones que pueden tener efectos secundarios en el estado y que en su mayoría se especifican de manera implícita utilizando una condición previa y una condición posterior. La "Escuela Danesa" ( Bjørner et al. 1982) ha tendido a enfatizar un enfoque constructivo con una especificación operacional explícita utilizada en mayor medida. El trabajo en la escuela danesa condujo al primer compilador Ada validado europeo .

En 1996 se publicó una norma ISO para el lenguaje (ISO, 1996).

La sintaxis y la semántica de VDM-SL y VDM++ se describen en detalle en los manuales de lenguaje de VDMTools y en los textos disponibles. La norma ISO contiene una definición formal de la semántica del lenguaje. En el resto de este artículo se utiliza la sintaxis de intercambio definida por ISO (ASCII). Algunos textos prefieren una sintaxis matemática más concisa .

Un modelo VDM-SL es una descripción del sistema en términos de la funcionalidad que se realiza sobre los datos. Consiste en una serie de definiciones de tipos de datos y funciones u operaciones que se realizan sobre ellos.

VDM-SL incluye tipos básicos que modelan números y caracteres como se indica a continuación:

Los tipos de datos se definen para representar los datos principales del sistema modelado. Cada definición de tipo introduce un nuevo nombre de tipo y proporciona una representación en términos de los tipos básicos o en términos de los tipos ya introducidos. Por ejemplo, un tipo que modele los identificadores de usuario para un sistema de gestión de inicio de sesión podría definirse de la siguiente manera:

tipos
Id. de usuario = nat

Para manipular valores pertenecientes a tipos de datos, se definen operadores sobre los valores. Por lo tanto, se proporcionan sumas, restas, etc. de números naturales, así como operadores booleanos como igualdad y desigualdad. El lenguaje no fija un número representable máximo o mínimo ni una precisión para los números reales. Dichas restricciones se definen cuando son necesarias en cada modelo por medio de invariantes de tipo de datos, expresiones booleanas que denotan condiciones que deben respetar todos los elementos del tipo definido. Por ejemplo, un requisito de que los identificadores de usuario no deben ser mayores que 9999 se expresaría de la siguiente manera (donde <=es el operador booleano "menor o igual a" en números naturales):

Id. de usuario = nat
invuid ==uid <= 9999

Dado que los invariantes pueden ser expresiones lógicas arbitrariamente complejas y la pertenencia a un tipo definido está limitada únicamente a aquellos valores que satisfacen el invariante, la corrección de tipo en VDM-SL no es decidible automáticamente en todas las situaciones.

Los otros tipos básicos incluyen char para caracteres. En algunos casos, la representación de un tipo no es relevante para el propósito del modelo y solo agregaría complejidad. En tales casos, los miembros del tipo pueden representarse como tokens sin estructura. Los valores de los tipos de token solo se pueden comparar para determinar su igualdad; no se definen otros operadores en ellos. Cuando se requieren valores con nombre específicos, estos se introducen como tipos de comillas. Cada tipo de comillas consta de un valor con nombre del mismo nombre que el tipo en sí. Los valores de los tipos de comillas (conocidos como literales de comillas) solo se pueden comparar para determinar su igualdad.

Por ejemplo, al modelar un controlador de señal de tráfico, puede ser conveniente definir valores para representar los colores de la señal de tráfico como tipos de comillas:

< Rojo > , < Ámbar > , < Ámbar intermitente > , < Verde >

Los tipos básicos por sí solos tienen un valor limitado. Se crean tipos de datos nuevos y más estructurados mediante constructores de tipos.

El constructor de tipos más básico forma la unión de dos tipos predefinidos. El tipo (A|B)contiene todos los elementos del tipo A y todos los del tipo B. En el ejemplo del controlador de señales de tráfico, el tipo que modela el color de una señal de tráfico podría definirse de la siguiente manera:

Color de la señal =   < Rojo > | < Ámbar > | < Ámbar intermitente > | < Verde >

Los tipos enumerados en VDM-SL se definen como se muestra arriba como uniones en tipos de comillas.

Los tipos de productos cartesianos también se pueden definir en VDM-SL. El tipo (A1*…*An)es el tipo compuesto por todas las tuplas de valores, cuyo primer elemento es del tipo A1y el segundo del tipo, A2y así sucesivamente. El tipo compuesto o de registro es un producto cartesiano con etiquetas para los campos. El tipo

T::f1:A1
     f2:A2
     ...
     fn:Uno

es el producto cartesiano con campos etiquetados como f1,…,fn. Un elemento de tipo Tpuede estar compuesto por sus partes constituyentes mediante un constructor, escrito mk_T. A la inversa, dado un elemento de tipo T, los nombres de campo pueden usarse para seleccionar el componente nombrado. Por ejemplo, el tipo

Fecha:: día:nat1
        mes:nat1
        año:nat
inv mk_Date(d,m,y) == d<=31 y m<=12

modela un tipo de fecha simple. El valor mk_Date(1,4,2001)corresponde al 1 de abril de 2001. Dada una fecha d, la expresión d.monthes un número natural que representa el mes. Si se desea, se pueden incorporar restricciones sobre los días por mes y los años bisiestos al invariante. Combinando estos:

mk_Date(1,4,2001).mes = 4

Los tipos de colección modelan grupos de valores. Los conjuntos son colecciones finitas no ordenadas en las que se suprime la duplicación entre valores. Las secuencias son colecciones finitas ordenadas (listas) en las que puede producirse duplicación y las asignaciones representan correspondencias finitas entre dos conjuntos de valores.

El constructor de tipo de conjunto (escrito set of Tdonde Tes un tipo predefinido) construye el tipo compuesto por todos los conjuntos finitos de valores extraídos del tipo T. Por ejemplo, la definición de tipo

UGroup  =  conjunto de UserId  

define un tipo UGroupcompuesto por todos los conjuntos finitos de UserIdvalores. Se definen varios operadores en los conjuntos para construir su unión, intersecciones, determinar relaciones de subconjuntos no estrictos y propias, etc.

El constructor de tipo de secuencia finita (escrito seq of Tdonde Tes un tipo predefinido) construye el tipo compuesto por todas las listas finitas de valores extraídos del tipo T. Por ejemplo, la definición de tipo

Cadena  =  secuencia de caracteres
  

Define un tipo Stringcompuesto por todas las cadenas finitas de caracteres. Se definen varios operadores en secuencias para construir concatenaciones, selección de elementos y subsecuencias, etc. Muchos de estos operadores son parciales en el sentido de que no están definidos para ciertas aplicaciones. Por ejemplo, la selección del quinto elemento de una secuencia que contiene solo tres elementos no está definida.

El orden y la repetición de elementos en una secuencia es significativo, por lo que [a, b]no es igual a [b, a], y [a]no es igual a [a, a].

Una asignación finita es una correspondencia entre dos conjuntos, el dominio y el rango, con el dominio indexando elementos del rango. Por lo tanto, es similar a una función finita. El constructor de tipo de asignación en VDM-SL (escrito map T1 to T2donde T1y T2son tipos predefinidos) construye el tipo compuesto de todas las asignaciones finitas de conjuntos de T1valores a conjuntos de T2valores. Por ejemplo, la definición de tipo

Cumpleaños  =  asignar cadena a fecha   

Define un tipo Birthdaysque asigna cadenas de caracteres a Date. Nuevamente, los operadores se definen en asignaciones para indexar en la asignación, fusionar asignaciones, sobrescribir y extraer subasignaciones.

La principal diferencia entre las notaciones VDM-SL y VDM++ es la forma en que se aborda la estructuración. En VDM-SL hay una extensión modular convencional, mientras que VDM++ tiene un mecanismo de estructuración orientado a objetos tradicional con clases y herencia.

En la norma ISO para VDM-SL hay un anexo informativo que contiene diferentes principios de estructuración. Todos ellos siguen los principios tradicionales de ocultación de información con módulos y pueden explicarse de la siguiente manera:

• Nomenclatura de módulos : cada módulo comienza sintácticamente con la palabra clave moduleseguida del nombre del módulo. Al final de un módulo endse escribe la palabra clave seguida nuevamente del nombre del módulo.
• Importación : Es posible importar definiciones que se han exportado desde otros módulos. Esto se hace en una sección de importaciones que comienza con la palabra clave importsy sigue con una secuencia de importaciones desde diferentes módulos. Cada una de estas importaciones de módulos comienza con la palabra clave fromseguida del nombre del módulo y una firma del módulo. La firma del módulo puede ser simplemente la palabra clave allque indica la importación de todas las definiciones exportadas desde ese módulo, o puede ser una secuencia de firmas de importación. Las firmas de importación son específicas para tipos, valores, funciones y operaciones y cada una de ellas comienza con la palabra clave correspondiente. Además, estas firmas de importación nombran las construcciones a las que se desea acceder. Además, puede estar presente información de tipo opcional y, finalmente, es posible cambiar el nombre de cada una de las construcciones al importar. Para los tipos, también es necesario utilizar la palabra clave structsi se desea obtener acceso a la estructura interna de un tipo en particular.
• Exportación : Las definiciones de un módulo a las que se desea que tengan acceso otros módulos se exportan utilizando la palabra clave exportsseguida de una firma de módulo de exportaciones. La firma de módulo de exportaciones puede consistir simplemente en la palabra clave allo en una secuencia de firmas de exportación. Dichas firmas de exportación son específicas para tipos, valores, funciones y operaciones, y cada una de ellas comienza con la palabra clave correspondiente. En caso de que se desee exportar la estructura interna de un tipo, structse debe utilizar la palabra clave.
• Características más exóticas : en versiones anteriores de las herramientas VDM-SL también se admitían módulos parametrizados e instancias de dichos módulos. Sin embargo, estas características se eliminaron de VDMTools alrededor del año 2000 porque casi nunca se utilizaban en aplicaciones industriales y existían muchos problemas con las herramientas relacionadas con ellas.

En VDM++ la estructuración se realiza mediante clases y herencia múltiple. Los conceptos clave son:

• Clase : Cada clase comienza sintácticamente con la palabra clave classseguida del nombre de la clase. Al final de una clase endse escribe la palabra clave seguida nuevamente del nombre de la clase.
• Herencia : en caso de que una clase herede construcciones de otras clases, el nombre de la clase en el encabezado de la clase puede ir seguido de las palabras clave is subclass ofseguidas de una lista separada por comas de nombres de superclases.
• Modificadores de acceso : La ocultación de información en VDM++ se realiza de la misma manera que en la mayoría de los lenguajes orientados a objetos que utilizan modificadores de acceso. En VDM++, las definiciones son privadas por defecto, pero delante de todas las definiciones es posible utilizar una de las palabras clave de modificadores de acceso: private, publicy protected.

En VDM-SL, las funciones se definen sobre los tipos de datos definidos en un modelo. El soporte para la abstracción requiere que sea posible caracterizar el resultado que una función debe calcular sin tener que decir cómo debe calcularse. El mecanismo principal para hacer esto es la definición de función implícita en la que, en lugar de una fórmula que calcule un resultado, un predicado lógico sobre las variables de entrada y resultado, denominado postcondición , proporciona las propiedades del resultado. Por ejemplo, una función SQRTpara calcular la raíz cuadrada de un número natural podría definirse de la siguiente manera:

SQRT (x:nat)r: publicación real
 r*r = x
   

Aquí la poscondición no define un método para calcular el resultado r, sino que establece qué propiedades se pueden suponer que cumple. Nótese que esto define una función que devuelve una raíz cuadrada válida; no hay ningún requisito de que deba ser la raíz positiva o negativa. La especificación anterior se cumpliría, por ejemplo, con una función que devolviera la raíz negativa de 4 pero la raíz positiva de todas las demás entradas válidas. Nótese que las funciones en VDM-SL deben ser deterministas, de modo que una función que satisfaga la especificación del ejemplo anterior siempre debe devolver el mismo resultado para la misma entrada.

Se llega a una especificación de función más restringida reforzando la condición posterior. Por ejemplo, la siguiente definición restringe la función para que devuelva la raíz positiva.

SQRT (x:nat)r: post real
 r*r = x y r >= 0     

Todas las especificaciones de funciones pueden estar restringidas por condiciones previas que son predicados lógicos sobre las variables de entrada únicamente y que describen restricciones que se supone que se cumplen cuando se ejecuta la función. Por ejemplo, una función de cálculo de raíz cuadrada que funciona únicamente con números reales positivos podría especificarse de la siguiente manera:

SQRTP (x: real )r: real 
antes de  x >= 0 después de r*r = x y r >= 0 
     

La condición previa y la condición posterior forman juntas un contrato que debe ser satisfecho por cualquier programa que pretenda implementar la función. La condición previa registra los supuestos bajo los cuales la función garantiza devolver un resultado que satisface la condición posterior. Si se llama a una función con entradas que no satisfacen su condición previa, el resultado no está definido (de hecho, ni siquiera se garantiza la terminación).

VDM-SL también admite la definición de funciones ejecutables a la manera de un lenguaje de programación funcional. En una definición de función explícita , el resultado se define mediante una expresión sobre las entradas. Por ejemplo, una función que produce una lista de los cuadrados de una lista de números podría definirse de la siguiente manera:

SqList: seq de nat -> seq de nat
 SqList (s) == si s = [] entonces [] de lo contrario [( hd s) ** 2 ] ^ SqList ( tl s)
                   

Esta definición recursiva consta de una firma de función que proporciona los tipos de entrada y resultado y un cuerpo de función. Una definición implícita de la misma función podría adoptar la siguiente forma:

SqListImp (s:seq de nat)r:seq de nat
 después de len r = len s y
 para todo i en el conjunto inds s y r(i) = s(i) ** 2                        

La definición explícita es, en un sentido simple, una implementación de la función especificada implícitamente. La corrección de una definición de función explícita con respecto a una especificación implícita puede definirse de la siguiente manera.

Dada una especificación implícita:

f(p: T_p )r: T_r 
pre pre -f(p)
 post post -f(p, r)
   

y una función explícita:

f:T_p - > T_r  

Decimos que satisface la especificación si y solo si :

para todo  p en el conjunto T_p y pre -f(p) => f(p): T_r y post -f(p, f(p))
          

Por lo tanto, " fes una implementación correcta" debe interpretarse como " fsatisface la especificación".

En VDM-SL, las funciones no tienen efectos secundarios como cambiar el estado de una variable global persistente. Esta es una capacidad útil en muchos lenguajes de programación, por lo que existe un concepto similar; en lugar de funciones, se utilizan operaciones para cambiar las variables de estado (también conocidas como globales ).

Por ejemplo, si tenemos un estado que consta de una sola variable someStateRegister : nat, podríamos definirlo en VDM-SL como:

 Registro estatal de algúnStateRegister : nat
 end  
      

En VDM++ esto se definiría como:

  variables
 de instancia    someStateRegister  :  nat

Una operación para cargar un valor en esta variable podría especificarse como:

 CARGAR (i:nat)
  text  wr  algúnStateRegister:nat
 post algúnStateRegister = i
    

La cláusula externaext ( ) especifica a qué partes del estado puede acceder la operación, rdlo que indica acceso de solo lectura y wres acceso de lectura y escritura.

A veces es importante hacer referencia al valor de un estado antes de que se modificara; por ejemplo, una operación para agregar un valor a la variable puede especificarse como:

 AGREGAR (i:nat)
  text  wr  someStateRegister  :  nat
 post someStateRegister = someStateRegister~ + i
      

Donde el ~símbolo en la variable de estado en la postcondición indica el valor de la variable de estado antes de la ejecución de la operación.

Este es un ejemplo de una definición de función implícita. La función devuelve el elemento más grande de un conjunto de números enteros positivos:

 máx(s:conjunto de nat)r:nat
 antes de la tarjeta s > 0 después de r en el conjunto s y
 para todo r' en el conjunto s y r' <= r
       
                    

La poscondición caracteriza el resultado en lugar de definir un algoritmo para obtenerlo. La precondición es necesaria porque ninguna función podría devolver un r en el conjunto s cuando el conjunto está vacío.

 multp(i,j:nat)r:nat
 antes verdadero después r = i*j
  
    

Aplicación de la obligación de prueba forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))a una definición explícita de multp:

 multp(i,j)  ==
 si i= 0 entonces 0 de lo contrario si es -par(i)
 entonces 2 *multp(i/ 2 ,j)
 de lo contrario j+multp(i- 1 ,j)
   
   
                    

Entonces la obligación de prueba pasa a ser:

 para todo  i,  j  :  nat  y  multp(i,j):nat  y  multp(i,  j)  =  i*j

Esto se puede demostrar correctamente mediante:

1. Probar que la recursión termina (esto a su vez requiere probar que los números se vuelven más pequeños en cada paso)
2. Inducción matemática

Este es un ejemplo clásico que ilustra el uso de la especificación de operaciones implícitas en un modelo basado en estados de una estructura de datos conocida. La cola se modela como una secuencia compuesta de elementos de un tipo Qelt. La representación es Qeltinmaterial y, por lo tanto, se define como un tipo de token.

 tipos

 Qelt  =  token;
 Cola = secuencia de Qelt ;     

 estado LaCola de q : Fin de la cola  
     
 

 operaciones

 ENQUEUE (e: Qelt )
  ext  wr  q: Cola de 
mensajes q = q~ ^ [e];      

 DEQUEUE ()e: Qelt
  ext  wr  q: Cola 
pre q <> []
 post q~ = [e]^q;        

 IS - EMPTY ()r:bool
  ext  rd  q: Cola 
de mensajes r <= > ( len q = 0 )
       

Como ejemplo muy simple de un modelo VDM-SL, considere un sistema para mantener los detalles de la cuenta bancaria del cliente. Los clientes se modelan mediante números de cliente ( CustNum ), las cuentas se modelan mediante números de cuenta ( AccNum ). Las representaciones de los números de cliente se consideran inmateriales y, por lo tanto, se modelan mediante un tipo de token. Los saldos y sobregiros se modelan mediante tipos numéricos.

 AccNum  =  token;
 CustNum = token;
 Saldo = int ;
 Sobregiro = nat;         

 AccData  ::  propietario  : CustNum saldo : Saldo 
              

 estado Banco de accountMap : mapear AccNum a AccData overdraftMap : mapear CustNum a Overdraft inv mk_Bank(accountMap,overdraftMap) == para todos a en el conjunto rng accountMap y a.owner en el conjunto dom overdraftMap y
 a.balance >= -overdraftMap(a.owner)
  
        
        
                                                            

Con operaciones: NEWC asigna un nuevo número de cliente:

 operaciones
 NEWC (od : Sobregiro )r : CustNum ext wr overdraftMap : asigna CustNum a Sobregiro post r no en el conjunto dom ~overdraftMap y overdraftMap = ~overdraftMap ++ { r | -> od};
     
        
                

NEWAC asigna un nuevo número de cuenta y establece el saldo en cero:

 NEWAC (cu  : CustNum )r : AccNum ext wr accountMap : asigna AccNum a AccData rd overdraftMap asigna CustNum a Sobregiro pre cu en el conjunto dom overdraftMap
 post r no en el conjunto dom accountMap~ y accountMap = accountMap~ ++ {r| -> mk_AccData(cu, 0 )}
   
        
          
                    

ACINF devuelve todos los saldos de todas las cuentas de un cliente, como un mapa del número de cuenta al saldo:

 ACINF (cu  : CustNum )r : asigna AccNum a Balance ext rd accountMap : asigna AccNum a AccData post r = {an | -> accountMap(an).balance | an en el conjunto dom accountMap y accountMap(an).owner = cu}
      
        
                

Varias herramientas diferentes admiten VDM:

• VDMTools era la herramienta comercial líder para VDM y VDM++, propiedad de CSK Systems, comercializada, mantenida y desarrollada por esta última, basándose en versiones anteriores desarrolladas por la empresa danesa IFAD. Los manuales y un tutorial práctico están disponibles. Todas las licencias están disponibles, de forma gratuita, para la versión completa de la herramienta. La versión completa incluye generación automática de código para Java y C++, biblioteca de vínculos dinámicos y compatibilidad con CORBA.
• Overture es una iniciativa de código abierto basada en la comunidad que tiene como objetivo proporcionar soporte de herramientas de libre acceso para todos los dialectos VDM (VDM-SL, VDM++ y VDM-RT), originalmente sobre la plataforma Eclipse, pero posteriormente sobre la plataforma Visual Studio Code. Su objetivo es desarrollar un marco para herramientas interoperables que sean útiles para aplicaciones industriales, investigación y educación.
• vdm-mode es una colección de paquetes de Emacs para escribir especificaciones VDM utilizando VDM-SL, VDM++ y VDM-RT. Admite resaltado y edición de sintaxis, verificación de sintaxis sobre la marcha, finalización de plantillas y compatibilidad con intérpretes.
• SpecBox: de Adelard, ofrece comprobación de sintaxis, comprobación semántica sencilla y generación de un archivo LaTeX que permite imprimir especificaciones en notación matemática. Esta herramienta está disponible de forma gratuita, pero ya no se mantiene.
• Existen macros LaTeX y LaTeX2e disponibles para respaldar la presentación de modelos VDM en la sintaxis matemática del lenguaje estándar ISO. Han sido desarrolladas y son mantenidas por el Laboratorio Nacional de Física del Reino Unido. La documentación y las macros están disponibles en línea.

El VDM se ha aplicado ampliamente en una variedad de dominios de aplicación. Las aplicaciones más conocidas son:

• Compiladores Ada y CHILL : El primer compilador Ada validado europeo fue desarrollado por Dansk Datamatik Center utilizando VDM. ^[8] Asimismo, la semántica de CHILL y Modula-2 se describió en sus estándares utilizando VDM.
• ConForm: un experimento en British Aerospace que compara el desarrollo convencional de una pasarela confiable con un desarrollo que utiliza VDM.
• Dust-Expert: un proyecto llevado a cabo por Adelard en el Reino Unido para una aplicación relacionada con la seguridad que determina que la seguridad es apropiada en el diseño de plantas industriales.
• El desarrollo de VDMTools: la mayoría de los componentes del conjunto de herramientas VDMTools se desarrollan utilizando VDM. Este desarrollo se ha llevado a cabo en el FIDA en Dinamarca y en el CSK en Japón . ^[9]
• TradeOne: Algunos componentes clave del sistema administrativo TradeOne desarrollado por CSK Systems para la bolsa de valores japonesa se desarrollaron utilizando VDM. Existen mediciones comparativas de la productividad de los desarrolladores y la densidad de defectos de los componentes desarrollados con VDM en comparación con el código desarrollado de manera convencional.
• FeliCa Networks ha informado del desarrollo de un sistema operativo para un circuito integrado para aplicaciones de telefonía celular .

El uso de VDM comienza con un modelo muy abstracto y lo desarrolla hasta convertirlo en una implementación. Cada paso implica la reificación de datos y luego la descomposición de las operaciones .

La reificación de datos desarrolla los tipos de datos abstractos en estructuras de datos más concretas , mientras que la descomposición de operaciones desarrolla las especificaciones implícitas (abstractas) de operaciones y funciones en algoritmos que pueden implementarse directamente en un lenguaje de computadora elegido.

${\displaystyle {\begin{array}{|rcl|}{\textbf {Specification}}&&{\textbf {Implementation}}\\\hline {\text{Abstract data type}}&\xrightarrow {\text{Data reification}} &{\text{Data structure}}\\{\text{Operations}}&{\xrightarrow[{\text{Operation decomposition}}]{}}&{\text{Algorithms}}\end{array}}}$

La reificación de datos (refinamiento por pasos) implica encontrar una representación más concreta de los tipos de datos abstractos utilizados en una especificación. Puede haber varios pasos antes de llegar a una implementación. Cada paso de reificación para una representación de datos abstracta ABS_REPimplica proponer una nueva representación NEW_REP. Para demostrar que la nueva representación es precisa, se define una función de recuperaciónNEW_REP que se relaciona con ABS_REP, es decir retr : NEW_REP -> ABS_REP. La corrección de una reificación de datos depende de demostrar la adecuación , es decir

 para todo  a: ABS_REP  & existe r: NEW_REP & a = retr(r)
      

Dado que la representación de los datos ha cambiado, es necesario actualizar las operaciones y funciones para que operen en NEW_REP. Se debe demostrar que las nuevas operaciones y funciones conservan cualquier invariante de tipo de datos en la nueva representación. Para demostrar que las nuevas operaciones y funciones modelan las que se encuentran en la especificación original, es necesario cumplir con dos obligaciones de prueba:

• Regla de dominio:

 para todos  r: NEW_REP y pre - OPA (retr(r)) => pre - OPR (r)
     

• Regla de modelado:

 para todos  ~r,r: NEW_REP  y pre - OPA (retr(~r)) y post - OPR (~r,r) => post - OPA (retr(~r,), retr(r))
      

En un sistema de seguridad empresarial, los trabajadores reciben tarjetas de identificación, que se introducen en lectores de tarjetas al entrar y salir de la fábrica. Operaciones necesarias:

• INIT()inicializa el sistema, asume que la fábrica está vacía
• ENTER(p : Person)registra que un trabajador está entrando a la fábrica; los datos de los trabajadores se leen de la tarjeta de identificación)
• EXIT(p : Person)Registra que un trabajador está saliendo de la fábrica.
• IS-PRESENT(p : Person) r : boolComprueba si un trabajador específico está en la fábrica o no.

Formalmente esto sería:

 tipos

 Persona  =  token;
 Trabajadores = conjunto de Personas ;     

 AWCCS estatal de pres: Los trabajadores terminan  
    
 

 operaciones

 INIT ()
  ext  wr  pres: Trabajadores post pres = {}; 
    

 ENTER (p  : Persona )
 ext wr pres : Trabajadores pre p no está en el conjunto pres
 post pres = pres~ sindicato {p};      
            

 SALIR (p  : Persona )
 ext wr pres : Trabajadores pre p en el conjunto pres
 post pres = pres~\{p};      
         

 IS - PRESENTE (p  : Persona ) r : bool
 ext rd pres : Trabajadores post r <= > p en conjunto pres~
         
       

Como la mayoría de los lenguajes de programación tienen un concepto comparable a un conjunto (a menudo en forma de matriz), el primer paso a partir de la especificación es representar los datos en términos de una secuencia. Estas secuencias no deben permitir la repetición, ya que no queremos que el mismo trabajador aparezca dos veces, por lo que debemos agregar un invariante al nuevo tipo de datos. En este caso, el orden no es importante, por lo que [a,b]es lo mismo que [b,a].

El método de desarrollo de Viena es útil para sistemas basados ​​en modelos, pero no es adecuado si el sistema está basado en el tiempo. Para estos casos, el cálculo de sistemas comunicantes (CCS) es más útil.

• Métodos formales
• Especificación formal
• Código pidgin
• Lógica de predicados
• Cálculo proposicional
• Lenguaje de especificación Z , la principal alternativa a VDM-SL (comparar)

• Bjørner, Dines; Cliff B. Jones (1978). El método de desarrollo de Viena: el metalenguaje, Lecture Notes in Computer Science 61. Berlín, Heidelberg, Nueva York: Springer. ISBN 978-0-387-08766-5.
• O'Regan, Gerard (2006). Enfoques matemáticos para la calidad del software . Londres: Springer. ISBN 978-1-84628-242-3.
• Cliff B. Jones, ed. (1984). Lenguajes de programación y su definición — H. Bekič (1936-1982) . Apuntes de clase sobre informática . Vol. 177. Berlín, Heidelberg, Nueva York, Tokio: Springer-Verlag. doi :10.1007/BFb0048933. ISBN 978-3-540-13378-0.S2CID 7488558  .
• Fitzgerald, JS y Larsen, PG, Modelling Systems: Practical Tools and Techniques in Software Engineering (Sistemas de modelado: herramientas y técnicas prácticas en ingeniería de software ). Cambridge University Press , 1998 , ISBN 0-521-62348-0 (edición japonesa publicada por Iwanami Shoten, 2003, ISBN 4-00-005609-3 ). ^[10]  
• Fitzgerald, JS , Larsen, PG, Mukherjee, P., Plat, N. y Verhoef, M., Validated Designs for Object-oriented Systems . Springer Verlag 2005. ISBN 1-85233-881-4 . El sitio web de soporte [1] incluye ejemplos y soporte de herramientas gratuito. ^[11] 
• Jones, CB , Systematic Software Development using VDM , Prentice Hall 1990. ISBN 0-13-880733-7 . También disponible en línea y de forma gratuita: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip 
• Bjørner, D. y Jones, CB , Especificación formal y desarrollo de software Prentice Hall International, 1982. ISBN 0-13-880733-7 
• J. Dawes, Guía de referencia VDM-SL , Pitman 1991. ISBN 0-273-03151-1 
• Organización Internacional de Normalización , Tecnología de la información – Lenguajes de programación, sus entornos e interfaces de software de sistema – Método de desarrollo de Viena – Lenguaje de especificación – Parte 1: Lenguaje base Norma internacional ISO/IEC 13817-1, diciembre de 1996.
• Jones, CB , Desarrollo de software: un enfoque riguroso , Prentice Hall International, 1980. ISBN 0-13-821884-6 
• Jones, CB y Shaw, RC (eds.), Estudios de casos en desarrollo sistemático de software , Prentice Hall International, 1990. ISBN 0-13-880733-7 
• Bicarregui, JC, Fitzgerald, JS , Lindsay, PA, Moore, R. y Ritchie, B., Prueba en VDM: una guía para profesionales . Springer Verlag Enfoques formales de la informática y la tecnología de la información (FACIT), 1994. ISBN 3-540-19813-X . 

• Información sobre VDM y VDM++ (copia archivada en archive.org)
• Lenguaje de definición de Viena (VDL)
• Lenguaje de modelado COMPASS Archivado el 19 de febrero de 2020 en Wayback Machine (CML), una combinación de VDM-SL con CSP , basada en Teorías Unificadoras de Programación , desarrollada para modelar Sistemas de Sistemas (SoS)