Notação Z

Prévia do material em texto

Métodos Formais
 Introdução à notação Z 
Prof. Álvaro Sobrinho 
alvaro.sobrinho@ufersa.edu.br
Especificação Formal
• Utilização de notações matemáticas 
– Descrever propriedades de maneira precisa 
– O que um sistema de informação deve conter? 
• Não são descritos detalhes de como comportamentos de 
sistemas são implementados 
• O ato de “esconder” detalhes de implementação é 
denominado de abstração 
– Não são necessários detalhes de como o programa deve ser codificado 
– O que é realizado no sistema, e não como é realizado!
 2
Especificação Formal
• Serve como ponto de referência 
– Estudar as necessidades de clientes 
– Implementar programas nos quais necessidades são satisfeitas 
– Testar programas 
– Documentar programas 
• Pode ser conduzida e finalizada nas fases iniciais do processo 
de desenvolvimento de software 
• Mesmo que modanças constantes possam ocorrer na 
especificação, pode servir como um ponto comum de 
partida 
– Tipos específicos de sistemas estão sujeitos a mudanças constantes
 3
Especificação Formal
• Tipos de dados matemáticos podem ser usados para modelar 
dados em sistemas 
– Raciociar efetivamente sobre o comportamento de um sistema 
• Lógica de predicados é usada para descrever abstratamente 
o efeito de cada operação do sistema 
• Uma especificação é decomposta em esquemas 
– Pequenos pedaços ligados com um comentário para explicar 
informalmente a significância da formalização 
– Usados para descrever aspectos estáticos e dinâmicos
 4
Conceitos Fundamentais: Z
• Um tipo é uma expressão de um tipo restrito 
– Conjunto 
– Composição de tipos 
• O valor de um tipo é denominado “carrier” 
• Cada variável possui um tipo 
• Por exemplo: 
– (0,1) = {1,2,3}
 5
Conceitos Fundamentais: Z
• Um tipo é uma expressão de um tipo restrito 
– Conjunto 
– Composição de tipos 
• O valor de um tipo é denominado “carrier” 
• Cada variável possui um tipo 
• Por exemplo: 
– (0,1) = {1,2,3}
 6
Não faz sentido!
Conceitos Fundamentais: Z
• Qualquer conjunto de objetos membros do mesmo tipo t é 
um objeto no tipo de conjunto ℙ t 
• Um conjunto pode ser definido por meio de seus elementos 
– Por exemplo: {1,2,4,8,16} 
– Possui o tipo ℙ ℤ (conjunto de inteiros – cinco primeiras potências de 
2) 
• É possível definir por meio de propriedades 
– Por exemplo: {p : PESSOA | idade(p) >= 16} 
– Possui tipo ℙ PESSOA (membros são exatamente tipos básicos de 
PESSOA com idade maior que 16)
 7
Tipos em Z
• Considere um sistema para gerenciar uma locadora de filmes 
• Em uma especificação, os seguintes conjuntos podem surgir: 
– Acervo: filmes de que dispõe a locadora 
– Locadas: filmes que estão locados a cliente no momento 
– Disponíveis: filmes que estão disponíveis para locação 
– Títulos: títulos de filmes de que a loja dispõe 
– Clientes: pessoas que estão cadastradas como clientes da loja 
– Empregados: funcionários que trabalham na loja 
• Portanto, Acervo, Locadas e Disponíveis são conjuntos de 
filmes 
– Podemos escrever expressões, tais como: 
– Acervo \ Locadas 
– Disponíveis U Locadas
 8
Tipos em Z
• Podemos formar também predicados: 
– Disponíveis = Acervo \ Locadas 
– Empregados ⊆ Clientes 
• Note que estes são objetos da mesma natureza 
– Mesmo tipo 
• Em Z, a seguinte expressão não faz sentido: 
– Disponíveis U Clientes 
• O tipo de um objeto determina um conjunto de dados 
– Ou valores que o objeto pode assumir
 9
Tipos em Z
• Todo objeto mencionado deve ser primeiramente declarado 
– Um tipo é associado ao objeto 
– Não é possível alterar o tipo de um objeto ao longo da especificação 
• Toda especificação contará com tipos iniciais 
– Estrutura interna não é detalhada 
• Por exemplo, é possível definir os seguintes tipos: 
– [Codigos] 
– [Pessoas] 
– [Filmes] 
• Outra possibilidade: [Codigos, Pessoas, Filmes]
 10
Tipos em Z
• Podemos então declarar variáveis 
– Lista de nomes, separados por vírgula, finalizada por dois pontos 
– Por exemplo: u,v : Codigos 
– Objetos tipados simples 
• A variável pode assumir um valor genérico dentro um 
conjunto de valores possíveis especificados por seu tipo 
• Pode-se então definir expressões mais complexas (ou termos) 
• Por exemplo: 
– x : T 
– ꓯy : T ⦁ (x ≠ y)
 11
Tipos em Z
• Podemos então declarar variáveis 
– Lista de nomes, separados por vírgula, finalizada por dois pontos 
– Por exemplo: u,v : Codigos 
– Objetos tipados simples 
• A variável pode assumir um valor genérico dentro um 
conjunto de valores possíveis especificados por seu tipo 
• Pode-se então definir expressões mais complexas (ou termos) 
• Por exemplo: 
– x : T 
– ꓯy : T ⦁ (x ≠ y)
 12
Predicado falso!
Tipos em Z
• É possível também definir tipos enumerados 
• Por exemplo, em um sistema de chaveamento: 
– LigDeslig ::= ligada | desligada 
• Em um baralho: 
– Naipe ::= ouros | copas | paus | espadas 
• Tipos primitivos podem ser usados 
– Por exemplo, o tipo que formado pelo conjunto dos números inteiros 
ℤ 
– Ou seja: x,y : ℤ
 13
