Notação Z - Especificação Formal

Prévia do material em texto

Métodos Formais
Notação Z - Revisão
Notação Z
✔ Utiliza lógica de predicado e teoria de 
conjuntos
✔ Permite dividir uma especificação em 
esquemas 
✔ Esquemas descrevem aspectos estáti-
cos e dinâmico
Notação Z
✔ Aspectos estáticos:
✔ Estado que um sistema ocupa
✔ As invariantes de relacionamento que são 
mantidas
Notação Z
✔ Aspectos dinâmicos:
✔ Operações possíveis
✔ O relacionamento entre entradas e saídas
✔ As mudanças de estado que acontecem
Notação Z
✔ Uma especificação Z consiste de pará-
grafos matemáticos:
✔ Matemática: conjuntos, sequências, 
coleções, funções e relações 
✔ Tipos básicos
✔ Variáveis
✔ Descrições axiomáticas
Notação Z
✔ Uma especificação Z consiste de pará-
grafos matemáticos:
✔ 'Constraints'
✔ Esquemas
✔ Abreviações
✔ Comentários ?
Notação Z - Tipos
✔ Tipos são interpretados como conjun-
tos
✔ Fortemente tipada 
✔ Todas as variáves, constantes e expressões 
devem ter um nome
✔ Tipos podem ser simples e compostos
Notação Z - Tipos
✔ Tipos simples podem ser:
✔ Primitivos e básicos
✔ Tipo primitivo: 
✔ Como todos os tipos são tratados como 
conjuntos, operações como = e ∈ são 
definidas para todos os tipos
ℤ
✔ Tipos básicos:
✔ São definidos para uma especificação
✔ [Nome_1,...,Nome_n]
[NOME,MATRICULA]
✔ Operações de conjuntos
[NOME]
Notação Z - Tipos
∀ x ,y :NOME •x≠y ⇒ ...
...
x ∈ NOME ⇒ ... 
Notação Z - Tipos
✔ Tipos compostos
✔ Conjuntos
✔ Produtos cartesianos
✔ Esquemas
✔ Variáveis, predicados, expressões
✔ Conjuntos
✔ Enumeração
status = {pronto, executando}
✔ Compressão
pares = {x : | x < 1000 ∧ x mod 2 = 0}
Notação Z - Tipos
ℕ
Notação Z - Tipos
✔ Abreviações
✔ Pode ser útil definir um novo nome no 
modelo para representar expressões 
complexas
✔ Exemplo
Título X Autor X Ano
Livro == Título X Autor X Ano
Notação Z - Tipos
✔ Tuplas e produto cartesiano
Livro : Titulo X Autor X Ano
Livro = (The Notation Z, J.M. Spivey, 2001)
Notação Z - Variáveis
✔ Variáveis
✔ As variáveis são associadas a um tipo 
através de declarações
✔ ident_1, ..., ident_n : expressão
p, q : 1..10
livro : Titulo X Autor X Ano
Notação Z - Variáveis
✔ Expressões axiomáticas
✔ Introduz variáveis e 'constraints' sobre 
seus valores
✔ Predicados podem não ser declarados
Declaração
Predicado;...;Predicado
Declaração
Predicado;...;Predicado
square : ℕℕ
∀n :ℕ•squaren=n∗n
Notação Z - Predicados
✔ Predicados
✔ Expressões booleanas
✔ Podem ser definidos isoladamente
✔ Sobre variáveis pré-definidas
✔ Exemplo:
 n_client < 5
