Método de Desenvolvimento de Viena

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 Laboratório IBM de Viena [1] na década de 1970, cresceu para incluir um grupo de técnicas e ferramentas baseadas em uma linguagem de especificação formal – a Linguagem de Especificação VDM (VDM-SL). Possui uma forma estendida, VDM++, [2] 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 pesquisas 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 computacionais podem ser modelados em VDM-SL em um nível de abstração mais alto do que é possível usando linguagens de programação, permitindo a análise de projetos e a identificação de características-chave, incluindo defeitos, em um estágio inicial de desenvolvimento do sistema. Os modelos que foram validados podem ser transformados em projetos detalhados de sistemas através de um processo de refinamento. A linguagem possui uma semântica formal, permitindo comprovar as propriedades dos modelos com alto nível de segurança. Também possui um subconjunto executável, para que os modelos possam ser analisados ​​por meio de testes e executados por meio de interfaces gráficas de usuário, para que os modelos possam ser avaliados por especialistas que não estão necessariamente familiarizados com a linguagem de modelagem em si.

História

As origens do VDM-SL estão no Laboratório IBM em Viena , onde a primeira versão da linguagem foi chamada de V ienna D efinition Language (VDL). [3] O VDL foi essencialmente usado para fornecer descrições semânticas operacionais em contraste com o VDM – Meta-IV que fornecia semântica denotacional [4]

«No final de 1972, o grupo de Viena voltou novamente a sua atenção para o problema do desenvolvimento sistemático de um compilador a partir de uma definição de linguagem. A abordagem geral adotada foi denominada "Método de Desenvolvimento de Viena"... A metalinguagem realmente adotada ("Meta-IV") é usada para definir porções principais do PL/1 (conforme fornecido no ECMA 74 - curiosamente, um "formal documento de padrões escrito como um intérprete abstrato") em BEKIČ 74.» [5]

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

Portanto, o Meta-IV foi "usado para definir grandes 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 diversas variantes, geralmente descritas como Escolas Dinamarquesa, Inglesa e Irlandesa.

A "Escola Inglesa" 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 do estado persistente [7] através do uso de tipos de dados construídos a partir de uma rica coleção de tipos base. A funcionalidade é normalmente 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) tende a enfatizar uma abordagem construtiva com especificações operacionais explícitas utilizadas em maior medida. O trabalho na escola dinamarquesa levou ao primeiro compilador Ada validado na Europa .

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

Recursos VDM

