21
Notação Z - Predicados Formas de montar predicados em Z = 2200 ∈ 5 ¬ 5 1

Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

  • Upload
    hanhan

  • View
    213

  • Download
    0

Embed Size (px)

Citation preview

Page 1: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Predicados

● Formas de montar predicados em Z

= ∀∈ ∃¬ ∃1

∧ ∨ ⇒⇔

Page 2: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Operações

● Operações sobre tipos primitivos

ℤ ℕ

+ <

- >

* ≤

div ≥

mod ..

ℕ1 succ

Page 3: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Operações

● Operações sobre conjuntos

∈ - pertence

∪ - união

∩ - intersecção

\ - diferença

# - cardinalidade

⊆ - subconjunto

⊂ - subconjunto próprio

Page 4: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Operações

● Operações sobre conjuntos

= - igualdade

U - união generalizada

P - powerset

Page 5: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Operações

● Relações e funções● Relações binárias modelam objetos

que relacionam membros de dois conjuntos

A ↔ B = P(A x B)

r : A ↔ B

Page 6: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Operações

● Funçõestotal

parcial

total injetora

parcial injetora

total sobrejetora

parcial sobrejetora

parcial bijetora

total bijetora

Page 7: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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

°

Page 8: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Operações

● Operadores em relações e funções

◁ restrição de domínioConj ◁ Relação

▷ restrição de contra-domínio

◁ subtração de domínio

▷ subtração de contra-domínio

~ inverso relação

_ ( _ ) imagem relacionalRelação ( Conj ) => A<-->B X PA --> PB

Page 9: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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

Page 10: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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

Page 11: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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

Page 12: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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 naturaisBagX == X → ℕ1

TipoFicha == {vermelho, amarelo, azul}

BagFicha == {vermelho → 3, amarelo → 5}● São especificados através da palavra

reservada bag

Page 13: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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

+

-

Page 14: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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ígitosCaracter = {a, b, c, d, ..., z}

nome : seq1 Caracter

nome ≠ senha#senha < 8

Login

senha : seq1 Caracter

Page 15: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Exemplos

● Livro de Aniversário– De uma lista de pessoas conhecidas,

desejo 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

Page 16: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Exemplos

● Cliente X Servidor– Não podem existir 2 servidores com

mesmo id– Um servidor pode atender até no máximo

5 requisiçõeslimite == ℕlimite < 5

Servidor

req: limiteid: ℕ lServ : P Servidor

SisServ

∀ s1, s2 ∈ lServ •s1.id = s2.id ⇔ s1 = s2

Page 17: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

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 DISCIPLINATurma

∀n : ℕ • (n > 30 ∧ n ⊗ lTurma = ∅)

Page 18: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Exercícios

● Represente os tipos (não as operações) do sistema de controle de créditos:– Principais dados: cidade, sexo, idade,

escolaridade– Defina as pesquisas:

● Clientes que residem em João Pessoa e que são homens com mais de 30 anos

● Clientes que residem em Campina Grande, que possuem nível superior e que são mulheres

● etc...

Page 19: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Exercícios● Represente os tipos (não as operações)

de um sistema computacional:– Um processador aloca recursos para

execução de processos (não há duplicação de processos)

– Quando não há recurso disponível, o processo fica em uma fila de espera

– O processador pode estar em estado de espera ou execução

– Se um processador está em estado de espera, não há processos a serem alocados ou não há recursos disponíveis

Page 20: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Exercícios

● Represente os tipos (não as operações) de um sistema de segurança:– O sistema mantém uma três níveis de

hierarquia e um conjunto de usuários– Usuários podem ser cadastrados em

diferentes níveis hierárquicos, mas possui somente um nível

– O nível de hierarquia mais alto pode acessar dados dos níveis de hierarquia inferiores

Page 21: Notação Z - Predicadosaflj/EspecificDeSistemasDistribuidos/CSP-Z/Aula2Z.pdf · Livro de Aniversário – De uma lista de pessoas conhecidas, desejo representar uma agenda que armazene

Notação Z - Exercícios

● Altere o exemplo de aniversário para que o livro armazene os aniversariantes de hoje

[NOME,DATA]

lNomes : P NOME

lNomes = dom aniversarios

Agenda

aniverisarios : NOME →DATA