Método de desarrollo de Viena - Vienna Development Method

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 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 VDM Specification Language (VDM-SL). Tiene una forma extendida, VDM ++, que admite el modelado de sistemas concurrentes y orientados a objetos . 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 .

Filosofía

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 pueden ser evaluados por expertos que no están necesariamente familiarizados con el lenguaje de modelado en sí.

Historia

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). El VDL se usó esencialmente para dar descripciones de semántica operativa en contraste con el VDM - Meta-IV que proporcionó semántica denotacional

«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 indica en ECMA 74 - curiosamente un "formal documento de normas escrito como intérprete de resúmenes ") en BEKIČ 74.»

No hay conexión entre Meta-IV 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.

Por 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 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 las escuelas danesa, inglesa e irlandesa.

La "escuela inglesa" deriva del trabajo de Cliff Jones sobre los aspectos de VDM que no están específicamente relacionados con la definición del lenguaje y el diseño del compilador (Jones 1980, 1990). Enfatiza el modelado del estado persistente 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 implícitamente 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 especificación operativa explícita utilizada en mayor medida. El trabajo en la escuela danesa condujo al primer compilador Ada validado en Europa .

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

Funciones de VDM

La sintaxis y la semántica de VDM-SL y VDM ++ se describen detalladamente en los manuales de idioma 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 definido por ISO (ASCII). Algunos textos prefieren una sintaxis matemática más concisa .

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

Tipos básicos: numérico, carácter, token y cotización

VDM-SL incluye números y caracteres de modelado de tipos básicos de la siguiente manera:

Tipos basicos
bool Tipo de datos booleano falso verdadero
nat números naturales (incluido el cero) 0, 1, 2, 3, 4, 5 ...
nat1 números naturales (excluyendo el cero) 1, 2, 3, 4, 5, ...
int enteros ..., −3, −2, −1, 0, 1, 2, 3, ...
rat numeros racionales a / b , donde a y b son números enteros, b no es 0
real numeros reales ...
char caracteres A B C, ...
token tokens sin estructura ...
<A> el tipo de cotización que contiene el valor <A> ...

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 ofrece una representación en términos de los tipos básicos o en términos de los tipos ya introducidos. Por ejemplo, un tipo de identificadores de usuario de modelado para un sistema de gestión de inicio de sesión podría definirse de la siguiente manera: 

types
UserId = nat

Para manipular valores que pertenecen a tipos de datos, los operadores se definen en los valores. Por lo tanto, se proporcionan sumas, restas, etc. de números naturales, al igual que operadores booleanos como igualdad y desigualdad. El lenguaje no fija un número máximo o mínimo representable o una precisión para los números reales. Dichas restricciones se definen cuando se requieren en cada modelo mediante invariantes de tipo de datos: expresiones booleanas que denotan condiciones que deben ser respetadas por 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 que" en números naturales): 

UserId = nat
inv uid == uid <= 9999

Dado que los invariantes pueden ser expresiones lógicas arbitrariamente complejas, y la pertenencia a un tipo definido se limita solo a aquellos valores que satisfacen el invariante, la corrección de tipos en VDM-SL no se puede decidir automáticamente en todas las situaciones.

Los otros tipos básicos incluyen char para personajes. 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 tokens solo se pueden comparar para determinar la igualdad; no se definen otros operadores en ellos. Cuando se requieren valores con nombre específicos, estos se introducen como tipos de cotización. Cada tipo de cotización 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 por igualdad.

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

<Red>, <Amber>, <FlashingAmber>, <Green>

Constructores de tipos: unión, producto y tipos compuestos

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

Constructores de tipo básico
T1 | T2 | ... | Tn Unión de tipos T1,...,Tn
T1*T2*...*Tn Producto cartesiano de tipos T1,...,Tn
T :: f1:T1 ... fn:Tn Tipo compuesto (registro)

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: 

SignalColour =  <Red> | <Amber> | <FlashingAmber> | <Green>

