Método de Desenvolvimento de Viena - Vienna Development Method

O Método de Desenvolvimento de Viena ( VDM ) é um dos métodos formais mais antigos para o desenvolvimento de sistemas baseados em computador. Originado no trabalho realizado no IBM Laboratory Vienna na década de 1970, ele cresceu para incluir um grupo de técnicas e ferramentas baseadas em uma linguagem de especificação formal - a VDM Specification Language (VDM-SL). Possui uma forma estendida, VDM ++, que suporta a modelagem de sistemas orientados a objetos e concorrentes. O suporte para VDM inclui ferramentas comerciais e acadêmicas para análise de modelos, incluindo suporte para teste e comprovação de propriedades de modelos e geração de código de programa a partir de modelos VDM validados. Há uma história de uso industrial de VDM e suas ferramentas e um crescente corpo de pesquisa no formalismo levou a contribuições notáveis ​​para a engenharia de sistemas críticos, compiladores , sistemas concorrentes e em lógica para ciência da computação .

Filosofia

Os sistemas de computação podem ser modelados em VDM-SL em um nível de abstração mais alto do que é possível usar linguagens de programação, permitindo a análise de projetos e identificação de recursos-chave, incluindo defeitos, em um estágio inicial de desenvolvimento do sistema. Os modelos que foram validados podem ser transformados em projetos de sistema detalhados por meio de um processo de refinamento. A linguagem possui uma semântica formal, possibilitando a comprovação das propriedades dos modelos com um alto nível de segurança. Ele também possui um subconjunto executável, para que os modelos possam ser analisados ​​por meio de testes e possam ser executados por meio de interfaces gráficas com o usuário, para que os modelos possam ser avaliados por especialistas que não necessariamente estão familiarizados com a linguagem de modelagem em si.

História

As origens de VDM-SL encontram-se na IBM Laboratório em Viena , onde a primeira versão da linguagem foi chamado o V ienna D DEFINIÇÃO G anguage (VDL). O VDL foi essencialmente usado para fornecer descrições semânticas operacionais em contraste com o VDM - Meta-IV que fornecia semântica denotacional

«No final de 1972, o grupo de Viena voltou sua atenção para o problema de desenvolver sistematicamente um compilador a partir de uma definição de linguagem. A abordagem geral adotada foi denominada "Método de Desenvolvimento de Viena" ... A meta-linguagem realmente adotada ("Meta-IV") é usada para definir partes principais do PL / 1 (conforme fornecido no ECMA 74 - curiosamente um "formal documento de normas escrito como um intérprete abstrato ") em BEKIČ 74.»

Não há conexão entre o Meta-IV e a linguagem Meta-II de Schorre , ou seu sucessor, o Tree Meta ; estes eram sistemas compilador-compilador em vez de serem adequados para descrições de problemas formais.

Portanto, o Meta-IV foi "usado para definir as principais partes" da linguagem de programação PL / I. Outras linguagens de programação descritas retrospectivamente, ou parcialmente descritas, usando Meta-IV e VDM-SL incluem a linguagem de programação BASIC , FORTRAN , a linguagem de programação APL , ALGOL 60, a linguagem de programação Ada e a linguagem de programação Pascal . O Meta-IV evoluiu para várias variantes, geralmente descritas como escolas dinamarquesas, inglesas e irlandesas.

A "Escola de Inglês" derivou do trabalho de Cliff Jones sobre os aspectos do VDM não especificamente relacionados à definição da linguagem e ao design do compilador (Jones 1980, 1990). Ele enfatiza a modelagem de estado persistente por meio do uso de tipos de dados construídos a partir de uma rica coleção de tipos de base. A funcionalidade é tipicamente descrita por meio de operações que podem ter efeitos colaterais no estado e que são principalmente especificadas implicitamente usando uma pré-condição e uma pós-condição. A "Escola Dinamarquesa" ( Bjørner et al. 1982) tendeu a enfatizar uma abordagem construtiva com especificações operacionais explícitas usadas em maior extensão. O trabalho na escola dinamarquesa levou ao primeiro compilador Ada validado na Europa .

Um padrão ISO para a linguagem foi lançado em 1996 (ISO, 1996).

