Conjuntos (continuação)
Notação
– Os operadores de conjunto (união,
interseção, etc.) serão introduzidos
através de definições axiomáticas na
linguagem Z
– Forma geral de uma definição axiomática
[T]
declaração
predicado
– onde T é uma variável de tipo que
possibilita definições polimórficas
1
União

Definição
[X]
__: [P X  [P X  [P X
 S, T : [P X . S  T = {x:X | x  S  x  T}

Teoremas
SS=S
ST=TS
S  (T  R) = (S  T)  R
S  {} = S
S  (S  T)
idempotência
comutatividade
associatividade
elemento neutro
2
Interseção

Definição
[X]
__: [P X  [P X  [P X
 S, T : [P X . S  T = {x:X | x  S  x  T}

Teoremas
SS=S
ST=TS
S  (T  R) = (S  T)  R
S  {} = {}
(S  T)  S
S  (T  R) = (S  T)  (S  R)
S  (T  R) = (S  T)  (S  R)
idempotência
comutatividade
associatividade
elemento nulo
distributividade
distributividade
3
Diferença

Definição
[X]
_\_: [P X  [P X  [P X
 S, T : [P X . S \ T = {x:X | x  S  x  T}

Teoremas
S \ S = {}
S \ {} = S
{} \ S = {}
(S \ T) \ R = S \ (T  R)
(S \ T)  S
(S  T) \ R = (S \ R)  (T \ R)
(S  T) \ R = (S \ R)  (T \ R)
4
União Distribuída

Generalização da união binária para um
número arbitrário de conjuntos
 {S1, S2, ..., Sn} = S1  S2  ...  Sn

Exemplos
 {{1,2,3}, {2,3,4}, {5,6}} = {1,2,3,4,5,6}
 {{1}} = {1}
 {{}} = {}
5
União Distribuída

Definição
[X]
 : [P ([P X)  [P X
 SS : [P ([P X) .  SS = {x:X |  S : SS . x  S}

Teoremas
 {} = {}
 {S,T} = S  T
 (SS  TT) = ( SS)  ( TT)
( SS) \ T =  {S : SS . S \ T}
SS  TT  ( SS)  ( TT)
6
Interseção Distribuída

Generalização da interseção binária
para um número arbitrário de conjuntos
 {S1, S2, ..., Sn} = S1  S2  ...  Sn

Exemplos
 {{1}, {1,2}, {1,2,3}} = {1}
 {{1},{1,2},{2,3}} = {}
 {{1}} = {1}
7
Interseção Distribuída

Definição
[X]
 : [P ([P X)  [P X
 SS : [P ([P X) .  SS = {x:X |  S : SS . x  S}

Teoremas
 {S,T} = S  T
 (SS  TT) = ( SS)  ( TT)
S \ ( TT) =  {T : TT . S \ T}
SS  TT  ( TT)  ( SS)
8
Uma especificação usando conjuntos


Controle de acesso de pessoas a um local
(por exemplo, sala de aula)
Operações
–
–
–
–

Inicialização (inicialmente não há pessoas)
Inclusão (chegada de uma nova pessoa)
Remoção (saída de uma pessoa)
Consulta (verifica se ausente/presente)
Restrição
– Máximo de 50 pessoas na sala
9
Uma especificação usando conjuntos:
estrutura de um solução imperativa
program Controle_Acesso
type Pessoa = ...
type Mensagem = ausente | presente;
var s : set Pessoa;
const lim = 50;
procedure init () ... s = {} ...
procedure inclusao(p: Pessoa)
... if (lim < 50) and (p  s) then s = s  {p} ...
procedure exclusao(p: Pessoa)
... if p  s then s = s \ {p} ...
procedure consulta(p: Pessoa; m: Mensagem)
... if p  s then m = presente else m = ausente ...
10
Em Z ...

Deve-se abstrair da representação de alguns
tipos que modelam entidades básicas (como
Pessoa). Isto é feito introduzindo-se apenas
um nome para o tipo, entre colchetes, sem
uma definição
– Exemplo: [Pessoa]

Constantes são introduzidas como em
linguagens de programação
– Exemplo: lim == 50

Tipos enumerados são semelhantes aos
datatypes de programação funcional
– Exemplo: Msg ::= ausente | presente
11
Em Z ...

As variáveis globais, juntamente com as
restrições sobre valores que estas podem
assumir, formam o estado do sistema e são
declaradas dentro de uma estrutura
denominada esquema
– Exemplo:
Estado
s : |P Pessoa
# s  lim
12
Em Z ...


Como variáveis em lógica não podem ser atribuídas,
faz-se necessária uma convenção para representar a
mudança de estado. Em Z, usa-se o símbolo ’ no
final do nome da variável
– Exemplo: s’ = s \ {p}
Quando o símbolo é usado em um nome de
esquema, este é adicionado a todas as variáveis
– Exemplo: Estado´ corresponde ao esquema
Estado’
s’ : |P Pessoa
# s’  lim
13
Em Z ...

A inicialização define os valores iniciais das
variáveis de estado e devem usar o ’ para
indicar a atribuição de valor
– Exemplo:
Init
Estado’
s’ = {}

Observe a ocorrência do nome do esquema
Estado na parte de declaração de Init; isto
permite o acesso às variáveis
14
Em Z ...

Algumas operações modificam o estado e
referenciam variáveis de estado iniciais e as
finais (com o ’). Tais operações devem incluir
o esquema D Estado
D Estado
Estado
Estado’
que equivale a
D Estado
s,s’ : |P Pessoa
#s  lim  #s’ lim
15
Em Z ...

A operação de inclusão é um exemplo de
operação que muda o estado
Inclusão
D Estado
p?: Pessoa
(#s < lim ^ p?  s)
s’ = s  {p?}

Observe a variável p? na parte de declaração
de esquema: é uma convenção para
variáveis de entrada
16
Em Z ...

Algumas operações não modificam o estado
mas devem tornar isto explícito. Tais
operações devem incluir o esquema
XEstado
– Exemplo:
XEstado
Estado
Estado’
s’ = s
17
Em Z ...

A operação de consulta é um exemplo de
operação que não muda o estado
Consulta
X Estado
p?: Pessoa
m!: Msg
(p?  s ^ m! = presente) v
(p?  s ^ m! = ausente)

Observe a variável m! na parte de declaração
de esquema: é uma convenção para
variáveis de saída
18
Especificação em Z: Controle de Acesso
[Pessoa]
lim == 50
Estado
s : |P Pessoa
Init
Estado’
# s  lim
s’ = {}
Inclusão
D Estado
p?: Pessoa
(#s < lim ^ p?  s)
s’ = s  {p?}
Exclusão
D Estado
p?: Pessoa
p?  s
s’ = s \ {p?}
Msg ::= ausente
| presente
Consulta
X Estado
p?: Pessoa
m!: Msg
(p?  s ^ m! = presente) v
(p?  s ^ m! = ausente)
19