Los tipos enumerados en VDM-SL se definen como se muestra arriba como uniones en tipos de cotización.

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, el primer elemento del cual 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:An

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

Date :: day:nat1
        month:nat1
        year:nat
inv mk_Date(d,m,y) == d <=31 and 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. Las restricciones de días por mes y años bisiestos podrían incorporarse al invariante si se desea. Combinando estos: 

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

Colecciones

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

Conjuntos

El constructor de tipos de conjuntos (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 = set of UserId

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

Operadores principales en conjuntos (s, s1, s2 son conjuntos)
{a, b, c} Conjunto de enumeración: el conjunto de elementos a, byc
{x | x:T & P(x)} Comprensión de conjuntos: el conjunto de xdesde tipo Ttal queP(x)
{i, ..., j} El conjunto de enteros en el rango iaj
e in set s e es un elemento del conjunto s
e not in set s e no es un elemento del conjunto s
s1 union s2 Unión de conjuntos s1ys2
s1 inter s2 Intersección de conjuntos s1ys2
s1 \ s2 Establecer diferencia de conjuntos s1ys2
dunion s Unión distribuida de conjunto de conjuntos s
s1 psubset s2 s1 es un subconjunto (adecuado) de s2
s1 subset s2 s1 es un subconjunto (débil) de s2
card s La cardinalidad del conjunto s

Secuencias

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ídas del tipo T. Por ejemplo, la definición de tipo 

String = seq of char

Define un tipo Stringcompuesto por todas las cadenas finitas de caracteres. Se definen varios operadores en secuencias para construir concatenación, selección de elementos y subsecuencias, etc. Muchos de estos operadores son parciales en el sentido de que no están definidos para determinadas 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 los elementos en una secuencia es significativo, por [a, b]lo que no es igual [b, a]ni [a]es igual a [a, a].

Operadores principales en secuencias (s, s1, s2 son secuencias)
[a, b, c] Enumeración de secuencias: la secuencia de elementos a, byc
[f(x) | x:T & P(x)] Comprensión de secuencia: secuencia de expresiones f(x)para cada uno xde los tipos (numéricos) Ttal que se P(x)mantienen
( xvalores tomados en orden numérico)
hd s La cabeza (primer elemento) de s
tl s La cola (secuencia restante después de quitar la cabeza) de s
len s El largo de s
elems s El conjunto de elementos de s
s(i) El iésimo elemento des
inds s el conjunto de índices para la secuencia s
s1^s2 la secuencia formada por la concatenación de secuencias s1ys2

Mapas

Un mapeo finito es una correspondencia entre dos conjuntos, el dominio y el rango, con los elementos de indexación del dominio del rango. Por tanto, es similar a una función finita. El constructor de tipos de mapeo en VDM-SL (escrito map T1 to T2donde T1y T2son tipos predefinidos) construye el tipo compuesto por todos los mapeos finitos desde conjuntos de T1valores a conjuntos de T2valores. Por ejemplo, la definición de tipo 

Birthdays = map String to Date

Define un tipo al Birthdaysque se asignan cadenas de caracteres Date. Nuevamente, los operadores se definen en mapeos para indexarlos en el mapeo, fusionar mapeos, sobrescribir y extraer submapeos.

Principales operadores en mapeos
{a |-> r, b |-> s} Mapeo de enumeración: amapea a r, bmapea as
{x |-> f(x) | x:T & P(x)} Mapeo de comprensión: se xasigna a f(x)todos xpara el tipo de Tmodo queP(x)
dom m El dominio de m
rng m El rango de m
m(x) m aplicado a x
m1 munion m2 Unión de asignaciones m1y m2( m1, m2debe ser coherente donde se superponen)
m1 ++ m2 m1 sobrescrito por m2

Estructuración

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

Estructuración en VDM-SL

En la norma ISO para VDM-SL existe un anexo informativo que contiene diferentes principios de estructuración. Todos estos siguen los principios tradicionales de ocultación de información con módulos y se pueden explicar como:

  • Denominación del módulo : Cada módulo está sintácticamente comenzó con la palabra clave moduleseguida por el nombre del módulo. Al final de un módulo, endse escribe la palabra clave seguida de nuevo por el 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 una secuencia de importaciones desde diferentes módulos. Cada una de estas importaciones de módulos se inicia 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 que allindica 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 se inicia con la palabra clave correspondiente. Además, estas firmas de importación nombran las construcciones a las que se desea acceder. Además, puede haber 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 acceder a la estructura interna de un tipo en particular.
  • Exportando : Las definiciones de un módulo al que se desea que tengan acceso otros módulos se exportan utilizando la palabra clave exportsseguida de una firma del módulo de exportación. La firma del módulo de exportaciones puede consistir simplemente en la palabra clave allo como 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 se inicia con la palabra clave correspondiente. En caso de que se desee exportar la estructura interna de un tipo, se structdebe utilizar la palabra clave .
  • Funciones más exóticas : en versiones anteriores de las herramientas VDM-SL también existía soporte para 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 usaron en aplicaciones industriales y hubo una cantidad sustancial de desafíos de herramientas con estas características.

Estructuración en VDM ++

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

  • Clase : cada clase se inicia sintácticamente con la palabra clave classseguida del nombre de la clase. Al final de una clase, endse escribe la palabra clave seguida de nuevo por el 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 de nombres de superclases separados por comas.
  • 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 utilizando modificadores de acceso. En las definiciones de VDM ++ son por defecto privado, pero delante de todas las definiciones es posible usar una de las palabras clave modificador de acceso: private, publicy protected.

Funcionalidad de modelado

Modelado funcional

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 calcula un resultado, un predicado lógico sobre las variables de entrada y resultado, denominado una condición posterior , da 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:real
post r*r = x

Aquí, la condición posterior no define un método para calcular el resultado, rsino que establece qué propiedades se puede suponer que lo cumplen. Tenga en cuenta que esto define una función que devuelve una raíz cuadrada válida; no hay ningún requisito de que sea 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. Tenga en cuenta 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 fortaleciendo la condición posterior. Por ejemplo, la siguiente definición obliga a la función a devolver la raíz positiva. 

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

Todas las especificaciones de función 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 solo con números reales positivos se puede especificar de la siguiente manera: 

SQRTP(x:real)r:real
pre x >=0
post r*r = x and r>=0

La precondición y la poscondición juntas forman 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 satisfaga la condición posterior. Si se llama a una función en entradas que no satisfacen su condición previa, el resultado no está definido (de hecho, la terminación ni siquiera está garantizada).

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 of nat -> seq of nat
SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s)

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