Recursos VDM

A sintaxe e semântica do VDM-SL e VDM ++ são descritas detalhadamente nos manuais de linguagem do VDMTools e nos textos disponíveis. O padrão ISO contém uma definição formal da semântica da linguagem. No restante deste artigo, a sintaxe ISO-defined interchange (ASCII) é usada. Alguns textos preferem uma sintaxe matemática mais concisa .

Um modelo VDM-SL é uma descrição do sistema dada em termos da funcionalidade executada nos dados. Consiste em uma série de definições de tipos de dados e funções ou operações executadas sobre eles.

Tipos básicos: tipos numéricos, caracteres, token e aspas

VDM-SL inclui números de modelagem de tipos básicos e caracteres como segue:

Tipos Básicos

bool	Tipo de dados booleano	falso verdadeiro
nat	números naturais (incluindo zero)	0, 1, 2, 3, 4, 5 ...
nat1	números naturais (excluindo zero)	1, 2, 3, 4, 5, ...
int	inteiros	..., −3, −2, −1, 0, 1, 2, 3, ...
rat	números racionais	a / b , onde a e b são inteiros, b não é 0
real	numeros reais	...
char	personagens	A, B, C, ...
token	tokens sem estrutura	...
<A>	o tipo de cotação contendo o valor <A>	...

Os tipos de dados são definidos para representar os dados principais do sistema modelado. Cada definição de tipo introduz um novo nome de tipo e fornece uma representação em termos dos tipos básicos ou em termos de tipos já introduzidos. Por exemplo, um tipo de modelagem de identificadores de usuário para um sistema de gerenciamento de login pode ser definido da seguinte forma:

types
UserId = nat

Para manipular valores pertencentes a tipos de dados, os operadores são definidos nos valores. Assim, adição de número natural, subtração etc. são fornecidos, assim como os operadores booleanos, como igualdade e desigualdade. A linguagem não fixa um número máximo ou mínimo representável ou uma precisão para números reais. Essas restrições são definidas onde são exigidas em cada modelo por meio de invariantes de tipo de dados - expressões booleanas que denotam condições que devem ser respeitadas por todos os elementos do tipo definido. Por exemplo, um requisito de que os identificadores de usuário não sejam maiores que 9999 seria expresso da seguinte forma (onde <=é o operador booleano "menor ou igual a" em números naturais):

UserId = nat
inv uid == uid <= 9999

Uma vez que invariantes podem ser expressões lógicas arbitrariamente complexas e a associação de um tipo definido é limitada a apenas aqueles valores que satisfazem o invariante, a correção de tipo em VDM-SL não é automaticamente decidida em todas as situações.

Os outros tipos básicos incluem char para caracteres. Em alguns casos, a representação de um tipo não é relevante para o propósito do modelo e apenas aumentaria a complexidade. Nesses casos, os membros do tipo podem ser representados como tokens sem estrutura. Os valores dos tipos de token só podem ser comparados quanto à igualdade - nenhum outro operador é definido neles. Onde valores nomeados específicos são necessários, eles são introduzidos como tipos de cotação. Cada tipo de cotação consiste em um valor nomeado com o mesmo nome do próprio tipo. Os valores dos tipos de cotação (conhecidos como literais de cotação) só podem ser comparados por igualdade.

Por exemplo, ao modelar um controlador de semáforo, pode ser conveniente definir valores para representar as cores do semáforo como tipos de cotação:

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

Construtores de tipo: união, produto e tipos compostos

Os tipos básicos por si só são de valor limitado. Novos tipos de dados mais estruturados são criados usando construtores de tipo.

Construtores de tipo básico

T1 | T2 | ... | Tn	União de tipos T1,...,Tn
T1*T2*...*Tn	Produto cartesiano de tipos T1,...,Tn
T :: f1:T1 ... fn:Tn	Tipo composto (registro)

O construtor de tipo mais básico forma a união de dois tipos predefinidos. O tipo (A|B)contém todos os elementos do tipo A e todos do tipo B. No exemplo do controlador de sinal de tráfego, o tipo de modelagem da cor de um sinal de tráfego pode ser definido da seguinte forma:

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