A sintaxe e a semântica do VDM-SL e VDM++ são descritas detalhadamente nos manuais da linguagem 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 de intercâmbio definido pela ISO (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 realizadas sobre eles.

Tipos básicos: tipos numéricos, de caracteres, de token e de cotação

VDM-SL inclui tipos básicos de números e caracteres de modelagem 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 números inteiros, b não é 0
real numeros reais ...
char personagens A,B,C,...
token tokens sem estrutura ...
<A> o tipo de cotação que contém 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 identificação de usuário de modelagem para um sistema de gerenciamento de login pode ser definido da seguinte forma:

tipos 
UserId  =  nat

Para manipular valores pertencentes a tipos de dados, operadores são definidos nos valores. Assim, são fornecidas adição, subtração de números naturais, etc., assim como operadores booleanos, como igualdade e desigualdade. A linguagem não fixa um número representável máximo ou mínimo 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 devem ser 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

Como os invariantes podem ser expressões lógicas arbitrariamente complexas e a associação a um tipo definido é limitada apenas aos valores que satisfazem o invariante, a correção do tipo no VDM-SL não é automaticamente decidível 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 acrescentaria 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 quanto à 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:

<Vermelho>, <Âmbar>, <Âmbar intermitente>, <Verde>

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

Os tipos básicos por si só têm valor limitado. Tipos de dados novos e mais estruturados são criados usando construtores de tipo.

Construtores de tipo básico
T1 | T2 | ... | Tn União de tiposT1,...,Tn
T1*T2*...*Tn Produto cartesiano de tiposT1,...,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 semáforo, o tipo que modela a cor de um semáforo pode ser definido da seguinte forma:

CorSinal  =   <Vermelho> |< Âmbar > | < Âmbar piscante > | <Verde>      

Os tipos enumerados em 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 no VDM-SL. O tipo (A1*…*An)é o tipo composto por todas as tuplas de valores, sendo o primeiro elemento do tipo A1e o segundo do tipo A2e assim por diante. O tipo composto ou registro é um produto cartesiano com rótulos para os campos. O tipo

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

é o produto cartesiano com campos rotulados como f1,…,fn. Um elemento do tipo Tpode ser composto a partir 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

Data  ::  dia : nat1 
        mês : nat1 
        ano : nat 
inv  mk_Date ( d , m , y )  ==  d  <= 31  e  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 de dias por mês e anos bissextos poderiam ser incorporadas à invariante, se desejado. Combinando estes:

data_mk ( 1 , 4 , 2001 ). mês  =  4

Coleções

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

Conjuntos

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

UGroup  =  conjunto  de  UserId

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

Operadores principais em conjuntos (s, s1, s2 são conjuntos)
{a, b, c} Enumeração de conjunto: o conjunto de elementos a, bec
{x | x:T & P(x)} Compreensão de conjunto: o conjunto do xtipo from Ttal queP(x)
{i, ..., j} O conjunto de inteiros no intervalo iatéj
e in set s eé um elemento do conjuntos
e not in set s enão é um elemento do conjuntos
s1 union s2 União de conjuntos s1es2
s1 inter s2 Interseção de conjuntos s1es2
s1 \ s2 Definir diferença de conjuntos s1es2
dunion s União distribuída de conjunto de conjuntoss
s1 psubset s2 s1 é um subconjunto (adequado) des2
s1 subset s2 s1 é um subconjunto (fraco) des2
card s A cardinalidade do conjuntos

Sequê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  =  sequência  de  char

Define um tipo Stringcomposto por todas as sequências finitas de caracteres. Vários operadores são definidos em sequências para construção de 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 determinadas aplicações. Por exemplo, selecionar o 5º 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 [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 de sequência: sequência de expressões f(x)para cada xtipo (numérico) Ttal que P(x)vale
( xvalores tomados em ordem numérica)
hd s A cabeça (primeiro elemento) des
tl s A cauda (sequência restante após a remoção da cabeça) des
len s O comprimento dos
elems s O conjunto de elementos des
s(i) O iº elemento des
inds s o conjunto de índices para a sequências
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 contradomínio, com os elementos de indexação do domínio do contradomínio. É, 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

Aniversários  =  mapear  String  até  Data

Define um tipo Birthdaysque mapeia cadeias de caracteres para Date. Novamente, os operadores são definidos nos mapeamentos para indexação no mapeamento, mesclando mapeamentos, substituindo e extraindo submapeamentos.

Principais operadores em mapeamentos
{a |-> r, b |-> s} Enumeração de mapeamento: amapas para r, bmapas paras
{x |-> f(x) | x:T & P(x)} Compreensão de mapeamento: xmapeia para f(x)todos xpara um tipo Ttal queP(x)
dom m O domínio dem
rng m O alcance dem
m(x) maplicado ax
m1 munion m2 União de mapeamentos m1e m2( m1, m2deve ser consistente onde se sobrepõem)
m1 ++ m2 m1substituído porm2

Estruturação

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

Estruturação em VDM-SL

Na norma ISO para VDM-SL existe um anexo informativo que contém diferentes 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-chave endé 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 começa 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 allque indica 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 se deseja obter acesso. Além disso, informações opcionais de tipo podem estar presentes e, finalmente, é possível renomear cada uma das construções na importação. Para tipos é necessário também usar a palavra-chave structse desejar 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 exports. A assinatura do módulo de exportação pode consistir simplesmente na palavra-chave allou como uma sequência de assinaturas de exportação. Tais 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 queira exportar a estrutura interna de um tipo structdeverá ser utilizada a palavra-chave.
  • Recursos mais exóticos : Nas versões anteriores do VDM-SL, as ferramentas também tinham 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 quase nunca eram usados ​​em aplicações industriais e havia um número substancial de desafios de ferramentas com esses recursos.

Estruturação em VDM++

No 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 aula a palavra-chave endé escrita seguida novamente do nome da classe.
  • Herança : No caso de uma classe herdar construções de outras classes, o nome da classe no cabeçalho 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 : a ocultação de informações no VDM++ é feita da mesma maneira que na maioria das linguagens orientadas a objetos usando modificadores de acesso. No VDM++ as definições são privadas por padrão, mas na frente de todas as definições é possível usar uma das palavras-chave modificadoras de acesso: 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 à abstração exige que seja possível caracterizar o resultado que uma função deve calcular sem ter que dizer como deve ser calculado. O principal mecanismo para fazer isso é a definição implícita de função na qual, em vez de uma fórmula computando um resultado, um predicado lógico sobre as variáveis ​​de entrada e resultado, denominado 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 : postagem real 
r * r = x   

Aqui, a pós-condição não define um método para calcular o resultado, rmas afirma 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 modo que uma função que satisfaça a especificação do exemplo acima deve sempre retornar 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 a retornar a raiz positiva.

SQRT ( x : nat ) r : postagem real 
r * r = x e r >= 0     

Todas as especificações de função podem ser restringidas por pré-condições que são predicados lógicos apenas sobre as variáveis ​​de entrada 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 com números reais positivos pode ser especificada da seguinte forma:

SQRTP ( x : real ) r : real 
pré  x  >= 0 
pós  r * r  =  x  e  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 for chamada em entradas que não satisfazem sua pré-condição, o resultado será indefinido (na verdade, o término nem mesmo é garantido).

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

SqList :  seq  de  nat  ->  seq  de  nat 
SqList ( s )  ==  se  s  =  []  então  []  else  [( hd  s ) ** 2 ]  ^  SqList ( tl  s )

Esta definição recursiva consiste em uma assinatura de função que fornece 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  de  nat ) r : seq  de  nat 
post  len  ​​r  =  len  s  e 
     para todos  i  no  conjunto  inds  s  &  r ( i )  =  s ( i ) ** 2

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

Dada uma especificação implícita:

f ( p : T_p ) r : T_r 
pré  pré - f ( p ) 
pós  pós - f ( p ,  r )

e uma função explícita:

f : T_p  ->  T_r

dizemos que satisfaz a especificação se :

para todos  p  no  conjunto  T_p  &  pré - f ( p )  =>  f ( p ) : T_r  e  pós - 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, operações são usadas para alterar variáveis ​​de estado (também conhecidas como globais ).

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

  Registro  estadual de 
   someStateRegister  :  nat 
 end

No VDM++, isso seria definido como:

  variáveis ​​de 
   instância 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 externalsext ( ) especifica quais partes do estado podem ser acessadas pela operação; rdindicando acesso somente leitura e wracesso 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 máxima

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 : conjunto  de  nat ) r : nat 
 pré  cartão  s  >  0 
 pós  r  no  conjunto  s  e 
      para todos  r' no conjunto s & r'  <=  r

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