SqListImp(s:seq of nat)r:seq of nat
post len r = len s and
     forall i in set inds s & 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 exactitud de una definición de función explícita con respecto a una especificación implícita se puede definir como sigue.

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 sif : 

forall p in set T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))

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

Modelado basado en estados

En VDM-SL, las funciones no tienen efectos secundarios como cambiar el estado de una variable global persistente. Esta es una habilidad útil en muchos lenguajes de programación, por lo que existe un concepto similar; en lugar de funciones, las operaciones se utilizan 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 definir esto en VDM-SL como: 

state Register of
  someStateRegister : nat
end

En VDM ++, esto se definiría en su lugar como: 

instance variables
  someStateRegister : nat

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

LOAD(i:nat)
ext wr someStateRegister:nat
post someStateRegister = i

La cláusula externals ( ext) especifica a qué partes del estado se puede acceder mediante la operación; rdindicando acceso de solo lectura y wrsiendo acceso de lectura / 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 se puede especificar como: 

ADD(i:nat)
ext wr someStateRegister : nat
post someStateRegister = someStateRegister~ + i

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

Ejemplos de

La función máxima

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 enteros positivos: 

max(s:set of nat)r:nat
pre card s > 0
post r in set s and
     forall r' in set s & r' <= r

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

Multiplicación de números naturales

multp(i,j:nat)r:nat
pre true
post r = i*j