Os tipos enumerados no VDM-SL são definidos conforme mostrado acima como uniões em tipos de cotação.

Os tipos de produtos cartesianos também podem ser definidos em VDM-SL. O tipo (A1*…*An)é o tipo composto de todas as tuplas de valores, sendo que o primeiro elemento é do tipo A1e o segundo do tipo A2e assim por diante. O tipo composto ou de registro é um produto cartesiano com rótulos para os campos. O tipo

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

é o produto cartesiano com campos rotulados f1,…,fn. Um elemento de tipo Tpode ser composto de suas partes constituintes por um construtor, escrito mk_T. Por outro lado, dado um elemento do tipo T, os nomes dos campos podem ser usados ​​para selecionar o componente nomeado. Por exemplo, o tipo

Date :: day:nat1
        month:nat1
        year:nat
inv mk_Date(d,m,y) == d <=31 and m<=12

modela um tipo de data simples. O valor mk_Date(1,4,2001)corresponde a 1 de abril de 2001. Dada uma data d, a expressão d.monthé um número natural que representa o mês. Restrições em dias por mês e anos bissextos podem ser incorporadas ao invariante, se desejado. Combinando estes:

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

Coleções

Os tipos de coleção modelam grupos de valores. Conjuntos são coleções não ordenadas finitas nas quais a duplicação entre os valores é suprimida. As sequências são coleções ordenadas finitas (listas) nas quais a duplicação pode ocorrer e os mapeamentos representam correspondências finitas entre dois conjuntos de valores.

Jogos

O construtor de tipo de conjunto (escrito set of Tonde Té um tipo predefinido) constrói o tipo composto de todos os conjuntos finitos de valores extraídos do tipo T. Por exemplo, a definição de tipo

UGroup = set of UserId

define um tipo UGroupcomposto de todos os conjuntos finitos de UserIdvalores. Vários operadores são definidos em conjuntos para construir sua união, interseções, determinar relacionamentos de subconjunto adequados e não estritos, etc.

Operadores principais em conjuntos (s, s1, s2 são conjuntos)

{a, b, c}	Set enumeração: o conjunto de elementos a, bec
{x | x:T & P(x)}	Conjunto de compreensão: o conjunto de xtipo de Ttal queP(x)
{i, ..., j}	O conjunto de inteiros no intervalo idej
e in set s	e é um elemento do conjunto s
e not in set s	e não é um elemento do conjunto s
s1 union s2	União de conjuntos s1es2
s1 inter s2	Interseção de conjuntos s1es2
s1 \ s2	Defina a diferença de conjuntos s1es2
dunion s	União distribuída de conjunto de conjuntos s
s1 psubset s2	s1 é um subconjunto (adequado) de s2
s1 subset s2	s1 é um subconjunto (fraco) de s2
card s	A cardinalidade do conjunto s

Seqüências

O construtor de tipo de sequência finita (escrito seq of Tonde Té um tipo predefinido) constrói o tipo composto de todas as listas finitas de valores extraídas do tipo T. Por exemplo, a definição de tipo

String = seq of char

Define um tipo Stringcomposto de todas as cadeias finitas de caracteres. Vários operadores são definidos em sequências para construir concatenação, seleção de elementos e subsequências, etc. Muitos desses operadores são parciais no sentido de que não são definidos para certas aplicações. Por exemplo, selecionar o quinto elemento de uma sequência que contém apenas três elementos é indefinido.

A ordem e a repetição dos itens em uma sequência são significativas, portanto, [a, b]não é igual a [b, a]e [a]não é igual a [a, a].

Operadores principais em sequências (s, s1, s2 são sequências)

[a, b, c]	Enumeração de sequência: a sequência de elementos a, bec
[f(x) | x:T & P(x)]	Compreensão da sequência: sequência de expressões f(x)para cada xtipo (numérico) de Ttal forma que P(x)mantém ( xvalores tomados em ordem numérica)
hd s	A cabeça (primeiro elemento) de s
tl s	A cauda (sequência restante após a remoção da cabeça) de s
len s	O comprimento do s
elems s	O conjunto de elementos de s
s(i)	O iº elemento des
inds s	o conjunto de índices para a sequência s
s1^s2	a sequência formada pela concatenação de sequências s1es2