Tipos em Z
• Muitas vezes, é conveniente atribuir um nome ao conjunto 
definido 
– Por exemplo? PeqInt == {1,2,3} 
• A declaração ParesPos == {x: ℤ | (x > 0) ᴧ (ⱻk : ℤ ⦁ x = 2 * k)} 
– Conjunto de todos os números pares positivos 
• É possível também definir relações de pertinência 
– Por exemplo: 
• p : Pessoas 
• p ϵ {jose, maria, rui} 
• Se C denota um conjunto finito de tipo ℙ T, então a expressão 
– #C denota o número de elementos no conjunto (cardinalidade)
 14
Tipos em Z
• Pode ser interessante também definir todos os subconjuntos 
finitos de um conjunto dado 
• Se C é um conjunto de objetos de tipo T, então a expressão FC 
– Denota o conjunto formado por todos os subconjuntos finitos do 
conjunto representado por C 
• Por exemplo Fℕ denota o conjunto {ø, {0}. {0,1},{2}, {0,2}, 
{1,2}, ...} 
– Todos os subconjuntos finitos de números naturais 
• Uma declaração como finito : ℙ ℤ nos permite escrever o predicado 
– finito ϵ Fℤ
 15
Tipos em Z
• Como definir subintervalos? 
– Por exemplo, de -1 a 5 
– {n : ℤ | -1 ≤ n ≤ 5}, onde é uma abreviação para (n ≥ -1) ᴧ (n ≤ 5) 
– Em Z, poderia ser designado simplesmente como -1..5 
• Por outro lado, se x e y são dois objetos membros dos tipos t 
e u, o par ordenado (x,y) é um objeto 
– Tipo produto cartesiano t X u 
• Se x, y, e z são três objetos membros dos tipos, t, u e v, a 
tripla ordenada (x, y, z) é um objeto 
– Tipo produto cartesiano t X u X v 
– A tripla (x, y, z) é diferente de (x,(y,z))
 16
Tipos em Z
• Considere como exemplo um sistema que envolve o controle 
de filas que se formam em um banco 
• Cada fila é determinada pelo seu comprimento e pelo caixa 
que a serve 
– Os caixas são introduzidos pela declaração [Caixas] 
• Portanto, Fila == Caixas x ℤ 
• Podemos escrever filas : ℙ Fila 
– Conjunto de pares na forma (c, n) 
– c é um objeto do tipo Caixas e n é um objeto do tipo ℤ
 17
Tipos em Z
• Um caixa não pode ter associado a si filas de comprimentos 
distintos: 
– ꓯ n1, n2 : ℤ; c : Caixas ⦁ ((c, n1) ϵ filas ᴧ (c, n2) ϵ filas -> n1 = n2) 
• Cada Caixa tem pelo menos uma fila associada a si: 
– ꓯc : Caixas ⦁ (ⱻn : ℤ ⦁(c,n) ϵ filas)
 18
Tipos em Z
• Se p e q são identificadores distintos, e x e y objetos de tipos 
t e u, existe uma ligação (binding): 
– z = ⟨ p x, q y⟩ 
– Ou seja, componentes z.p = x e z.q = y 
• A ligação descrita anteriormente é um objeto com o 
esquema: 
– ⦉ p:t , q:u ⦊ 
 19
Exercício
• Estamos construindo parte de uma especificação para um 
sistema bancário 
• Os conjuntos Contas e Clientes devem ser introduzidos como 
tipos inciais 
• As seguintesvariáveis devem ser declaradas: 
– ccorr: conjunto de contas-corrente 
– cpoup: conjunto de contas de poupança 
– cnegat: conjunto de contas com saldo negativo 
• Crie um parágrafo em Z que defina o conjunto inicial e as 
variáveis indicadas
 20
Exercício
• Posteriormente, escriva novos parágrafos para refletir as 
seguintes condições: 
– Somente contas correntes podem ficar negativas 
– Uma conta não pode ser de ambas as naturezas: poupança e conta 
corrente 
• Considere em seguida novas variáveis: 
– titulares: conjunto de pares em que o primeiro componente é um 
cliente e o segundo é uma de suas contas 
– saldos: um conjunto de pares em que o primeiro componente indica 
uma conta e o segundo indica seu saldo 
• Considere a seguinte restrição para titulares: 
– Ninguém pode ser titular de mais de uma conta corrente
 21
Exercício
• Considere a seguinte restrição para saldo: 
– Não é possível ter saldo de alguma conta corrente negativo se o 
mesmo cliente não tiver também uma conta de poupança com saldo 
suficiente para cobrir o valor negativo 
• Restrição desafio: 
– A soma dos saldos de todas as contas de poupança de um mesmo 
cliente deve ser suficiente para cobrir a totalidade de seus saldos 
negativos em contas corrente
 22
Definição Axiomática
• Declaração de variáveis e aplicação de restrições 
• De maneira geral: 
• Declarações estão relacionadas com variáveis 
• Predicados estão relacionados com restrições sobre variáveis
 23
Declarações
Predicados
Definição Axiomática
• Considere novamente o exemplo da locadora: 
• Considerando uma definição axiomática:
 24
[Codigos, Carros, Titulos, Pessoas, Mesgs] 
Mesgs ::= OK 
 | existe | naoexiste 
 | locado | disponível | ematraso 
 | pago | cliente | naocliente 
 
 