Multiplicação de números naturais

 multp ( i , j : nat ) r : nat 
 pré  post verdadeiro 
 r = i * j   

Aplicando 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 )  == 
  se  i = 0 
  então  0 
  senão  se  for- par ( i ) 
       então  2 * multp ( i / 2 , j ) 
       senão  j + multp ( i - 1 , j )

Então a obrigação de prova passa a ser:

 para todos  i ,  j  :  nat  &  multp ( i , j ) : nat  e  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 ficam menores a cada passo)
  2. Indução matemática

Tipo de dados abstrato da 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.

 tipos

 Qelt  =  ficha ; 
 Fila  =  seq  de  Qelt ;

 estado  TheQueue  de 
   q  :  Fim da fila
 

 operações

 ENQUEUE ( e : Qelt ) 
 ext  wr  q : Postagem na fila 
 q = q~ ^ [ e ];     

 DEQUEUE () e : Qelt 
 ext  wr  q : Fila 
 pré  q  <>  [] 
 post  q~  =  [ e ] ^q ;

 IS - EMPTY () r : bool 
 ext  rd  q : Postagem 
 na fila  r  <=>  ( len  q  =  0 )

Exemplo de sistema bancário

Como um exemplo muito simples de 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 ( AcNum ). As representações dos números dos 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.

 NúmeroAc  =  token ; 
 CustNum  =  token ; 
 Saldo  =  int ; 
 Cheque especial  =  nat ;

 AccData  ::  proprietário  :  CustNum 
            saldo  :  Saldo

 state  Bank  of 
   accountMap  :  mapear  AccNum  para  AccData 
   overdraftMap  :  mapear  CustNum  para  Overdraft 
 inv  mk_Bank ( accountMap , overdraftMap )  ==  para  todos  a  no  conjunto  rng  accountMap  &  a . proprietário  em  set  dom  overdraftMap  e 
                                         um arquivo . saldo  >=  - cheque especialMap ( a .proprietário )