Mapas

Um mapeamento finito é uma correspondência entre dois conjuntos, o domínio e o intervalo, com os elementos de indexação do domínio do intervalo. Portanto, é semelhante a uma função finita. O construtor de tipo de mapeamento em VDM-SL (escrito map T1 to T2onde T1e T2são tipos predefinidos) constrói o tipo composto de todos os mapeamentos finitos de conjuntos de T1valores para conjuntos de T2valores. Por exemplo, a definição de tipo

Birthdays = map String to Date

Define um tipo para o Birthdaysqual mapeia cadeias de caracteres Date. Novamente, os operadores são definidos em mapeamentos para indexar no mapeamento, mesclar mapeamentos, sobrescrever e extrair submapeamentos.

Operadores principais em mapeamentos

{a |-> r, b |-> s}	Enumeração de mapeamento: amapeia para r, bmapeia paras
{x |-> f(x) | x:T & P(x)}	Compreensão de mapeamento: xmapeia para f(x)para todos os xtipos de Tmodo queP(x)
dom m	O domínio de m
rng m	O alcance de m
m(x)	m aplicado a x
m1 munion m2	União de mapeamentos m1e m2( m1, m2deve ser consistente, onde eles se sobrepõem)
m1 ++ m2	m1 sobrescrito por m2

Estruturante

A principal diferença entre as notações VDM-SL e VDM ++ é a forma como a estruturação é tratada. No VDM-SL, há uma extensão modular convencional, enquanto o VDM ++ tem um mecanismo de estruturação tradicional orientado a objetos com classes e herança.

Estruturação em VDM-SL

No padrão ISO para VDM-SL existe um anexo informativo que contém diversos princípios estruturantes. Todos eles seguem os princípios tradicionais de ocultação de informações com módulos e podem ser explicados como:

• Nomenclatura do módulo : cada módulo é iniciado sintaticamente com a palavra-chave moduleseguida pelo nome do módulo. No final de um módulo, a palavra end- chave é escrita, seguida novamente pelo nome do módulo.
• Importando : é possível importar definições que foram exportadas de outros módulos. Isso é feito em uma seção de importações que é iniciada com a palavra-chave importse seguida por uma sequência de importações de diferentes módulos. Cada uma dessas importações de módulo é iniciada com a palavra-chave fromseguida pelo nome do módulo e uma assinatura do módulo. A assinatura do módulo pode ser simplesmente a palavra-chave que allindica a importação de todas as definições exportadas desse módulo ou pode ser uma sequência de assinaturas de importação. As assinaturas de importação são específicas para tipos, valores, funções e operações e cada uma delas é iniciada com a palavra-chave correspondente. Além disso, essas assinaturas de importação nomeiam as construções às quais há um desejo de obter acesso. Além disso, informações de tipo opcionais podem estar presentes e, finalmente, é possível renomear cada uma das construções na importação. Para os tipos, é necessário também usar a palavra-chave structse quisermos obter acesso à estrutura interna de um tipo específico.
• Exportando : As definições de um módulo ao qual se deseja que outros módulos tenham acesso são exportadas usando a palavra-chave exportsseguida por uma assinatura do módulo de exportação. A assinatura do módulo de exportação pode consistir simplesmente na palavra-chave allou em uma sequência de assinaturas de exportação. Essas assinaturas de exportação são específicas para tipos, valores, funções e operações e cada uma delas é iniciada com a palavra-chave correspondente. Caso se deseje exportar a estrutura interna de um tipo structdeve-se utilizar a palavra-chave .
• Recursos mais exóticos : Em versões anteriores das ferramentas VDM-SL, também havia suporte para módulos parametrizados e instanciações de tais módulos. No entanto, esses recursos foram retirados do VDMTools por volta de 2000 porque raramente eram usados ​​em aplicações industriais e havia um número substancial de desafios de ferramentas com esses recursos.

Estruturação em VDM ++

Em VDM ++, a estruturação é feita usando classes e herança múltipla. Os conceitos-chave são:

• Classe : cada classe é iniciada sintaticamente com a palavra-chave classseguida pelo nome da classe. No final de uma classe, a palavra end- chave é escrita, seguida novamente pelo nome da classe.
• Herança : no caso de uma classe herdar construções de outras classes, o nome da classe no título da classe pode ser seguido pelas palavras-chave is subclass ofseguidas por uma lista separada por vírgulas de nomes de superclasses.
• Modificadores de acesso : as informações ocultas no VDM ++ são feitas da mesma maneira que na maioria das linguagens orientadas a objetos usando modificadores de acesso. Em definições VDM ++ são por padrão privado, mas na frente de todas as definições, é possível usar uma das palavras-chave de acesso modificadoras: private, publice protected.

Funcionalidade de modelagem

Modelagem funcional

No VDM-SL, as funções são definidas sobre os tipos de dados definidos em um modelo. O suporte para abstração requer que seja possível caracterizar o resultado que uma função deve calcular, sem ter que dizer como deve ser computada. O principal mecanismo para fazer isso é a definição de função implícita na qual, em vez de uma fórmula computando um resultado, um predicado lógico sobre as variáveis ​​de entrada e resultado, denominado uma pós - condição , fornece as propriedades do resultado. Por exemplo, uma função SQRTpara calcular a raiz quadrada de um número natural pode ser definida da seguinte forma:

SQRT(x:nat)r:real
post r*r = x

Aqui, a pós-condição não define um método para calcular o resultado, rmas declara quais propriedades podem ser consideradas válidas para ele. Observe que isso define uma função que retorna uma raiz quadrada válida; não há exigência de que seja a raiz positiva ou negativa. A especificação acima seria satisfeita, por exemplo, por uma função que retornasse a raiz negativa de 4, mas a raiz positiva de todas as outras entradas válidas. Observe que as funções no VDM-SL devem ser determinísticas, de forma que uma função que satisfaça a especificação do exemplo acima sempre retorne o mesmo resultado para a mesma entrada.

Uma especificação de função mais restrita é obtida fortalecendo a pós-condição. Por exemplo, a definição a seguir restringe a função para retornar a raiz positiva.

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

Todas as especificações de função podem ser restritas por pré-condições que são predicados lógicos sobre as variáveis ​​de entrada apenas e que descrevem restrições que são consideradas satisfeitas quando a função é executada. Por exemplo, uma função de cálculo de raiz quadrada que funciona apenas em números reais positivos pode ser especificada da seguinte maneira:

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

A pré-condição e a pós-condição juntas formam um contrato que deve ser satisfeito por qualquer programa que pretenda implementar a função. A pré-condição registra as suposições sob as quais a função garante retornar um resultado que satisfaça a pós-condição. Se uma função é chamada em entradas que não satisfazem sua pré-condição, o resultado é indefinido (na verdade, o encerramento nem mesmo é garantido).

O VDM-SL também suporta a definição de funções executáveis ​​na forma de uma linguagem de programação funcional. Em uma definição de função explícita , o resultado é definido por meio de uma expressão nas entradas. Por exemplo, uma função que produz uma lista dos quadrados de uma lista de números pode ser definida da seguinte maneira:

SqList: seq of nat -> seq of nat
SqList(s) == if s = [] then [] else [(hd s)**2] ^ SqList(tl s)

Esta definição recursiva consiste em uma assinatura de função fornecendo os tipos de entrada e resultado e um corpo de função. Uma definição implícita da mesma função pode assumir a seguinte 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

A definição explícita é, em um sentido simples, uma implementação da função especificada implicitamente. A exatidão de uma definição de função explícita com respeito a uma especificação implícita pode ser definida como segue.

Dada uma especificação implícita:

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

e uma função explícita:

f:T_p -> T_r

dizemos que satisfaz a especificação iff :

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

Portanto, " fé uma implementação correta" deve ser interpretado como " fsatisfaz a especificação".

Modelagem baseada em estado

No VDM-SL, as funções não têm efeitos colaterais, como alterar o estado de uma variável global persistente. Esta é uma habilidade útil em muitas linguagens de programação, portanto, existe um conceito semelhante; em vez de funções, as operações são usadas para alterar as variáveis ​​de estado (também conhecidas como globais ).