disp, loc, carro : ℙ Carros 
clientes, atraso : ℙ Pessoas 
titulo : ℙ Titulos 
maxloc, maxtitulo : ℤ 
maxloc ≥ 0 
maxtitulo ≥ 0 
disp ꓵ loc = Ø 
disp U loc = carro 
atraso ⊆ clientes 
Variáveis
• Pode-se usar variáveis: 
– Entrada 
– Saída 
– Estado 
• Toda variável de entrada deve ter seu nome terminando no 
caracter “?” 
• Toda variável de saída deve ser seu nome terminado no 
símbolo “!” 
• Por exemplo:
 25
dev? : Carros 
resp! : Mesgs 
...
Variáveis
• Pode-se usar variáveis: 
– Entrada 
– Saída 
– Estado 
• Toda variável de entrada deve ter seu nome terminando no 
caracter “?” 
• Toda variável de saída deve ser seu nome terminado no 
símbolo “!” 
• Por exemplo:
 26
dev? : Carros 
resp! : Mesgs 
...
Variável de entrada
Variáveis
• Pode-se usar variáveis: 
– Entrada 
– Saída 
– Estado 
• Toda variável de entrada deve ter seu nome terminando no 
caracter “?” 
• Toda variável de saída deve ser seu nome terminado no 
símbolo “!” 
• Por exemplo:
 27
dev? : Carros 
resp! : Mesgs 
...
Variável de saída
Variáveis
• Variáveis de estado não são definidas como entrada ou saída 
• Escrevemos novos valores assumidos por uma variável de 
estado escrevendo seu nome seguido do caractere ‘ 
• Por exemplo:
 28
disp, loc, carro : ℙ Carros 
disp’, loc’ : ℙ Carros 
max : ℕ 
dev? : Carros 
resp! : Mesgs
#carro ≤ max 
disp ꓵ loc = Ø 
disp U loc = carro 
dev? ϵ loc 
disp’ = disp U {dev?} 
loc’ = loc \ {dev?} 
resp! = OK 
Relações e Funções
• Considere X e Y como tipos previamente declarados 
• Uma relação rel cujo conjunto fonte contém objetos do tipo 
X e cujo conjunto alvo contém objetos do tipo Y 
– É um conjunto de pares de elementos (x,y) 
– x em X e y em Y 
– Portanto, rel é um element de ℙ(X × Y) 
• Pode-se escrever uma declaração para rel na forma: 
– | rel : ℙ(X × Y) 
• Neste caso, o tipo de rel é ℙ(X × Y) 
 29
Relações e Funções
• Podemos assumir que para todo par de conjuntos X e Y, a linguagem 
Z já contém uma declaração implícita na forma: 
– X ↔ Y == ℙ(X × Y) 
• Essa definição caracteriza o objeto X ↔ Y como o conjunto de todos 
os subconjuntos do produto X × Y 
• Pode-se então escrever: 
– | rel : X ↔ Y 
• Considerando o par de elementos (x,y) especificado pela relação rel: 
– (x,y) ϵ rel 
– Ou: x → y ϵ rel
 30
Relações e Funções
• Exemplo: 
• Na parte declarativa, a posição dos argumentos é marcada 
pelo símbolo “_” 
• É determinado que n > m vale sempre que existir um 
número positivo k tal que somado a m produza o valor de n
 31
_>_ : ℤ ↔ ℤ 
ꓯ n,m : ℤ ⦁ (n,m) ϵ > ⇔ (ⱻk : ℕ1 ⦁ m + k = n ) 
Relações e Funções
• Como outro exemplo, considere a relação infixa para 
mapear um par de elementos dos inteiros 
– No número correspondente à soma de seus elementos 
• Ou seja: 
• Se rel : ℙ(X × Y) é uma declaração para a relação rel, 
designamos por dom rel 
– Seu conjunto domínio 
– Por ran rel, seu conjunto imagem
 32
_somapar_ : (ℤ × ℤ) ↔ ℤ 
ꓯ x,y,z : ℤ ⦁ ((x,y) somapar z ⇔ z = x + y ) 
Relações e Funções
• Portanto: 
– dom rel = {x : X | ⱻy: Y ⦁ x → y ϵ rel} 
– ran rel = {y : Y | ⱻ x : X ⦁ x → y ϵ rel} 
• Quando rel for do tipo ℙ(X × Y) e tivermos em c um objeto 
do tipo ℙ X, poderíamos considerar o conjunto imagem de c 
sob a relação rel 
– rel (| c |) = {x : X; y : Y | (x ϵ c) ᴧ (x → y ϵ rel) ⦁ y} 
• O predicado seleciona todos os elementos y que são a 
imagem de algum elemento x que está em c
 33
Relações e Funções
• Se tivermos as declarações: 
• Então, para formar as relações obtidas por restrição do 
conjunto fonte e restrição do conjunto alvo: 
– s < rel = {x : X; y : Y | (x ϵ s) ᴧ (x → y ϵ rel) ⦁ x → y} 
– rel > r = {x : X; y : Y | (y ϵ r) ᴧ (x → y ϵ rel) ⦁ x → y} 
• A operação de composição relacional é indicada pelo símbolo 
– Significa que se X, Y e W são tipos em Z, as declarações: 
– Nos permitem construir a expressão: rel1 rel2 
– Para designar um objeto do tipo X ↔ W 
– Que satisfaz: ꓯ x : X; w : W ⦁ (x → w ϵ rel1 rel2 ⇔ ⱻ y : Y ⦁ (x → y ϵ 
rel1) ᴧ y → w ϵ rel2))
 34
