Especificação Normal em Z
946 palavras
4 páginas
Especificação Z
Vinícius M.
Métodos formais
São técnicas embasados em formalismos matemáticos para especificação desenvolvimento e verificação dos sistemas de softwares e hardwares.
Uma linguagem de especificação formal usada para descrever e modelar sistemas computacionais
Especificação z
Z é um método formal.
Proposto por Jean-Raymond Abrial.
O modelo Z foi desenvolvido na Universidade de Oxford na década de 70.
Para servir como notação para a especificação formal de sistemas.
Utiliza uma variedade de estruturas matemáticas como conjuntos, relações e funções para descrever o comportamento do sistema através da construção de modelos, estados de um sistema e suas transições
A especificação em Z é formada por um número de esquemas que são decomposições da especificação em partes menores.
Z é baseada na notação matemática padrão usada no axioma da teoria dos conjuntos e lógica predicada de primeira ordem.
Todas as expressões são tipadas
Z contém um catálogo padronizado de funções matemáticas usadas com mais frequencia e predicados. Sintaxe de Z
Sintaxe de Z - Introdução
A especificação de um documento em notação Z consiste na declaração de tipos primitivos, iniciais, enumerados, potência, definições axiomáticas, predicados e esquemas .
Os tipos primitivos são conjuntos dos números inteiros, denotado por Z.
Os axiomas apresentam parte declarativa e predicativa.
Apresenta elementos da Lógica de Predicados de Primeira e segunda ordem.
Fortemente tipada: um tipo é um conjunto, e todas as variáveis, constantes expressões devem ter um nome.
Símbolos e Operações
Tabela de Prioridades:
Símbolos e Operações
Sobre Conjuntos:
Símbolos e Operações
Sobre Relações:
Símbolos e Operações
Sobre Funções:
Sobre Sequências:
Símbolos e Operações
Bags: conjunto