Notação Z - Esquemas
✔ Esquemas
Declarações
Predicado;...;PredicadoPredicado;...;Predicado
Nome Esquema
NomeEsquema =^⇔
nome : seq Char
∀n:nome,m:senha • n ≠m
Usuario
senha : seq Char ⇔ Usuario =^
[ nome : seq Char; senha : seq Char |
∀n:nome,m:senha • nome ≠senha ]
[D1,...,Dn | P1,...,Pm]
Notação Z
✔ Tipos
✔ Simples e compostos
✔ Abreviações
✔ Produtos Cartesianos
✔ Expressões
✔ Predicados
✔ Variáveis
✔ Esquemas
Notação Z - Predicados
✔ Formas de montar predicados em Z
= ∀
∈ ∃
¬ ∃1
∧ 
∨ 
⇒
⇔
Notação Z - Operações
✔ Operações sobre tipos primitivos
ℤ ℕ
+ < 
- >
* ≤
div ≥
mod ..
ℕ1 succ
Notação Z - Operações
✔ Operações sobre conjuntos
∈ - pertence
∪ - união
∩ - intersecção
\ - diferença
# - cardinalidade
⊆ - subconjunto
⊂ - subconjunto próprio
Notação Z - Operações
✔ Operações sobre conjuntos
= - igualdade
U - união generalizada
P - powerset
Notação Z - Operações
✔ Relações e funções
✔ Relações binárias modelam objetos 
que relacionam membros de dois con-
juntos
A ↔ B = P(A x B)
r : A ↔ B
Notação Z - Operações
✔ Funções
total
parcial
total injetora
parcial injetora
total sobrejetora
parcial sobrejetora
parcial bijetora
total bijetora
Notação Z - Operações
✔ Operadores em relações e funções
↔ relação binária
→ maplet
dom domínio
ran contra-domínio
 9 composição relacional 
q:X↔Y,r:Y↔Z => X↔Z
º            volta da composição relacional
°
Notação Z - Operações
✔ Operadores em relações e funções
◁ restrição de domínio
Conj ◁ Relação
▷ restrição de contra-domínio
◁ subtração de domínio
▷ subtração de contra-domínio
~ inverso relação
_ ( _ ) imagem relacional
Relação ( Conj ) => A<-->B X PA --> PB
Notação Z - Operações
✔ Sequência
✔ Tipos são definidos a partir dos símbolos 〈 
e 〉
S1 = 〈a, b, c, d〉
✔ Variáveis são especificadas:
✔ Sequência vazia - palavra chave seq
✔ Sequência não vazia - palavra chave seq₁
✔ Sequência com elementos duplicados - palavra 
iseq
Notação Z - Operações
✔ Operações sobre sequências
# – tamanho ⌒ – concatenação
rev – reverso da sequência
head – primeiro elemento
last – último elemento
tail – sequência sem o primeiro elemento
front – sequência sem o último elemento
Notação Z - Operações
✔ Operações sobre sequência ⌒/ – concatenação distribuída – sequência 
de sequência - ⌒/q
prefix – prefixo
suffix – sufixo
in – segmento
⌉ – subsequência = índice + sequência
⌈ – subsequência = sequência + elementos
Notação Z - Operações
✔ Coleções (Bags)
✔ Conjunto contendo a quantidade de cada 
elementos armazenado
✔ Definido a partir de uma função parcial 
nos naturais
BagX == X → ℕ1
TipoFicha == {vermelho, amarelo, azul}
BagFicha == {vermelho → 3, amarelo → 5}
✔ São especificados através da palavra 
reservada bag
Notação Z - Operações
✔ Operações em 'bags'
count ou # – quantidade de um elemento no 
bag
⊗ – elemento que aparece 'n' vezes em um 
bag
 – pertence
U –união
U – diferença
 – está contido
+
-
Notação Z - Exemplos
✔ Conta de usuário
✔ Um usuário possui nome e senha
✔ O nome é diferente da senha
✔ A senha não deve ter mais que 8 dígitos
Caracter = {a, b, c, d, ..., z}
nome : seq1 Caracter
nome ≠ senha
#senha < 8
Login
senha : seq1 Caracter
Notação Z - Exemplos
✔ Livro de Aniversário
✔ De uma lista de pessoas conhecidas, dese-
jo representar uma agenda que armazene 
datas de aniversário
✔ A agenda deve armazenar nomes e datas 
de aniversário 
[NOME, DATA]
lNomes : P NOME
lNomes = dom aniversarios
Agenda
aniversarios : NOME →DATA
 