rel : X ↔ Y 
s : ℙ X 
r : ℙ Y
rel1 : X ↔ Y 
rel2 : Y ↔ W
Relações e Funções
• Relembre que funções são relações que obedecem a certas 
exigências adicionais 
• Em geral, podemos declarar uma função f por meio de um 
parágrafo: 
• Esta declaração é equivalente a: 
• O símbolo → indica uma função parcial
 35
 f : X ↔ Y 
ꓯ x : X; y, z: Y ⦁ ( x → y ϵ f) ᴧ (x → z ϵ f) ⇒ y = z) 
 f : X → Y 
Relações e Funções
• Por outro lado, considera a classe das funções totais 
• O símbolo → indica uma função total 
• Portanto: 
• Seria equivalente a:
 36
 f : X → Y 
 f : X → Y 
ꓯ x : X ⦁ (ⱻ y : Y ⦁ (x → y ϵ f)) 
Relações e Funções
• Pode-se também utilizar funções injetoras totais e parciais: 
– X → Y == {f : X → Y | ꓯx,y : X; z : Y ⦁ (x → z ϵ f) ᴧ (y → z ϵ f) ⇒ (x 
= y)} 
– X → Y == {f : X → Y | ꓯx,y : X; z : Y ⦁ (x → z ϵ f) ᴧ (y → z ϵ f) ⇒ (x 
= y)} 
• Considere também as funções sobrejetoras totais e parciais: 
– X >> Y == {f : X → Y | ran f = Y} 
– X >> Y == {f : X → Y | ran f = Y} 
• Além disso, considere a bijeção: 
– X >> Y == {f : X → Y | ran f = Y}
 37
Relações e Funções
• Suponha que T é um tipo fixo e predefinido 
• Especificar a função identidade em T: 
• O tipo de id é ℙ(T × T) 
• É possível parametrizar declarações 
– Maneira sistemática de obter novos objetos quando os parâmetros 
formais são substituídos por tipos reais 
 
 38
 id : T → T 
Id = {t : T ⦁ t → t}
Relações e Funções
• Portanto: 
• Outra forma para definição parametrizada: 
– id[X] == {t : X ⦁ t → t} 
• Forma simplificada para definição parametrizada: 
– id X == {t : X ⦁ t → t}
 39
 id : X → X 
Id = {t : X ⦁ t → t}
[X]
Relaçõese Funções
• Pode-se também utilizar mais de um parâmetro: 
• Define duas funções para extrair o primeiro e o segundo 
elemento de um par ordenado
 40
 prim_ : X × Y → X 
 sec_ : X × Y → Y
ꓯ x : X; y : Y ⦁ (prim(x,y) = x) ᴧ (sec(x,y) = y) 
[X, Y]
Relações e Funções
• Como exemplo de aplicação dos conceitos apresentados, 
considere a noção de sequências 
• Portanto, impor ordem em elementos 
• Por exemplo, a sequência s = <a, b, a, c, b, d> pode ser 
entendida como uma função fs 
– Mapeia elementos do conjunto fonte {1,2,3,4,5,6} em elementos do 
conjunto alvo {a, b, c, d} 
• Essa sequência seria uma função parcial de ℕ em T 
(assumindo que são do tipo T) 
 41