Com operações: NEWC aloca um novo número de cliente:

 operações 
 NEWC ( od  :  Cheque especial ) r  :  CustNum 
 ext  wr  overdraftMap  :  mapeia  CustNum  para  posto de cheque especial 
 r não em set dom ~overdraftMap e overdraftMap = ~overdraftMap ++ { r | -> od };               

NEWAC aloca um novo número de conta e define o saldo como zero:

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

ACINF retorna todos os saldos de todas as contas de um cliente, como mapa de número de conta para saldo:

 ACINF ( cu  :  CustNum ) r  :  mapeia  AccNum  para  Balance 
 ext  rd  accountMap  :  mapeia  AccNum  para  AccData 
 post  r  =  { an  | ->  accountMap ( um ). equilíbrio  |  um  conjunto  dom accountMap  & accountMap ( an ) . proprietário = cu }     

Suporte de ferramenta

Várias ferramentas diferentes suportam VDM:

  • VDMTools era a ferramenta comercial líder para VDM e VDM++, de propriedade, comercializada, mantida e desenvolvida 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.
  • Overture é uma iniciativa de código aberto baseada na comunidade que visa fornecer suporte de ferramenta disponível gratuitamente para todos os dialetos VDM (VDM-SL, VDM++ e VDM-RT) originalmente na plataforma Eclipse, mas posteriormente na plataforma Visual Studio Code. O seu objectivo é desenvolver um quadro para ferramentas interoperáveis ​​que serão úteis para aplicações industriais, investigação e educação.
  • vdm-mode é uma coleção de pacotes Emacs para escrever especificações VDM usando VDM-SL, VDM++ e VDM-RT. Ele suporta destaque e edição de sintaxe, verificação de sintaxe em tempo real, preenchimento de modelo e suporte a 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 mantida.
  • Macros LaTeX e LaTeX2e estão disponíveis para suportar a apresentação de modelos VDM na sintaxe matemática da linguagem padrão ISO. Eles foram desenvolvidos e são mantidos pelo Laboratório Nacional de Física do Reino Unido. A documentação e as macros estão disponíveis online.

Experiência industrial

O VDM tem sido amplamente aplicado em vários 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. [8] Da mesma forma, a semântica de CHILL e Modula-2 foi descrita 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 se a segurança é adequada no layout de plantas industriais.
  • O desenvolvimento do VDMTools: A maioria dos componentes do conjunto de ferramentas VDMTools são desenvolvidos usando VDM. Este desenvolvimento foi feito no FIDA na Dinamarca e no CSK no Japão . [9]
  • TradeOne: Certos componentes-chave do sistema de back-office TradeOne desenvolvido pelos sistemas CSK para a bolsa de valores japonesa foram desenvolvidos usando VDM. Existem medições comparativas para a produtividade do desenvolvedor e a densidade de defeitos dos componentes desenvolvidos por VDM em comparação com o código desenvolvido convencionalmente.
  • 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 dos dados e depois 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 sua escolha.

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ários passos antes de uma implementação ser alcançada. Cada etapa de reificação de uma representação abstrata de dados ABS_REPenvolve a proposta de uma nova representação NEW_REP. Para mostrar que a nova representação é precisa, é definida uma função de recuperação relacionada NEW_REPa ABS_REP, ou seja retr : NEW_REP -> ABS_REP,. A exatidão de uma reificação de dados depende da comprovação da adequação , ou seja,

 para todos  a : ABS_REP  &  existe  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  &  pré - OPA ( retr ( r ))  =>  pré - OPR ( r )
  • Regra de modelagem:
 para todos  ~r , r : NEW_REP  &  pré - OPA ( retr ( ~r ))  e  pós - OPR ( ~r , r )  =>  pós - OPA ( retr ( ~r ,),  retr ( r ))

Exemplo de reificação de dados

Num sistema de segurança empresarial, os trabalhadores recebem cartões de identificação; estes são inseridos em leitores de cartões 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 : boolverifica se um trabalhador especificado está na fábrica ou não

Formalmente, isso seria:

 tipos

 Pessoa  =  token ; 
 Trabalhadores  =  conjunto  de  Pessoa ;

 estado  AWCCS  de 
   pres :  Fim dos trabalhadores
 

 operações

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

 ENTER ( p  :  Pessoa ) 
 ext  wr  pres  :  Trabalhadores 
 pre  p  não estão  em  set  pres 
 post  pres  =  pres~  union  { p };

 EXIT ( p  :  Pessoa ) 
 ext  wr  pres  :  Trabalhadores 
 pre  p  em  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), o primeiro passo da especificação é representar os dados em termos de uma sequência. Estas sequências não devem permitir repetição, pois não queremos que o mesmo trabalhador apareça duas vezes, por isso devemos adicionar uma invariante ao novo tipo de dados. Neste 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 comunicantes (CCS) é mais útil.

