Paulo Borba e Augusto Sampaio

Departamento de Informática

Universidade Federal de Pernambuco

Especificação Usando Conjuntos

Teoria de Conjuntos• Conjuntos são coleções de elementos onde a

ordem e a repetição de elementos são irrelevantes

• Existem dois tipos de representação:

Por extenso Compreensão

{e1, ..., en} {x:S | P(x) . t(x)}

• Exemplos

{2, 3, 5, 7} {x:IN | x é primo x<10 . x}

{0, 2, 4, ...} {x:IN | true . 2 * x}

{0, 2, 4, 6} {x:IN | x<4 . 2 * x}

Teoria de Conjuntos

• Abreviações

{x:S . t(x)} = {x:S | true . t(x)}

{x:S | P(x)} = {x:S | P(x) . x}

• Portanto, {x:IN . 2 * x} = {x:IN | true . 2 * x}

{x:IN | x é primo x<10} =

{x:IN | x é primo x<10. x}

Uma Operação Básica: Pertinência

• x S

• x S = (x S)

• {x:S | P(x) . T(x)} = {x | x S P(x) . T(x)}

Axiomas Fundamentais

• Axioma 1. Uma expressão pertence a um conjunto se e somente se tal expressão é igual a um dos elementos deste conjunto:

x {e1, ..., en} (x=e1 ... x=en)

• Axioma 2. Extensionalidade(S=T) (x . x S x

T) (x . x S x T)

(x . x T x S)

Versões do Axioma da Extensionalidade

• Axioma 3. x{y:S | P(y)} (xS P(x))

• Axioma 4. x{y:S . t(y)} (y:S . x=t(y))

Conjunto Vazio: {}

• Axioma 5.

x . x {}

ou equivalentemente:

x . ( x {})

ou ainda:

x . ( x {})

Subconjuntos:

Definição. (S T) (x . x S x T)

Teoremas:

(S = T) (S T T S)

(S T) (S T (S = T))

(S T) (S T)

S . {} S

S . S S

Conjunto das Partes: |P

Definição. (T |P S) (T S)

Teoremas:

S . {} |P S

S . S |P S

Produto Cartesiano:

Definição.

p (S T) y, z . p = (y, z) y S z T

Usando a notação de compreensão, temos:

(S T) = {y : S; z : T . (y, z)}

Alguns operadores auxiliares

Funções de projeção sobre pares:

first (y, z) = y

second (y, z) = z

Cardinalidade de conjuntos finitos:

# S

União: Notação

Definição

[T]Declaração

predicado

[X] : |P X |P X -> |P X

S,T: |P X . S T = {x : X . x S x T}

Algumas propriedades da União

• ComutatividadeS T = T S

• Associatividade S (T R ) = (S T) R

• Idempotência S S = S

• Elemento neutro (identidade) S {} = S

Como prová-las?

Interseção: Definição

Propriedades comutatividade

associatividade

...

[X] : |P X |P X -> |P X

S,T: |P X . S T = {x : X . x S x T}

Diferença: \

Definição

Propriedades (S \ T) \ R = S \ (T Q)

S \ S = {}

S \ {} = S

...

[X]\ : |P X |P X -> |P X

S,T: |P X . S \ T = {x : X . x S x T}

União distribuída: Generalização para conjuntos de conjuntos

Exemplo: {{1,2,3},{3,4},{3,5}}= {1,2,3,4,5}

Definição

[X] : |P (|P X) -> |P X

SS: |P (|P X) . SS = {x:X | S:SS . x S}

Interseção distribuída: Generalização para conjuntos de conjuntos

Exemplo: {{1,2,3},{3,4},{3,5}}= {3}

Definição

[X] : |P (|P X) -> |P X

SS: |P (|P X) . SS = {x:X | S:SS . x S}

Exercício

• Especifique um cadastro de pessoas, com as seguintes operações:– inclui (inclusão de uma nova pessoa)– remove (remoção de uma pessoa existente)– consulta (retorna mensagem ausente ou presente)

• Restrição– Não pode haver mais do que uma quantidade de

pessoas especificada pela constante limite (com valor 100)

Notação

• Pode-se definir um novo tipo em Z (given set) simplesmente introduzindo-se o seu nome entre colchetes (abstraindo a representação)Exemplos: [Pessoa]

[Matricula, CPF]

Elementos destes tipos admitem apenas igualdade

Pode-se fazer analogia com uma classe vazia emJava:

Exemplo: class Pessoa {

}

Notação

• Tipos enumerados (free types) podem ser introduzidos de forma semelhante aos datatypes em programação funcionalExemplo: Mesagem ::= ausente | presente

• Constantes são introduzidas da forma usualExemplo: limite == 100

Especificação em Z

incluiEstadop? : Pessoa# s < limitep? s s’ = s {p?}

consultaEstadop? : Pessoa r! : Mensagem

(p? s m! = presente)(p? s m! = ausente)

initEstado’

s’ = {}

[Pessoa]

EstadoS: |P Pessoa

# s limite

Mensagem ::= ausente | presente

Limite == 100

Remove ...

Exercício

• Na aula anterior, vimos a especificação de conta com operações: credito, debito e get_saldo.

• Especifique um banco como uma coleção de contas, com as operações: cadastro, remove, credito, debito e get_saldo.

• Uma restrição e´que as contas devem ter números distintos

Notação

• Um esquema pode ser usado como um tipo, sendo seus componentes referenciados da mesma forma que atributos em uma linguagem OO. Considere o esquema:

Usando Conta como tipo: c : Conta

c.num ... c.saldo ...

Contanum: Numerosaldo: |N

Bibliografia

• Seção 4.1 do livro– The Z Notation, A Reference Manual, J. M. Spivey,

Prentice Hall

• (Mais detalhes) Capítulo 5 do livro– Using Standard Z: Specification, Refinement and

Proof, J. Woodcock & J. Davies, Prentice Hall