Notação Z - Exemplos
✔ Cliente X Servidor
✔ Não podem existir 2 servidores com mes-
mo id
✔ Um servidor pode atender até no máximo 
5 requisições
limite == ℕ
limite < 5
Servidor
req: limite
id: ℕ lServ : P Servidor
SisServ
∀ s1, s2 ∈ lServ •s1.id = s2.id ⇔ s1 = s2
Notação Z - Exemplos
✔ Turmas X Alunos
✔ Uma turma é formada por um conjunto de 
disciplinas
✔ Cada disciplina pode ter no máximo 30 
alunos
[DISCIPLINA]
lTurma : bag DISCIPLINA
Turma
∀n : ℕ • (n > 30 ∧ n ⊗ lTurma = ∅) 
Notação Z - Decoração
✔ Z é uma linguagem que estrutura um 
conjunto de teorias matemáticas
✔ Convenções são utilizadas para permi-
tir o uso desta teoria matemática es-
truturada na descrição de programas
✔ O uso destas convenções permite-nos 
descrever espaço de estados e oper-
ações
Notação Z - Decoração
✔ Espaço de estados:
✔ Conjunto de estados iniciais
✔ Operações✔ Cada operação possui variáveis de entrada e 
saída
✔ As operações são especificadas pela relação en-
tre as variáveis de entrada e saída e um par de 
estados (o estado antes e depois da operação)
Notação Z - Decoração
✔ Em Z, um esquema especifica um es-
paço de estados sobre um tipo abstra-
do
valor, limite : ℕ
Contador
valor < limite
✔ O espaço de estados aqui é formado 
por todas as instâncias do contador 
que obedecem a invariante 0 ≤  valor < 
 limite do relacionamento entre os 
atributos valor e limite
Notação Z - Decoração
✔ Para uma especificação descrever sis-
temas é necessário um estado inicial
Contador
IniciaContador
valor = 0
limite = 100
Teorema: ∃Contador • IniciaContador
Notação Z - Decoração
✔ Uma operação especifica um estado 
anterior e posterior sobre um espaço 
de estados
✔ O símbolo ' identifica o estado final
Contador
Contador '
Incrementa
valor ' = valor + 1
limite ' = limite
✔ As invariantes de relacionamentos de-
vem ser mantidas antes e depois da 
operação
Notação Z - Decoração
✔ Uma operação pode conter valores de 
entrada e saída
✔ Valores de entrada são decorados no 
esquema que descreve a operação 
com o símbolo '?'
Contador
Contador '
incr? : ℕ
Add
valor ' = valor + incr?
limite' = limite
Notação Z - Decoração
✔ Valores de saída são decorados no es-
quema que descreve a operação com o 
símbolo '!'
Contador
Contador '
incr? : ℕ
retorno! : ℕ
AddComRetorno
valor ' = valor + incr?
limite' = limite
retorno! = valor '
Notação Z - Decoração
✔ O símbolo ∆  é usado para abreviar a 
escrita de operações em que há mu-
dança de estado
✔ É apenas uma convenção, não é uma 
operação
∆ Contador
Incrementa
valor ' = valor + 1
limite ' = limite
valor, limite : ℕ
valor ', limite ' : ℕ
Incrementa
valor < limite 
valor ' < limite '
valor ' = valor + 1
limite ' = limite
valor, limite : ℕ
Contador
valor < limite
≡
Notação Z - Decoração
✔ O símbolo Ξ  é usado para abreviar a 
escrita de operações em que não há 
mudança de estado
✔ Como ∆ , é apenas uma convenção, não 
é uma operação
∆ Contador
Incrementa
valor ' = valor + 1
limite ' = limite
valor, limite : ℕ
Contador
valor < limite
Ξ Incrementa
retorno! : ℕ
RetornaAposIncrementa
retorno! = valor '
valor, limite : ℕ
valor ', limite ': ℕ
retorno! : ℕ
RetornaAposIncrementa
valor < limite
valor ' < limite '
valor ' = valor + 1
limite ' = limite
retorno! = valor '
≡
Notação Z - Exemplo
✔ Exemplo do livro de aniversário
✔ Uma agenda para armazenar nomes e 
datas de aniversário
[NOME, DATA]
lNome : P NOME
lNome = dom aniversario
Livro
aniverisario : lNomes →DATA 
Notação Z - Exemplo
✔ Adicionar um novo nome no livro
∆ Livro
nome? : NOME
data? : DATA
nome? ∉ lNome
aniversario ' = aniversario ∪ {nome? → data?} 
AdicionaNoLivro
 
