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. Con origen en un trabajo realizado en el Laboratorio IBM de Viena [1] en la década de 1970, 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 soporta 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 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 lógica para la informática .
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 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 puedan analizarse mediante pruebas y ejecutarse 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 Laboratorio IBM en Viena , donde la primera versión del lenguaje se llamó V ienna D efinition Language (VDL). [3] El VDL se utilizó esencialmente para dar descripciones semánticas operativas en contraste con el VDM – Meta-IV que proporcionaba semántica denotacional [4]
«A 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 lengua. El enfoque general adoptado ha sido denominado el "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 "formal documento de normas escrito como 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.
Entonces Meta-IV fue "usado para definir partes importantes" del lenguaje de programación PL/I . Otros lenguajes de programación descritos retrospectivamente, o parcialmente descritos, 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 de Inglés" derivó 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 generalmente se describe a través de operaciones que pueden tener efectos secundarios en el estado y que en su mayoría se especifican implícitamente mediante 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 especificaciones operativas explícitas utilizadas 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).
La sintaxis y semántica de VDM-SL y VDM++ se describen detalladamente en los manuales del lenguaje 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 sobre los datos. Consiste en una serie de definiciones de tipos de datos y funciones u operaciones realizadas sobre ellos.
VDM-SL incluye tipos básicos de modelado de números y caracteres de la siguiente manera:
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 tipos ya introducidos. Por ejemplo, un tipo que modela identificadores de usuario para un sistema de gestión de inicio de sesión podría definirse de la siguiente manera:
tiposID de usuario = 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 ni una precisión para los números reales. Estas restricciones se definen cuando son necesarias 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, el requisito de que los identificadores de usuario no sean mayores que 9999 se expresaría de la siguiente manera (donde <=está el operador booleano "menor o igual a" en números naturales):
ID de usuario = natinv uid == uid <= 9999
Dado que los invariantes pueden ser expresiones lógicas arbitrariamente complejas y la pertenencia a un tipo definido se limita únicamente 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 caracteres. En algunos casos, la representación de un tipo no es relevante para el propósito del modelo y sólo 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 su 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 mismo. Los valores de los tipos de cotizaciones (conocidos como cotizaciones literales) solo se pueden comparar para determinar su igualdad.
Por ejemplo, al modelar un controlador de señales de tráfico, puede resultar conveniente definir valores para representar los colores de la señal de tráfico como tipos de cotizaciones:
<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 señal = <Rojo> | <Ámbar> | <Ámbar intermitente> | <Verde>
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, 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 ... nota: un
es el producto cartesiano con campos etiquetados f1,…,fn. Un elemento de tipo Tpuede estar compuesto a partir de sus partes constituyentes mediante un constructor, escrito mk_T. Por el contrario, dado un elemento de tipo T, los nombres de los campos se pueden usar para seleccionar el componente nombrado. Por ejemplo, el tipo
Fecha :: día:nat1 mes:nat1 año: natinv 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 podrían 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 desordenadas en las que se suprime la duplicación entre valores. Las secuencias son colecciones (listas) ordenadas finitas en las que puede ocurrir duplicación y las asignaciones representan correspondencias finitas entre dos conjuntos de valores.
El constructor de tipos de conjuntos (escrito set of Tdonde Thay 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 ID de usuario
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.
El constructor de tipos 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 carácter
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, seleccionar el quinto elemento de una secuencia que contiene solo tres elementos no está definido.
El orden y la repetición de los 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].
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 de conjuntos de T1valores a conjuntos de T2valores. Por ejemplo, la definición de tipo
Cumpleaños = mapa Cadena hasta la fecha
Define un tipo Birthdaysque asigna cadenas de caracteres a Date. Nuevamente, los operadores se definen en las asignaciones para indexar en la asignación, fusionar asignaciones, sobrescribir y extraer sub-asignaciones.
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 tradicional orientado a objetos con clases y herencia.
En la norma ISO para VDM-SL existe un anexo informativo que contiene diferentes principios estructurantes. Todos estos siguen principios tradicionales de ocultación de información con módulos y se pueden explicar como:
moduleseguida del nombre del módulo. Al final de un módulo endse escribe la palabra clave seguida nuevamente del nombre del módulo.importsy sigue por una secuencia de importaciones de diferentes módulos. Cada una de estas importaciones de módulos comienza con la palabra clave fromseguida del nombre del módulo y la 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 importarlas. Para los tipos, también es necesario utilizar la palabra clave structsi se desea acceder a la estructura interna de un tipo en particular.exportsseguida de una firma de módulo de exportación. La firma del módulo de exportaciones puede consistir simplemente en la palabra clave allo en una secuencia de firmas de exportación. Estas 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.En VDM++ la estructuración se realiza mediante clases y herencia múltiple. Los conceptos clave son:
classseguida del nombre de la clase. Al final de una clase endse escribe la palabra clave seguida nuevamente del nombre de la clase.is subclass ofseguidas de una lista de nombres de superclases separados por comas.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 calcula un resultado, un predicado lógico sobre las variables de entrada y resultado, denominado poscondició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:realpublicar r*r = x
Aquí la poscondición no define un método para calcular el resultado r, sino que establece qué propiedades se puede suponer que tiene. 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 poscondición. Por ejemplo, la siguiente definición restringe la función para que devuelva la raíz positiva.
SQRT(x:nat)r:realpublicar 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 satisfacen cuando se ejecuta la función. Por ejemplo, una función de cálculo de raíz cuadrada que funcione sólo con números reales positivos podría especificarse de la siguiente manera:
SQRTP(x:real)r:realpre x >=0publicar r*r = x y r>=0
La condición previa y la condición posterior 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 con 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 modo de 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: secuencia de nat -> secuencia de natSqList(s) == si s = [] entonces [] else [(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 natpost len r = len s y para todo i en el conjunto 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 de la siguiente manera.
Dada una especificación implícita:
f(p:T_p)r:T_rpre pre-f(p)post-f(p,r)
y una función explícita:
f:T_p -> T_r
decimos que satisface la especificación si :
forall p en el conjunto T_p & 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 habilidad útil en muchos lenguajes de programación, por lo que existe un concepto similar; en lugar de funciones, se utilizan operaciones para cambiar variables de estado (también conocidas como globales ).
Por ejemplo, si tenemos un estado formado por una única variable someStateRegister : nat, esto lo podríamos definir en VDM-SL como:
Registro estatal de algúnRegistroEstado: natfin
En VDM++ esto se definiría como:
variables de instancia algúnRegistroEstado: nat
Una operación para cargar un valor en esta variable podría especificarse como:
CARGAR(i:nat)ext wr algúnRegistroEstado:natpublicar algúnRegistroEstado = i
La cláusula externaext ( ) especifica a qué partes del estado puede acceder la operación; rdindicando acceso de sólo lectura y wrsiendo acceso de lectura/escritura.
A veces es importante hacer referencia al valor de un estado antes de que fuera modificado; por ejemplo, una operación para agregar un valor a la variable se puede especificar como:
AÑADIR(i:nat)ext wr algún registro de estado: natpublicar algúnRegistroEstado = algúnRegistroEstado~ + 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.
Este es un ejemplo de definición de función implícita. La función devuelve el elemento más grande de un conjunto de números enteros positivos:
max(s:conjunto de nat)r:nattarjeta previa s > 0publicar r en el conjunto s y forall r' en el conjunto 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 un conjunto s cuando el conjunto está vacío.
multp(i,j:nat)r:natpre ciertopublicación 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:
multip(i,j) == si yo = 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 & multp(i,j):nat y multp(i, j) = i*j
Esto se puede demostrar correcto mediante:
Este es un ejemplo clásico que ilustra el uso de una especificación de operación implícita en un modelo basado en estados de una estructura de datos conocida. La cola se modela como una secuencia compuesta por elementos de un tipo Qelt. La representación es Qeltirrelevante y por eso se define como un tipo de token.
tipos
Qelt = ficha;Cola = secuencia de Qelt;
estado La Cola de q : colafin
operaciones
ENCOLAR(e:Qelt)text wr q: colapublicar q = q~ ^ [e];
DEQUEUE()e:Qelttext wr q: colapre q <> []publicar q~ = [e]^q;
ESTÁ VACÍO()r:boolext rd q: colapublicar 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 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.
Número de cuenta = token;NúmCliente = token;Saldo = int;Sobregiro = nat;
AccData :: propietario: CustNum saldo : Saldo
banco estatal de accountMap: asignar AccNum a AccData overdraftMap: asigna CustNum a Sobregiroinv mk_Bank(accountMap,overdraftMap) == para todos los a en set rng accountMap & a.owner en set dom overdraftMap y a.saldo >= -overdraftMap(a.propietario)
Con operaciones: NEWC asigna un nuevo número de cliente:
operacionesNEWC(od: Sobregiro)r: CustNumext wr overdraftMap: asignar CustNum a Sobregiropublicar r no en set dom ~overdraftMap y overdraftMap = ~overdraftMap ++ { r |-> od};NEWAC asigna un nuevo número de cuenta y pone el saldo a cero:
NEWAC(cu: NumCliente)r: NumAccext wr accountMap: asignar AccNum a AccData 3er sobregiroMapa mapear CustNum a Sobregiropre cu in set dom overdraftMappublicar r no en set 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 de número de cuenta a saldo:
ACINF(cu: CustNum)r: asignar AccNum al saldoext rd accountMap: asigna AccNum a AccDatapublicar r = {un |-> accountMap(un).saldo | un mapa de cuenta dom en el conjunto y mapa de cuenta (an). propietario = cu}Varias herramientas diferentes admiten VDM:
VDM se ha aplicado ampliamente en una variedad de dominios de aplicación. Las más conocidas de estas aplicaciones son:
El uso de VDM comienza con un modelo muy abstracto y lo desarrolla hasta convertirlo en una implementación. Cada paso implica la cosificación de los datos y luego la descomposición de la operación .
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 (abstractas) implícitas de operaciones y funciones en algoritmos que pueden implementarse directamente en el lenguaje informático de su elección.
La reificació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 alcanzar una implementación. Cada paso de reificación de una representación de datos abstractos 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 exactitud de una cosificación de datos depende de que se demuestre su idoneidad , es decir
para todos 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 funcionen en NEW_REP. Las nuevas operaciones y funciones deben mostrarse para preservar cualquier tipo de datos invariantes en la nueva representación. Para demostrar que las nuevas operaciones y funciones modelan las encontradas en la especificación original, es necesario cumplir con dos obligaciones de prueba:
forall r: NEW_REP y pre-OPA(retr(r)) => pre-OPR(r)
forall ~r,r:NEW_REP & 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; estos se introducen en lectores de tarjetas al entrar y salir de la fábrica. Operaciones requeridas:
![{\displaystyle {\begin{array}{|rcl|}{\textbf {Especificación}}&&{\textbf {Implementación}}\\\hline {\text{Tipo de datos abstractos}}&\xrightarrow {\text{Datos reificación}} &{\text{Estructura de datos}}\\{\text{Operaciones}}&{\xrightarrow[{\text{Operación descomposición}}]{}}&{\text{Algoritmos}}\end{array }}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e7cfd927beebe328e3bd51537dffb7316579b2b7)
INIT()Inicializa el sistema, supone que la fábrica está vacía.ENTER(p : Person)registra que un trabajador ingresa a la fábrica; los datos de los trabajadores se leen en el DNI)EXIT(p : Person)registra que un trabajador está saliendo de la fábricaIS-PRESENT(p : Person) r : boolComprueba si un trabajador específico está en la fábrica o no.Formalmente esto sería:
tipos
Persona = ficha;Trabajadores = conjunto de Persona;
AWCCS estatal de prensa: Trabajadoresfin
operaciones
EN ESO()ext wr pres: Trabajadorespublicar pres = {};ENTRAR(p: Persona)ext wr pres: Trabajadorespre p no en set prespost pres = pres~ unión {p};SALIR(p: Persona)ext wr pres: Trabajadorespre p en establecer prespublicar pres = pres~\{p};ESTÁ PRESENTE (p: Persona) r: boolext rd pres: Trabajadorespublicar r <=> p en 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 repetición, ya que no queremos que aparezca dos veces el mismo trabajador, por lo que debemos agregar un invariante al nuevo tipo de datos. En este caso, el orden no es importante, también [a,b]lo es [b,a].
El Método de Desarrollo de Viena es valioso para sistemas basados en modelos. No es apropiado si el sistema se basa en el tiempo. Para tales casos, el cálculo de sistemas comunicantes (CCS) es más útil.