Aplicar 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) ==
 if i=0
 then 0
 else if is-even(i)
      then 2*multp(i/2,j)
      else j+multp(i-1,j)

Entonces la obligación de prueba se convierte en: 

forall i, j : nat & multp(i,j):nat and multp(i, j) = i*j

Esto se puede demostrar correctamente mediante:

  1. Demostrar que la recursividad 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

Tipo de datos abstractos de cola

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

types

Qelt = token;
Queue = seq of Qelt;

state TheQueue of
  q : Queue
end

operations

ENQUEUE(e:Qelt)
ext wr q:Queue
post q = q~ ^ [e];

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

IS-EMPTY()r:bool
ext rd q:Queue
post r <=> (len q = 0)

Ejemplo de sistema bancario

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 por números de cliente ( CustNum ), las cuentas se modelan por números de cuenta ( AccNum ). Las representaciones de los números de clientes se consideran irrelevantes 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;
Balance = int;
Overdraft = nat;

AccData :: owner : CustNum
           balance : Balance

state Bank of
  accountMap : map AccNum to AccData
  overdraftMap : map CustNum to Overdraft
inv mk_Bank(accountMap,overdraftMap) == for all a in set rng accountMap & a.owner in set dom overdraftMap and
                                        a.balance >= -overdraftMap(a.owner)

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

operations
NEWC(od : Overdraft)r : CustNum
ext wr overdraftMap : map CustNum to Overdraft
post r not in set dom ~overdraftMap and overdraftMap = ~overdraftMap ++ { r |-> od};

NEWAC asigna un nuevo número de cuenta y pone el saldo a cero: 

NEWAC(cu : CustNum)r : AccNum
ext wr accountMap : map AccNum to AccData
    rd overdraftMap map CustNum to Overdraft
pre cu in set dom overdraftMap
post r not in set dom accountMap~ and accountMap = accountMap~ ++ {r|-> mk_AccData(cu,0)}

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

ACINF(cu : CustNum)r : map AccNum to Balance
ext rd accountMap : map AccNum to AccData
post r = {an |-> accountMap(an).balance | an in set dom accountMap & accountMap(an).owner = cu}

Soporte de herramientas

Varias herramientas diferentes admiten VDM:

  • VDMTools son las principales herramientas comerciales para VDM y VDM ++, propiedad, comercializadas, mantenidas y desarrolladas por CSK Systems , basadas 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, sin cargo, 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 enlaces dinámicos y soporte CORBA.
  • Overture es una iniciativa de código abierto basada en la comunidad que tiene como objetivo proporcionar soporte de herramientas disponible gratuitamente para VDM ++ en la parte superior de la plataforma Eclipse. Su objetivo es desarrollar un marco para herramientas interoperables que serán útiles para la aplicación industrial, la investigación y la educación.
  • vdm-mode es una colección de paquetes de Emacs para escribir especificaciones VDM usando 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 proporciona verificación de sintaxis, una verificación semántica simple y la generación de un archivo LaTeX que permite imprimir las especificaciones en notación matemática. Esta herramienta está disponible gratuitamente, pero no se le está dando más mantenimiento.
  • Las macros LaTeX y LaTeX2e están disponibles para admitir la presentación de modelos VDM en la sintaxis matemática del lenguaje estándar ISO. Han sido desarrollados y son mantenidos por el Laboratorio Nacional de Física del Reino Unido. La documentación y las macros están disponibles en línea.

Experiencia industrial

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

  • Compiladores Ada y CHILL : Dansk Datamatik Center desarrolló el primer compilador Ada validado en Europa utilizando VDM. 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 puerta de enlace 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 adecuada en el diseño de plantas industriales.
  • El desarrollo de VDMTools: la mayoría de los componentes del conjunto de herramientas VDMTools se desarrollan ellos mismos utilizando VDM. Este desarrollo se ha realizado en el FIDA en Dinamarca y en el CSK en Japón .
  • TradeOne: Ciertos componentes clave del sistema de back-office TradeOne desarrollado por los sistemas CSK para la bolsa de valores japonesa se desarrollaron utilizando VDM. Existen medidas comparativas para la productividad del desarrollador y la densidad de defectos de los componentes desarrollados por VDM frente al código desarrollado convencionalmente.
  • FeliCa Networks ha informado del desarrollo de un sistema operativo para un circuito integrado para aplicaciones de telefonía celular .