Notação Z - Exemplo
✔ Encontrar uma data de aniversário
Ξ Livro
nome? : NAME
data! : DATA
nome? ∈lNome
data! = aniversario(nome?)
EncontrarAniversario
 
Notação Z - Exemplo
✔ Lembrete
Ξ Livro
dia? : DATA
aniversariantes! : P NOME
aniversariantes! = {a : lNome | aniversario(a) = dia?} 
Lembrete
 
Notação Z - Exemplo
✔ Estado inicial
Livro
lNome = ∅ 
Inicializacao
 
Notação Z - Exemplo
✔ A especificação está correta, mas não 
considera entrada de dados não es-
perados
✔ Adição de nomes que já existem
✔ Busca de nomes que não existem
✔ O sistema deve parar ? Deve contin-
uar operando e desconsiderar entrada 
de dados não esperadas ?
Notação Z - Exemplo
✔ Especificação adicional
✔ Identificação de possíveis 
erros/exceções
✔ Cada operação vai possuir uma saída 
resultado!
✔ Operações com sucesso retornam ok
✔ Os outros retornos são 
entrada_existente ou 
entrada_nao_existente
RETORNO = {ok, 
entrada_existente,entrada_nao_existente}
Notação Z - Exemplo
✔ Retorno de sucesso para a opreação 
AdicionaNoLivro
✔ O retorno é ok
∆ Livro
nome? : NAME
data? : DATA
nome? ∉ lNome
aniversario ' = aniversario ∪ {nome? → data?} 
AdicionaNoLivro
 
resultado! : RETORNO
resultado! = ok
Sucesso
 
AdicionaNoLivro ∧ Sucesso 
Notação Z - Exemplo
✔ Para completar a operação Adicio-
naNoLivro falta considerar o caso de 
que uma entrada existir 
Ξ Livro
nome? : NOME
resultado! : RETORNO
nome? ∈lNome
resultado! = entrada_existente
EntradaExistente
 
Notação Z - Exemplo
✔ Um esquema AdicionarNoLivro mais 
robusto NovoAdicionarNoLivro = 
(AdicionaNoLivro ∧ Sucesso) ∨
EntradaExistente
 ^
∆ Livro
nome? : NAME
data? : DATA
nome? ∉ lNome
aniversario ' = aniversario ∪ 
{nome? → data?} 
AdicionaNoLivro
 
resultado! : RETORNO
resultado! = ok
Sucesso
 
Ξ Livro
nome? : NOME
resultado! : RETORNO
nome? ∈ lNome
resultado! = entrada_existente
EntradaExistente
 
∆ Livro
nome? : NOME
data? : DATA
resultado! : RETORNO
(nome? ∉lNome ∧
aniversario ' = aniversario ∪ 
{nome? → data?} ∧ resultado! = ok) ∨ 
(nome? ∈lNome ∧
aniversario ' = aniversario ∧ 
resultado! = entrada_existente)
NovoAdicionarNoLivro
 
≡
Notação Z - Exemplo
✔ No caso da operação Encon-
trarAniversario o nome pode não exis-
tir
Ξ Livro
nome? : NOME
resultado! : RETORNO
nome? ∉lNome
resultado! = entrada_nao_existente
EntradaNaoExistente
 
NovoEncontrarAniversario = 
(EncontrarAniversario ∧ Sucesso) ∨
EntradaNaoExistente
 ^
Ξ Livro
nome? : NAME
data! : DATA
nome? ∈ lNome
data! = aniversario(nome?)
EncontrarAniversario
 
Notação Z - Exemplo
✔ No caso da operação Lembrete não há 
erro a ser registrado
✔ Se não existe aniversariante na data pas-
sada, o retorno é um conjunto vazio
Ξ Livro
dia? : DATA
aniversariantes! : P NOME
aniversariantes! = 
{a : lNome | aniversario(a) = dia?} 
Lembrete
 
resultado! : RETORNO
Sucesso
 resultado! = ok
NovoLembrete = Lembrete ∧ Sucesso ^