Relações e Funções
• Devemos exigir que o domínio da função seja dado pelo 
intervalo de números naturais 
– Consecutivos de 1 a n, onde n é o comprimento da sequência 
• Portanto: SeqT == {f : ℕ → T | dom f = 1..#f} 
– Função total e finita de ℕ em T 
• Podemos declarar sequências: 
– | s, t : SeqT 
• Pode-se também declarar enumerando elementos: 
– simp == {1 → a, 2 → b, 3 → a, 4 → c, 5 → b, 6 → d}
 42
Relações e Funções
• Em Z, existe uma notação própria para designar sequências 
• Se T é um tipo já declarado, então: 
– seq T 
• Poderíamos declarar variáveis como sequências de 
elementos de tipo T: 
– | s, t : seq T
 43
Relações e Funções
• Como concatenar sequências? 
• Dada pela união dos pares que formam as sequências s e t 
– Os que formam t sofrem um deslocamento de #s unidades para a direita 
• Por exemplo, para s = {1 → b, 2 → a} e t = {1 → a, 2 → b, 3 → 
a}: 
– s t = {1 → b, 2 → a} U {1+2 → a, 2+2 → b, 3+2 → a} = {1 → b, 2 → 
a, 3 → a, 4 → b, 5 → a}
 44
 _ _ : (seq T × seq T) → (seq T) 
ꓯ s, t : seq T ⦁ s t = s U {n : ℕ; x : T | n → x ϵ t ⦁ (n + #s) → x} 
[T]
Relações e Funções
• As seguintes operações também podem ser definidas (cabeça 
e calda da sequência):
 45
head : seq1 T → T 
tail : seq1 T → seq T
ꓯ s : seq1 T ⦁ head s = s 1 
 ꓯ s : seq1 T ⦁ tail s = {n : N1; z : T | (n+1 → z) ϵ s ⦁ n → z}
[T]
Relações e Funções
• As seguintes operações também podem ser definidas 
(primeiros e último da sequência):
 46
last : seq1 T → T 
front : seq1 T → seq T
ꓯ s : seq1 T ⦁ last s = s #s 
 ꓯ s : seq1 T ⦁ front s = {n : N; z : T | (n → z ϵ s) ᴧ (n < #s) ⦁ n → z}
[T]
Exemplo
• Considere um sistema para controlar operações de uma 
locadora de carros 
• Requisitos do sistema incluem: 
1. Controle da operação de locação e devolução de carros 
2. Meios para a inclusão e exclusão de clientes no cadastro da loja 
3. Controlar a entrada de novos carros no acervo da loja; controlar também a 
baixa do acervo para carros extraviados ou danificados 
4. Manter um controle do acervo de carros oferecidos para locação; o mesmo 
modelo pode estar disponível em várias unidades 
5. Emitir relatórios diversos 
1. Quais carros estão locados 
2. Qual o acervo de modelos 
3. Quantos carros do modelo a loja dispõe 
4. Quais modelos certo cliente tem em seu poder 
5. Quais os clientes cadastrados 
6. Qual cliente locou um determinado carro
 47
Conceitos Fundamentais: Z
• Por outro lado, uma assinatura é uma coleção de variáveis 
– Cada uma com um tipo 
• Assinaturas são criadas por meio de declarações 
– Oferecem um vocabulário para a definição de declarações 
matemáticas (expressos por predicados) 
• Por exemplo, a declaração x, y : ℤ é utilizada para criar uma 
assinatura com duas variáveis x e y do tipo ℤ 
– O predicado x < y pode ser usado para expressar a propriedade que o 
valor de x é menor que o valor de y 
– Dois predicados podem ser usados para expressar a mesmo 
propriedade: y > x e x < y
 48
Conceitos Fundamentais: Z
• Cada assinatura é associada naturalmente com um tipo de 
esquema 
– Por exemplo: a assinatura x, y : ℤ está associada com o tipo de 
esquema ⦉ x, y : ℤ ⦊ 
– Uma propriedade em uma assinatura é caracterizada pelo conjunto 
de ligações para as quais são verdadeiras. Por exemplo: x < y é 
verdadeira para as ligações ⟨ x 3 , y 5 ⟩ 
• Um predicado é usado para expressar uma propriedade 
– Por expressar propriedade diz-se que um predicado é verdadeiro 
sobre uma ligação, se a propriedade expressada é verdadeira sobre 
essa ligação 
– Diz-se que a ligação satisfaz a propriedade, se a propriedade é 
verdadeira sobre essa ligação
 49
Conceitos Fundamentais: Z
• Um esquema é uma assinatura associada a uma propriedade 
sobre a assinatura 
• Por exemplo: 
• Neste caso, x e y são componentes de Ex
 50
Conceitos Fundamentais: Z
• Algumas vezes, a declaração pode contribuir com algo em 
uma propriedade: 
• O tipo de f é ℙ (ℤ x ℤ) 
 51
Conceitos Fundamentais: Z
• Uma equação E1 = E2 expressa a propriedade que os valores 
das expressões E1 e E2 são iguais 
• O predicado E1 ∈ E2 expressa a propriedade que o valor de 
E1 é um membro de R2 
• Entretanto, predicados podem ser combinados para a 
construção de outras propriedades 
– Por exemplo: o predicado P1 ∧ P2 expressa a conjunção de 
propriedades expressas usando os predicados P1 e P2 
• Outros conectivos do cálculo proposicional (∨, ⇒, ¬, ⇔) 
podem também ser usados para a combinação de predicados
 52
Conceitos Fundamentais: Z
• Se x é um número natural, o predicado ∀z : ℕ ⦁ x ≤ z expressa 
a propriedade que o valor de x é menor ou igual todos os 
naturais 
– Ou seja, zero 
• O quantificador existencial ∃ também pode ser utilizado 
• Se S é um esquema, S’ é o mesmo S, exceto que os nomes dos 
componentes possuem agora ‘ 
• Por exemplo, se Ex é um esquema, então ligações para Ex 
possuem o tipo ⦉ x, y : ℤ⦊, e ligações para Ex’ possuem o tipo 
⦉ x’, y’ : ℤ⦊
 53
Conceitos Fundamentais: Z
• É possível combinar esquemas por meio de conectivos lógicos 
• Os operadores \ e ↾ oferecem maneiras de remover 
componentes de esquemas 
• Se S é um esquema, e x1, ... , xn são componentes de S: 
– S \ (x1, ... ,xn) 
• Componentes estão contidos em S, exceto por x1, ... , xn 
– Possuem os mesmo tipos como S
 54
Conceitos Fundamentais: Z
• Se S e T são esquemas com tipos de assinaturas compatíveis, S 
↾ T é também um esquema 
– Possui assinatura de T, e sua propriedade é satisfeita por exatamente 
ligações que são restrições de uma ligação satisfazendo a propriedade 
de S ∧ T 
– O mesmo que (S ∧ T) \ (x1, ... ,xn), onde x1, ... , xn são todos os 
componentes de S não compartilhados por T 
• Se D é uma declaração, P é um predicado, e S é um esquema: 
– ∀ D | P ⦁ S 
– É também um esquema 
– O esquema S deve possuir como componentes todas as variáveis 
introduzidas por D, e devem possuir o mesmo tipo 
– A assinatura contém todos os elementos de S, exceto os introduzidos 
por D
 55
Conceitos Fundamentais: Z
• Por exemplo, considere o seguinte esquema: 
• A expressão ∀ z : ℤ | z > 5 ⦁ Ex 
• Pode ser escrito da seguinte maneira:
 56
Conceitos Fundamentais: Z
• Especificações podem conter variáveis globais 
– Componentes de esquemas 
• É possível também definir variáveis locais por meio, por 
exemplo, do quantificador ∀ 
– ∀ y : ℕ ⦁ x > y 
• Para cada variável introduzida por uma declaração, existe 
uma região da especificação 
– Escopo da declaração 
• Diz-se que a variável é local para a região da especificação
 57
Conceitos Fundamentais: Z
• Variáveis podem também ser globais para esquemas 
– Definição axiomática 
• Por exemplo: 
• Portanto, um esquema pode ser definido:
 58
Conceitos Fundamentais: Z
• Além disso, é possível definir esquemas genéricos 
• Por exemplo, considere um esquema genérico para 
gerenciamento de recursos:
 59
Parâmetro Genérico
Conceitos Fundamentais: Z• Um espaço de estado de um gerenciador de recurso 
específico pode ser descrito como uma instância 
– Por exemplo: piscina de discos identificados por número de 0 a 7: 
DiscoPiscina Piscina[0..7]
 60
Exemplo
• Considere como exemplo um livro de aniversário 
– Sistema para registrar o aniversário de pessoas 
– Lembretes são emitidos 
– Deve-se lidar com nomes e datas 
– Não importa a forma de nomes e datas 
• Os seguintes conjuntos para todos os nomes e datas são 
podem ser definidos como tipos básicos da especificação: 
– [NOME, DATA] 
• Portanto, deve-se descrever o espaço de estados do sistema 
– Esquemas são usados
 61
Exemplo
 62
• Primeiro esquema para exemplo do livro de aniversário: 
J. M. Spivey. The Z Notation: A Reference Manual. Second Edition. University of Oxford. 1998 
Exemplo
 63
Conjunto das 
Partes
• Primeiro esquema para exemplo do livro de aniversário: 
Exemplo
 64
Função 
Parcial
• Primeiro esquema para exemplo do livro de aniversário: 
Exemplo
• Variáveis são declaradas no compartimento superior do 
esquema 
• Relacionamentos entre valores e variáveis são determinados 
no compartimento inferior 
– Relacionamentos que são verdadeiros para todos os estados e 
mantidos para todas as operações 
• No exemplo apresentado, valores da variável “conhecido” 
são derivados a partir do valor de “aniversario”
 65
Exemplo
 66
Conjunto de nomes 
com datas de 
aniversário conhecidos 
• Primeiro esquema para exemplo do livro de aniversário: 
Exemplo
 67
Função para associar 
nomes e datas de 
aniversário
• Primeiro esquema para exemplo do livro de aniversário: 
Exemplo
• Por exemplo, o seguinte estado pode ser atribuído ao 
sistema: 
– conhecido = {João, Pedro, Maria} 
– aniversario = {João ↦ 25-Março, Pedro ↦ 20-Dezembro, Maria ↦ 20 
Março} 
 
• Neste caso, a invariante é satisfeita porque “aniversario” 
contém uma data para exatamente os três nomes contidos 
em “conhecido”
 68
Exemplo
• Uma vez que o espaço de estados é definido, é possível 
definir operações do sistema:
 69
Exemplo
• Uma vez que o espaço de estados é definido, é possível 
definir operações do sistema:
 70
Alertar 
modificação de 
estado
Exemplo
• Uma vez que o espaço de estados é definido, é possível 
definir operações do sistema:
 71
Convenção para 
indicação de 
entrada
Exemplo
• Uma vez que o espaço de estados é definido, é possível 
definir operações do sistema:
 72
Observação de 
modificação de 
estado
Exemplo
• Uma vez que o espaço de estados é definido, é possível 
definir operações do sistema:
 73
Pré-condição para 
sucesso na 
operação
Exemplo
• Uma vez que o espaço de estados é definido, é possível 
definir operações do sistema:
 74
Função aniversario 
é estendida para 
mapear novo nome 
e data
Exemplo
• Uma vez que o espaço de estados é definido, é possível 
definir operações do sistema:
 75
Note que a pré-
condição deve ser 
satisfeita
Exemplo
• Portanto, isso implica que o novo nome será inserido no 
conjunto de nomes conhecidos: 
– conhecido‘ = conhecido ⋃ {nome?}
 76
Exemplo
• Outra possível operação é a consulta:
 77
Exemplo
• Outra possível operação é a consulta:
 78
Indica que o estado 
não é alterado
Exemplo
• Outra possível operação é a consulta:
 79
Indica saída de 
dados
Exemplo
• Outra possível operação é a consulta:
 80
Pré-condição
Exemplo
• Outra possível operação é a consulta:
 81
Valor da função 
aniversario no 
argumento nome?
Exemplo
• Pode ser interessante também uma operação para lembretes 
de aniversários em um dia específico:
 82
Exemplo
• Pode ser interessante também uma operação para lembretes 
de aniversários em um dia específico:
 83
Entrada
Exemplo
• Pode ser interessante também uma operação para lembretes 
de aniversários em um dia específico: 
• Portanto, pode não existir nenhuma, uma, ou mais de uma 
pessoa relacionada com um dia específico (cartões enviados 
ou não)
 84
Saída
Exemplo
• Pode ser interessante também uma operação para lembretes 
de aniversários em um dia específico: 
• Além disso, neste caso, não são definidas pré-condições
 85
Relembre: alteração de 
estado não é realizada 
Exemplo
• Ou seja: 
– m ∈ {n : conhecido | aniversario(n) = hoje?} 
 ⇔ m ∈ conhecido ∧ aniversario(m) = hoje? 
• Um nome “m” somente está em uma saída se é conhecido 
pelo sistema, e se seu aniversário for igual a entrada 
informada
 86
Exemplo
• O estado inicial do sistema pode ser definido da seguinte 
maneira: 
• Portanto, o conjunto “conhecido” e a função “aniversario” 
estão inicialmente vazios
 87
Exemplo
• Entretanto, existem alguns problemas críticos com 
especificação atual do sistema 
– Está indefinido o que ocorre quando algum nome já existente é 
inserido no conjunto “conhecido” 
– Está indefinido o que ocorre quando um usuário tentar encontrar o 
aniversário de um “desconhecido” 
• O que pode ocorrer? 
– O Sistema pode ignorer a entrada incorreta 
– Um estado indesejado pode ser alcançado (e.g., apresentar lixo de 
memória, ou um aniversário pode ser “esquecido”) 
– Pode paracer normal, mas futuramente alcançar um estado 
indesejado
 88
Exemplo
• Este tipo de problema compromete a especificação do sistema 
• Entretanto, não é necessário descartar a especificação 
existente 
– Uma nova especificação pode ser definida para descrever erros e 
respostas desejadas 
– Posteriormente, as especificações podem ser integradas 
• Para a nova especificação, uma nova saída denominada 
“resultado!” será adicionada para cada operação do sistema 
– O valor “ok” será definido quando uma operação for realizada com 
sucesso 
– Os valores “ja_conhecido” e “desconhecido” serão definidos quando 
erros forem detectados
 89
Exemplo
• Um conjunto denominado “RELATORIO” é definido como um 
tipo: 
– RELATORIO ::= ok | ja_conhecido | desconhecido 
• Primeiramente, um esquema denominado “Sucesso” pode ser 
definido:
 90
Exemplo
• O operador de conjunção ∧ pode ser usada para combinar a 
descrição anterior com a operação AdicionaAniversario: 
– AdicionaAniversario ∧ Sucesso 
• Além disso, para cada erro possível relacionado com a 
entrada, um esquema é definido 
– Em quais condições o erro ocorre? 
– Qual relatório deve ser produzido?
 91
Exemplo
• Esquema para especificação de relatório de erro 
“já_conhecido”:
 92
Estado não é 
alterado quando o 
erro ocorre
Exemplo
• As novas descrições podem ser combinadas para construir 
uma versão mais robusta da operação “AdicionaAniversario” 
• Portanto, um novo esquema denominado 
“RAdicionaAniversario” é criado a partir de três esquemas 
existentes 
• Especificações foram criadas separadamente e 
posteriormente combinadas (como exemplo)
 93
Exemplo
• Note que, desde o início, a operação “RAdicionaAniversario” 
poderia ser escrita como um único esquema:
 94
Exemplo
• Por outro lado, um esquema “Desconhecido” pode ser 
definido da seguinte maneira:
 95
Exemplo
• A operação “ConsultaAniversario” é combinada com os 
esquemas definidos: 
• A operação “Lembrete” é também combinada com o 
esquema “Sucesso”:
 96
Especificação Formal
• Até o momento, a notação Z foi usada para especificar 
módulos de software 
• Entretanto, existem técnicas para documentar o projeto de 
um programa (implementação da especificação) 
– Estruturas de dados concretas devem ser descritas (usadas para 
representar dados abstratosna especificação) 
– Derivar descrições de operações em termos de estruturas de dados 
concretas 
• Isso é chamado de processo de refinamento de dados
 97
Especificação Formal
• Refinamento de dados pode permitir que estruturas de 
controle se tornem explícitas 
– Refinamento de operações ou desenvolvimento de algoritmo 
• Em programas simples, é possível obter o programa final a 
partir da especificação em “um passo” 
– Refinamento direto 
• Em sistemas complexos, vários “passos” são necessários 
– Refinamento diferido 
– Ao invés de um programa, um primeiro passo resulta em uma nova 
especificação 
– Podem existir vários passos até o programa final
 98
Especificação Formal
• Retornando ao livro de aniversários ... 
– Estruturas de dados abstratas foram usadas 
• Considerando a implementação, é possível representar o 
livro de aniversários com duas arrays: 
– nomes : array [1..] of NOME; 
– datas : array [1..] of DATA; 
• Neste caso, arrays com limites infinitos foram definidos para 
maior simplicidade
 99
Especificação Formal
• As arrays podem ser modeladas matematicamente por meio 
de funções a partir de um conjunto de números inteiros 
positivos: 
– nomes : ℕ1 → NOME 
– datas : ℕ1 → DATA 
• O elemento nomes[i] do array é o valor nomes(i) da função 
• A atribuição nomes[i] := v é descrita pela seguinte 
especificação: 
– nomes‘ = nomes ⊕ {i ↦ v}
 100
Especificação Formal
• As arrays podem ser modeladas matematicamente por meio 
de funções a partir de um conjunto de números inteiros 
positivos: 
– nomes : ℕ1 → NOME 
– datas : ℕ1 → DATA 
• O elemento nomes[i] do array é o valor nomes(i) da função 
• A atribuição nomes[i] := v é descrita pela seguinte 
especificação: 
– nomes‘ = nomes ⊕ {i ↦ v}
 101
Tudo é considerado em 
nomes exceto {i ↦ v}
Especificação Formal
• Portanto, o espaço de estados do programa pode ser definido 
da seguinte maneira: 
• Ou seja: Não existem repetições entre os elementos 
– nomes(1),...,nomes(tamanho)
 102
Especificação Formal
• Cada nome é conectado com a data em seu elemento 
correspondente na array de datas 
• Isso pode ser documentado com o seguinte esquema: 
– Relacionamento entre espaço de estados abstrato e concreto
 103
Especificação Formal
• Portanto: 
– O conjunto conhecido consiste somente dos nomes que ocorrem entre 
nomes(1),…,nomes(tamanho) 
– O aniversário para nomes(i) é o elemento correspondente em datas(i) 
da array de datas 
• Vários estados concretos podem representar o mesmo estado 
abstrato 
– Ex.: a ordem dos nomes e datas na array não importa 
• Entretanto, um estado concreto somente representa um 
estado abstrato
 104
Exemplo
• Implementação da operação de adicionar:
 105
Exemplo
• Ou seja: 
– Quando AdicionaAniversario é válida em um estado abstrato, a 
implementação AdicionaAniversario’ é válida no estado concreto 
correspondente 
– O estado final obtido a partir de AdicionaAniversario’ representa um 
estado abstrato que pode ser produzido por AdicionaAniversario 
• Portanto: 
– AdicionaAniversario é válida se a pré-condição nome? ∈ conhecido é 
satisfeita 
– Neste caso, o predicado conhecido = {i : 1..tamanho ⦁ nomes(i)} de 
Abs indica que nome? não é um elemento de nomes(i): ∀i : 
1..tamanho ⦁ nome? ≠ nomes(i)
 106
Exemplo
• Note que seria possível traduzir facilmente a operação 
concreta para uma linguagem de programação qualquer: 
 procedimento AdicionaAniversario(nome : NOME, data : 
DATA); 
 inicio 
 tamanho := tamanho + 1; 
 nomes[tamanho] := nome; 
 datas[tamanho] := data; 
 fim;
 107
Exemplo
• A operação de consulta de aniversários pode ser definida com 
o seguinte esquema:
 108
Exemplo
• O quantificador existencial resulta em um loop no código do 
programa: 
 procedimento ConsultaAniversario(nome : NOME, data : 
DATA); 
 var i : INTEIRO; 
 inicio 
 i := 1; 
 enquanto nomes[i] != nome faca i := i + 1; 
 data := datas[i]; 
 fim;
 109
Exemplo
• Neste caso, a operação de lembrete também deve ser 
alterada:
 110
Exemplo
• Neste caso, a operação de lembrete também deve ser 
alterada (continuação):
 111
Exemplo
• O código do programa pode ser definido da seguinte maneira: 
 procedimento Lembrete(hoje : DATA, 
 listacartao : array [1..] de 
NOME 
 ncartoes : INTEIRO); 
 var j : INTEIRO; 
 inicio 
 ncartoes := 0; 
 j := 0; 
 Enquanto j < tamanho faca 
 inicio 
 j := j + 1;
 112
Exemplo
 j := j + 1; 
 se datas[j] = hoje então 
 inicio 
 ncartoes := ncartoes + 1; 
 listacartao[ncartoes] := nomes[j]; 
 fim 
 fim 
 fim; 
 
 113
Exemplo
• O estado inicial do programa possui tamanho = 0: 
• Resultando no seguinte código do programa: 
 procedimento IniciaLivroAniversario; 
 inicio 
 tamanho := 0; 
 fim;
 114
Exemplo
• Considere, como outro exemplo, a representação de uma 
base de dados 
• Dois tipos básicos de dados devem ser definidos: 
– [ENDERECO, PAGINA] 
• É possível definir uma “abreviação” para o conjunto de todas 
as funções a partir de ENDERECO para PAGINA 
– BASEDADOS == ENDERECO → PAGINA
 115
Exemplo
• O espaço de estados deste sistema pode ser definido com o 
seguinte esquema:
 116
Exemplo
• Deve ser possível acessar a “página” em um endereço 
específico:
 117
Exemplo
• Deve ser possível uma nova “página” na base de dados:
 118
Exemplo
• Por outro lado, uma possível operação de backup é a 
realização de uma cópia da base de dados atual:
 119
Exemplo
• Deve ser possível também restaurar a base de dados:
 120
Exemplo
• Entretanto, é possível melhorar esta especificação 
• Considere agora que somente uma cópia da base de dados 
será mantida 
– Menos recursos consumidos 
• Portanto, uma cópia “mestre” é utilizada:
 121
Exemplo
• O registro de alterações pode ser realizado considerando que 
o último ponto de verificação é uma função parcial de 
endereço para páginas 
– Nem toda página será atualizada 
 122
Exemplo
• O espaço de estados concreto pode ser descrito por: 
• Portanto: 
– A base de dados mestre é o backup 
– A base de dados atual é mestre ⊕ alteracoes
 123
Exemplo
• A operação concreta de acesso é definida da seguinte 
maneira:
 124
Exemplo
• O código do programa pode ser definido da seguinte maneira: 
 procedimento Acesso(e : ENDERECO, p : PAGINA); 
 var r : RELATORIO; 
 inicio 
 RecuperaAlteracao(e,p,r); 
 se r != ok então 
 LerMestre(e,p) 
 fim;
 125
Exemplo
• O código do programa pode ser definido da seguinte maneira: 
 procedimento Acesso(e : ENDERECO, p : PAGINA); 
 var r : RELATORIO; 
 inicio 
 RecuperaAlteracao(e,p,r); 
 se r != ok então 
 LerMestre(e,p) 
 fim;
 126
Opera somente em partes 
do estado
Exemplo
• O código do programa pode ser definido da seguinte maneira: 
 procedimento Acesso(e : ENDERECO, p : PAGINA); 
 var r : RELATORIO; 
 inicio 
 RecuperaAlteracao(e,p,r); 
 se r != ok então 
 LerMestre(e,p) 
 fim;
 127
Retorna uma página a 
partir da base de dados 
mestre
Exemplo
• A operação para recuperar alteração pode ser definida daseguinte maneira:
 128
Exemplo
• A operação para ler registro mestre pode ser definida da 
seguinte maneira:
 129
Exemplo
• A operação concreta para atualização pode ser definida da 
seguinte maneira:
 130
Exemplo
• A operação concreta para ponto de backup pode ser definida 
da seguinte maneira:
 131
Exemplo
• A operação concreta para restauração pode ser definida da 
seguinte maneira:
 132
Métodos Formais
 Introdução 
Prof. Álvaro Sobrinho 
alvaro.sobrinho@ufersa.edu.br