Refinamiento

El uso de VDM comienza con un modelo muy abstracto y lo desarrolla en una implementación. Cada paso implica la cosificación de datos y luego la descomposición de la operación .

La cosificació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 informático de elección.

Reificación de datos

La cosificación de datos (refinamiento paso a paso) 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 que se alcance 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 mostrar que la nueva representación es precisa, se define una función de recuperación que se relaciona NEW_REPcon ABS_REP, es decir retr : NEW_REP -> ABS_REP. La exactitud de una cosificación de datos depende de demostrar su idoneidad , es decir 

forall a:ABS_REP & exists 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 NEW_REP. Las nuevas operaciones y funciones deben mostrarse para preservar cualquier tipo de datos invariantes en la nueva representación. Para probar que las nuevas operaciones y funciones modelan las encontradas en la especificación original, es necesario cumplir con dos obligaciones de prueba:

  • Regla de dominio:
forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)
  • Regla de modelado:
forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))

Ejemplo de reificación de datos

En un sistema de seguridad empresarial, los trabajadores reciben tarjetas de identificación; estos se introducen en los lectores de tarjetas a la entrada y salida de la fábrica. Operaciones requeridas:

  • INIT() inicializa el sistema, asume que la fábrica está vacía
  • ENTER(p : Person)registra que un trabajador está ingresando 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 : bool comprueba si un trabajador específico está en la fábrica o no

Formalmente, esto sería: 

types

Person = token;
Workers = set of Person;

state AWCCS of
  pres: Workers
end

operations

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

ENTER(p : Person)
ext wr pres : Workers
pre p not in set pres
post pres = pres~ union {p};

EXIT(p : Person)
ext wr pres : Workers
pre p in set pres
post pres = pres~\{p};

IS-PRESENT(p : Person) r : bool
ext rd pres : Workers
post r <=> p in set 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 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 una invariante al nuevo tipo de datos. En este caso, ordenar no es importante, por lo que [a,b]es lo mismo que [b,a].

El método de desarrollo de Viena es valioso para los sistemas basados ​​en modelos. No es apropiado si el sistema se basa en el tiempo. Para tales casos, el cálculo de sistemas de comunicación (CCS) es más útil.

Ver también

Otras lecturas

  • Bjørner, Dines; Cliff B. Jones (1978). El método de desarrollo de Viena: el metalenguaje, notas de clase en informática 61 . Berlín, Heidelberg, Nueva York: Springer. ISBN 978-0-387-08766-5.
  • O'Regan, Gerard (2006). Enfoques matemáticos de 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 conferencias en Ciencias de la Computación . 177 . Berlín, Heidelberg, Nueva York, Tokio: Springer-Verlag. doi : 10.1007 / BFb0048933 . ISBN 978-3-540-13378-0.
  • Fitzgerald, JS y Larsen, PG, 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 pub. Iwanami Shoten 2003 ISBN  4-00-005609-3 ).
  • Fitzgerald, JS , Larsen, PG, Mukherjee, P., Plat, N. y Verhoef, M., Diseños validados para sistemas orientados a objetos . Springer Verlag 2005. ISBN  1-85233-881-4 . El sitio web de soporte [1] incluye ejemplos y soporte de herramientas gratuito.
  • Jones, CB , Desarrollo de software sistemático utilizando VDM , Prentice Hall 1990. ISBN  0-13-880733-7 . También disponible en línea y sin cargo: 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, The VDM-SL Reference Guide , 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 del 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 caso 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., Proof in VDM: a Practitioner's Guide . Springer Verlag Enfoques formales de la informática y la tecnología de la información (FACIT), 1994. ISBN  3-540-19813-X .

Referencias

enlaces externos