Por exemplo, se temos um estado que consiste em uma única variável someStateRegister : nat, podemos definir isso no VDM-SL como:

state Register of
  someStateRegister : nat
end

Em VDM ++, isso seria definido como:

instance variables
  someStateRegister : nat

Uma operação para carregar um valor nesta variável pode ser especificada como:

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

A cláusula externals ( ext) especifica quais partes do estado podem ser acessadas pela operação; rdindicando acesso somente leitura e wrsendo acesso de leitura / gravação.

Às vezes, é importante referir-se ao valor de um estado antes de ele ser modificado; por exemplo, uma operação para adicionar um valor à variável pode ser especificada como:

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

Onde o ~símbolo na variável de estado na pós-condição indica o valor da variável de estado antes da execução da operação.

Exemplos

A função max

Este é um exemplo de definição de função implícita. A função retorna o maior elemento de um conjunto de inteiros 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

A pós-condição caracteriza o resultado ao invés de definir um algoritmo para obtê-lo. A pré-condição é necessária porque nenhuma função poderia retornar um r em conjuntos quando o conjunto está vazio.

Multiplicação de número natural

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

Aplicar a obrigação de prova forall p:T_p & pre-f(p) => f(p):T_r and post-f(p, f(p))a uma definição 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)

Então, a obrigação de prova torna-se:

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

Isso pode ser mostrado correto por:

1. Provar que a recursão termina (isso, por sua vez, requer provar que os números se tornam menores a cada etapa)
2. Indução matemática

Tipo de dados abstratos de fila

Este é um exemplo clássico que ilustra o uso de especificação de operação implícita em um modelo baseado em estado de uma estrutura de dados bem conhecida. A fila é modelada como uma sequência composta por elementos de um tipo Qelt. A representação é Qeltimaterial e, portanto, é definida como um 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)

Exemplo de sistema bancário

Como um exemplo muito simples de um modelo VDM-SL, considere um sistema para manter detalhes da conta bancária do cliente. Os clientes são modelados por números de clientes ( CustNum ), as contas são modeladas por números de contas ( AccNum ). As representações de números de clientes são consideradas imateriais e, portanto, são modeladas por um tipo de token. Saldos e descobertos são modelados por 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)

Com operações: NEWC atribui um novo 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 aloca um novo número de conta e define o saldo para zero:

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 retorna todos os saldos de todas as contas de um cliente, como um mapa de número de conta para equilibrar:

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}

Suporte de ferramenta

Várias ferramentas diferentes suportam VDM:

• VDMTools são as principais ferramentas comerciais para VDM e VDM ++, pertencentes, comercializadas, mantidas e desenvolvidas pela CSK Systems , com base em versões anteriores desenvolvidas pela empresa dinamarquesa IFAD. Os manuais e um tutorial prático estão disponíveis. Todas as licenças estão disponíveis, gratuitamente, para a versão completa da ferramenta. A versão completa inclui geração automática de código para Java e C ++, biblioteca de vínculo dinâmico e suporte CORBA.
• A abertura é uma iniciativa de código aberto baseada na comunidade que visa fornecer suporte de ferramenta disponível gratuitamente para VDM ++ no topo da plataforma Eclipse. Seu objetivo é desenvolver uma estrutura para ferramentas interoperáveis ​​que sejam úteis para aplicação industrial, pesquisa e educação.
• vdm-mode é uma coleção de pacotes Emacs para escrever especificações VDM usando VDM-SL, VDM ++ e VDM-RT. Suporta realce e edição de sintaxe, verificação de sintaxe em tempo real, preenchimento de modelo e suporte de intérprete.
• SpecBox : da Adelard fornece verificação de sintaxe, algumas verificações semânticas simples e geração de um arquivo LaTeX permitindo que as especificações sejam impressas em notação matemática. Esta ferramenta está disponível gratuitamente, mas não está sendo mais mantida.
• As macros LaTeX e LaTeX2e estão disponíveis para suportar a apresentação de modelos VDM na sintaxe matemática da ISO Standard Language. Eles foram desenvolvidos e são mantidos pelo National Physical Laboratory do Reino Unido. A documentação e as macros estão disponíveis online.

