A Linguagem
de Especificação Z
Conteúdo
• Linguagens de especificação
–
–
•
Linguagem Z
–
–
–
–
•
Definição
Exemplos
Histórico
Vantagens de Uso
Operadores básicos
Exemplo prático
Referências
Linguagens de Especificação
Definição
• Linguagens de especificação usam notação
matemática para descrever o que um
programa deve fazer, sem descrever como
fazê-lo.
Linguagens de Especificação
Exemplos
Métodos de Especificação Formal
Linguagens Orientadas
ao Modelo
Linguagens Orientadas
ás Propriedades
{VDM, Z}
Linguagens Axiomáticas Linguagens Algébricas
{OBJ, Anna, Larch}
{Clear, Act One}
Linguagem Z
Histórico
• Proposta em 1977 por Jean-Raymond Abrial,
com a ajuda de Steve Schuman e Bertrand
Meyer.
• O nome Z (pronuncia-se “zed”) vem da teoria
de Zermelo-Fraenkel.
Linguagem Z
Vantagens de Uso
• Amplamente utilizada
• Possui um padrão internacional para sua
sintaxe, semântica e sistema de tipos.
• Fácil percepção de erros durante a
especificação formal e implementação.
Linguagem Z
Conceitos Básicos
•
•
•
•
•
Tipos
Esquemas
Conjuntos
Propriedades
Estado
Linguagem Z
Conceitos Básicos
• Notações:
– operação’: indica o resultado da operação sobre o
estado inicial, ou seja, o estado final.
– Δ Esquema: Indica mudança no estado.
– Ξ Esquema: Indica que o estado não muda.
– variável?: Indica que “variável” receberá entrada.
– variável!: Indica que “variável” gerará saída.
Linguagem Z
Exemplo Prático
Exemplo da agenda de aniversários:
Primeiro, especificamos que lidaremos com nomes e datas:
Então, definimos seu espaço de estados:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Agora podemos especificar a primeira operação, para
adicionar um nome:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Em seguida, a operação para encontrar o aniversário de uma
dada pessoa:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Agora, encontrar as pessoas que fazem aniversário em uma
certa data:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Por fim, especificamos qual é o estado do sistema quando ele
é iniciado pela primeira vez:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Agora, podemos considerar erros de entrada. Para isso,
precisamos de uma saída result!, que dirá se a entrada é
válida ou não. Então definimos um tipo INFO, que é um
conjunto com os seguintes valores:
Pode-se definir um esquema Sucesso, que especifica que o
resultado é ok, sem definir como o sistema muda:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Para o caso de o usuário entrar, em AddNome, um nome que
já faz parte de pessoa:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
E para o caso de o usuário entrar, em AcharNiver, um nome
que não faz parte de pessoa:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Porém, os três últimos esquemas não fazem sentido sozinhos.
Então, podemos relacioná-los com os outros esquemas:
onde o “R” antes do nome do esquema indica que esta é uma
versão “robusta” do esquema.
Seguem especificações dessas uniões em um só esquema:
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Linguagem Z
Exemplo Prático
Agenda de Aniversários
Linguagem Z
Exemplo Prático
Agenda de Aniversários
E, juntando todos os tipos e esquemas, a especificação está
completa.
Referências