Veja também

Leitura adicional

  • Bjorner, 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 . Berlim, Heidelberg, Nova York: Springer. ISBN 978-0-387-08766-5.
  • O'Regan, Gerard (2006). Abordagens matemáticas para 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 . Vol. 177. Berlim, Heidelberg, Nova York, Tóquio: Springer-Verlag. doi :10.1007/BFb0048933. ISBN 978-3-540-13378-0. S2CID7488558  .
  • Fitzgerald, JS e Larsen, PG, Modelagem de Sistemas: Ferramentas e Técnicas Práticas em Engenharia de Software . Cambridge University Press , 1998 ISBN 0-521-62348-0 (edição japonesa pub. Iwanami Shoten 2003 ISBN 4-00-005609-3 ). [10]  
  • Fitzgerald, JS , Larsen, PG, Mukherjee, P., Plat, N. e Verhoef, M., Projetos validados para sistemas orientados a objetos . Springer Verlag 2005. ISBN 1-85233-881-4 . O site de suporte [1] inclui exemplos e ferramentas de suporte gratuitas. [11] 
  • Jones, CB , Desenvolvimento sistemático de software usando VDM , Prentice Hall 1990. ISBN 0-13-880733-7 . Também disponível on-line e gratuitamente: http://www.csr.ncl.ac.uk/vdm/ssdvdm.pdf.zip 
  • Bjørner, D. e Jones, CB , Especificação Formal e Desenvolvimento de Software Prentice Hall International, 1982. ISBN 0-13-880733-7 
  • J. Dawes, O Guia de Referência VDM-SL , Pitman 1991. ISBN 0-273-03151-1 
  • Organização Internacional de 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 Padrão Internacional ISO/IEC 13817-1, dezembro de 1996.
  • Jones, CB , Desenvolvimento de software: uma abordagem rigorosa , Prentice Hall International, 1980. ISBN 0-13-821884-6 
  • Jones, CB e Shaw, RC (eds.), Estudos de caso em desenvolvimento sistemático de software , Prentice Hall International, 1990. ISBN 0-13-880733-7 
  • Bicarregui, JC, Fitzgerald, JS , Lindsay, PA, Moore, R. e Ritchie, B., Prova em VDM: um Guia do Praticante . Springer Verlag Abordagens formais para computação e tecnologia da informação (FACIT), 1994. ISBN 3-540-19813-X . 

Referências

  1. ^ Algumas ideias desse trabalho, incluindo um relatório técnico TR 25.139 sobre "Uma definição formal de um subconjunto PL/1", datado de 20 de dezembro de 1974, foi reimpresso em Jones 1984, p.107-155. Digno de nota é a lista de autores em ordem: H. Bekič, D. Bjørner, W. Henhapl, CB Jones, P. Lucas.
  2. ^ O duplo sinal de mais é adotado da linguagem de programação orientada a objetos C++ baseada em C.
  3. ^ Bjørner & Jones 1978, Introdução, p.ix
  4. ^ Observações introdutórias de Cliff B. Jones (editor) em Bekič 1984, p.vii
  5. ^ Bjørner & Jones 1978, Introdução, p.xi
  6. ^ Bjørner e Jones 1978, p.24.
  7. ^ Veja o artigo sobre persistência para seu uso na ciência da computação.
  8. ^ Clemmensen, Geert B. (janeiro de 1986). "Retargeting e rehosting do sistema compilador DDC Ada: Um estudo de caso - o Honeywell DPS 6" . ACM SIGAda Ada Letras . 6 (1): 22–28. doi :10.1145/382256.382794. S2CID16337448  .
  9. ^ Peter Gorm Larsen, "Dez anos de desenvolvimento histórico" Bootstrapping "VDMTools" Arquivado em 23 de janeiro de 2021 na Wayback Machine , In Journal of Universal Computer Science , volume 7(8), 2001
  10. ^ Modelagem de Sistemas: Ferramentas e Técnicas Práticas em Engenharia de Software
  11. ^ Projetos validados para sistemas orientados a objetos

links externos

Obtido em "https://en.wikipedia.org/w/index.php?title=Vienna_Development_Method&oldid=1217116085"