Experiência industrial

O VDM tem sido amplamente aplicado em uma variedade de domínios de aplicação. Os mais conhecidos desses aplicativos são:

• Compiladores Ada e CHILL : O primeiro compilador Ada validado na Europa foi desenvolvido pelo Dansk Datamatik Center usando VDM. Da mesma forma, as semânticas de CHILL e Modula-2 foram descritas em seus padrões usando VDM.
• ConForm: Um experimento na British Aerospace comparando o desenvolvimento convencional de um gateway confiável com um desenvolvimento usando VDM.
• Dust-Expert: Um projeto realizado pela Adelard no Reino Unido para uma aplicação relacionada à segurança que determina que a segurança é apropriada no layout de plantas industriais.
• O desenvolvimento de VDMTools: A maioria dos componentes do conjunto de ferramentas VDMTools são desenvolvidos usando VDM. Este desenvolvimento foi feito no IFAD na Dinamarca e no CSK no Japão .
• TradeOne: Certos componentes principais do sistema de back-office TradeOne desenvolvido pela CSK systems para a bolsa de valores japonesa foram desenvolvidos usando VDM. Existem medições comparativas para a produtividade do desenvolvedor e densidade de defeitos dos componentes desenvolvidos em VDM em relação ao código desenvolvido convencionalmente.
• A FeliCa Networks relatou o desenvolvimento de um sistema operacional para um circuito integrado para aplicações de telefonia celular .

Refinamento

O uso do VDM começa com um modelo muito abstrato e o desenvolve em uma implementação. Cada etapa envolve a reificação de dados e , em seguida , a decomposição da operação .

A reificação de dados desenvolve os tipos de dados abstratos em estruturas de dados mais concretas , enquanto a decomposição de operações desenvolve as especificações implícitas (abstratas) de operações e funções em algoritmos que podem ser implementados diretamente em uma linguagem de computador de escolha.

${\ displaystyle {\ begin {array} {| rcl |} {\ textbf {Specification}} && {\ textbf {Implementation}} \\\ hline {\ text {Abstract data type}} & \ xrightarrow {\ text {Data reificação}} & {\ text {Estrutura de dados}} \\ {\ text {Operações}} & {\ xrightarrow [{\ text {Decomposição de operações}}] {}} & {\ text {Algoritmos}} \ end {array }}}$

Reificação de dados

A reificação de dados (refinamento gradual) envolve encontrar uma representação mais concreta dos tipos de dados abstratos usados ​​em uma especificação. Pode haver várias etapas antes que uma implementação seja alcançada. Cada etapa de reificação para uma representação abstrata de dados ABS_REPenvolve a proposição de uma nova representação NEW_REP. Para mostrar que a nova representação é precisa, é definida uma função de recuperação que se relaciona NEW_REPcom ABS_REP, ie retr : NEW_REP -> ABS_REP. A correção de uma reificação de dados depende da comprovação da adequação , ou seja,

forall a:ABS_REP & exists r:NEW_REP & a = retr(r)

Como a representação dos dados mudou, é necessário atualizar as operações e funções para que operem NEW_REP. As novas operações e funções devem ser mostradas para preservar quaisquer invariantes de tipo de dados na nova representação. Para provar que as novas operações e funções modelam aquelas encontradas na especificação original, é necessário cumprir duas obrigações de prova:

• Regra de domínio:

forall r: NEW_REP & pre-OPA(retr(r)) => pre-OPR(r)

• Regra de modelagem:

forall ~r,r:NEW_REP & pre-OPA(retr(~r)) and post-OPR(~r,r) => post-OPA(retr(~r,), retr(r))

Exemplo de reificação de dados

Em um sistema de segurança empresarial, os trabalhadores recebem cartões de identificação; estes são alimentados nos leitores de cartão na entrada e saída da fábrica. Operações necessárias:

• INIT() inicializa o sistema, assume que a fábrica está vazia
• ENTER(p : Person)registra que um trabalhador está entrando na fábrica; os dados dos trabalhadores são lidos no cartão de identificação)
• EXIT(p : Person) registra que um trabalhador está saindo da fábrica
• IS-PRESENT(p : Person) r : bool verifica se um trabalhador especificado está na fábrica ou não

Formalmente, seria:

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 a maioria das linguagens de programação tem um conceito comparável a um conjunto (geralmente na forma de um array), a primeira etapa da especificação é representar os dados em termos de uma sequência. Essas sequências não devem permitir a repetição, pois não queremos que o mesmo trabalhador apareça duas vezes, portanto, devemos adicionar uma invariante ao novo tipo de dados. Nesse caso, a ordem não é importante, então [a,b]é o mesmo que [b,a].

O Método de Desenvolvimento de Viena é valioso para sistemas baseados em modelos. Não é apropriado se o sistema for baseado no tempo. Para tais casos, o cálculo de sistemas de comunicação (CCS) é mais útil.

Veja também

• Métodos formais
• Especificação formal
• Código Pidgin
• Lógica de predicado
• Cálculo proposicional
• Linguagem de especificação Z , a principal alternativa ao VDM-SL (compare)
• COMPASS Modeling Language (CML), uma combinação de VDM-SL com CSP , baseada em Teorias Unificadoras de Programação , desenvolvida para modelagem de Sistemas de Sistemas (SoS)

Leitura adicional

• Bjørner, Dines; Cliff B. Jones (1978). O Método de Desenvolvimento de Viena: A Meta-linguagem, Notas de Aula em Ciência da Computação 61 . Berlin, Heidelberg, New York: Springer. ISBN 978-0-387-08766-5.
• O'Regan, Gerard (2006). Abordagens matemáticas à qualidade de software . Londres: Springer. ISBN 978-1-84628-242-3.
• Cliff B. Jones, ed. (1984). Linguagens de programação e sua definição - H. Bekič (1936-1982) . Notas de aula em Ciência da Computação . 177 . Berlim, Heidelberg, Nova York, Tóquio: Springer-Verlag. doi : 10.1007 / BFb0048933 . ISBN 978-3-540-13378-0.
• Fitzgerald, JS e Larsen, PG, Sistemas de Modelagem: Ferramentas e Técnicas Práticas em Engenharia de Software . Cambridge University Press , 1998 ISBN  0-521-62348-0 (publicação de edição japonesa. Iwanami Shoten 2003 ISBN  4-00-005609-3 ).
• Fitzgerald, JS , Larsen, PG, Mukherjee, P., Plat, N. e Verhoef, M., Validated Designs for Object-oriented Systems . Springer Verlag 2005. ISBN  1-85233-881-4 . O site de suporte [1] inclui exemplos e suporte gratuito para ferramentas.
• Jones, CB , Systematic Software Development using VDM , Prentice Hall 1990. ISBN  0-13-880733-7 . Também disponível online e gratuitamente: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip
• Bjørner, D. e Jones, CB , Formal Specification and Software Development Prentice Hall International, 1982. ISBN  0-13-880733-7
• J. Dawes, The VDM-SL Reference Guide , Pitman 1991. ISBN  0-273-03151-1
• Organização Internacional para Padronização , Tecnologia da Informação - Linguagens de programação, seus ambientes e interfaces de software de sistema - Método de Desenvolvimento de Viena - Linguagem de Especificação - Parte 1: Linguagem base International Standard ISO / IEC 13817-1, dezembro de 1996.
• Jones, CB , Software Development: A Rigorous Approach , Prentice Hall International, 1980. ISBN  0-13-821884-6
• Jones, CB e Shaw, RC (eds.), Case Studies in Systematic Software Development , Prentice Hall International, 1990. ISBN  0-13-880733-7
• Bicarregui, JC, Fitzgerald, JS , Lindsay, PA, Moore, R. e Ritchie, B., Proof in VDM: a Practitioner's Guide . Springer Verlag Formal Approaches to Computing and Information Technology (FACIT), 1994. ISBN  3-540-19813-X .

Referências

links externos

• Informações sobre VDM e VDM ++ (cópia arquivada em archive.org)
• Linguagem de definição de Viena (VDL)