Tipos de Dados em Z e B

Sistemas de tipos em Z e B [1]

Motivação [página 85]

Existem duas principais razões para impormos um sistema de tipos para nossas especificações na notação Z. A primeira delas é a de garantir que os membros de um conjunto sejam todos elementos de um mesmo tipo ou natureza. A segunda é que o uso irrestrito da teoria dos conjuntos pode nos levar à construção de "conjuntos" contraditórios.

[página 86]
Imagine que estejamos especificando um sistema simples para gerenciar uma locadora de filmes. Durante o processo de criação da especificação surgirão vários conjuntos. Alguns deles são:

  • Acervo: conjunto de filmes de que dispõe a locadora;
  • Locadas: conjunto de filmes que estão locadas;
  • Disponiveis: conjunto de filmes que estão disponíveis para locação;
  • Clientes: Clientes cadastrados na locadora.

Note que utilizando os conceitos de operadores da teoria dos conjuntos podemos criar novos conjuntos. Alguns exemplos são:

  • $Acervo / Locadas$
  • $Disponiveis \cup Locadas$

Porém existem alguns tipos de operações e comparação que não fazem sentido dentro das especificações. Como exemplo podemos dar o seguinte conjunto: $Disponiveis \cup Clientes$.
Para evitar este tipo de situação dentro de uma especificação em Z a notação não permite o uso de tipos diferentes dentro das expressões e predicados.

[página 87]
A segunda situação é a do paradoxo de Russell. Que encontra uma situação de contradição dentro do conceito da teoria dos conjuntos matemática.

$U = \{ s \mid EUmConjunto(s) \wedge (s \not\in s)\}$
$P = U \in U$

Caso P seja verdade, então s = U e U não poderia pertencer a se mesmo. O que entra em contradição com P.
Já no caso de P ser falso, então pela definição de U este mesmo conjunto U pertenceria a si mesmo. O que contradiz novamente P.

Em Z o problema do paradoxo de Russel é resolvido através da limitação da relação de pertinência. Logo um conjunto não poderá ser elemento de si mesmo. Além disso o sistema de tipos restringe a natureza de cada um dos elemento definidos no conjunto.

Noção de tipos em Z [página 88]

Em Z, o tipo de um objeto determina um conjunto de dados, ou valores, que esse objeto pode assumir. Todo objeto mencionado numa especificação em Z deve ser primeiramente declarado.
Quando os tipos são associados a um objeto este permanecerá associado com o tipo durante toda a especificação. Desta forma um objeto só tem um tipo definido durante a especificação.

Tipos Inicias [página 88]

Os tipos inicias designam conjuntos predefinidos cuja a estrutura interna não é definida. A única características destes tipos é que dados dois destes conjuntos ele são disjuntos. O escopo destes tipos é iniciado a partir do ponto de sua declaração.

Os tipos inicias utilizam a seguinte notação : [ NOME ].

Alguns exemplos de tipos iniciais:

  • [CODIGOS]
  • [PESSOAS]
  • [CODIGOS,PESSOAS]

[página 93]
A linguagem Z já traz um tipo inicial embutido para representar o conjunto dos inteiros $\mathbb{Z}$. Este tipo tem relacionados os operadores aritméticos e relacionais, tais como +, -, *, div, mod, > e <.

Variáveis em Z [página 89]

Em Z, variáveis são declaradas construindo uma lista de seus nomes, separados por vírgulas, terminando a lista com o símbolo de dois-pontos, e escrevendo em seguida o nome do tipo que será associado às variáveis ora declaradas. As variáveis só podem assumir valores escolhidos dentre aqueles delimitados por seu tipo.

São exemplos de declaração de variáveis:

  • u,v:CODIGOS
  • p : PESSOAS
  • u,v : CODIGOS; p : PESSOAS

É importante lembrar que as variáveis em Z estão mais próximas da definição de variáveis matemáticas do que o conceito tradicional de variáveis numa linguagem de programação. Para estas variáveis não existe nenhuma associação com a memória ou espaço de alocação da máquina.

Tipos enumerados [página 91]

Imagine que precisamos definir um conjunto de poucos elementos disjuntos. Poderíamos fazer isso usando os conceitos vistos até agora da seguinte forma:

Exemplo LigDesliga:

[LIGDESLIGA]
ligada:LIGDESLIGA
desligada:LIGDESLIGA

Desta forma introduzimos um tipo simples LIGDESLIGA e criamos duas variáveis para este tipo. Porém ainda faltam garantir algumas propriedades para esta especificação. São elas:

  • Garantir que ligada e desligada são objetos destintos.
  • Garantir que ligada e desligada são os únicos objetos deste tipo.

Podemos especificar estas duas restrições através dos predicados:

  • $ligada \ne desligada$
  • $\forall x : LIGDESLIGA \bullet ((x = ligada) \vee (x = desligada))$

Em Z existe uma construção especial para lidar com este tipo de situação. São os tipos enumerados. Podemos definir o mesmo significado do exemplo acima com a expressão: $LIGDESLIGA ::= ligada \mid desligada$.

Em geral, uma declaração na forma $X ::= n_1 \mid n_2 \mid ... \mid n_k$, onde $k \geq 1$, introduz um tipo enumerado com as seguintes características:

  1. Define X como o nome do novo tipo.
  2. Declara os nomes das constantes $n_1, ..., n_k$, todas do tipo X.
  3. Introduz predicados (implícitos) os quais garantem que o tipo X é formado exatamente pelos k valores designados pelos objetos $n_1, ..., n_k$, e garantem que esses objetos são todos distintos entre si.

Conjuntos e o tipo potência (conj. das partes) [página 95]

Para declararmos conjuntos em Z de maneira enumerativa todos os elementos deve ter sido previamente declarados.

Exemplo:

[PESSOAS]
jose,maria,marta,rui:PESSOAS
cod1,cod2:CODIGOS

{jose, maria, rui}
{cod1,cod2}

Questões :

  • O conjunto {jose,cod1,rui} é válido ?
  • Sendo S = {jose, maria, rui}. Qual seria o tipo de S ?

O conjunto potência associado ao tipo PESSOAS se chama tipo potência. Em Z,o conjunto das partes de um conjunto é representado pelo símbolo $\mathbb{P}$ e é chamado de conjunto potência. Desta forma o conjunto potência de $\mathbb{Z}$ é definido da seguinte forma $\mathbb{PZ}$.

Muitas vezes, é conveniente atribuirmos um nome ao conjunto definido. Em Z, isso é conseguido usando-se o símbolo ==.

Exemplo:
$PeqInt == \{1,2,3\}$

Uma outra forma de definir um conjunto em Z é utilizando uma expressão que representa um critério de pertinência. Essa forma tem a seguinte notação: $\{x_1:T_1, x_2:T_2,...; x_k:T_k \mid P \bullet t\}$.

Exemplos:
$\mathbb{N} == \{n : \mathbb{Z} \mid n \geq 0\}$
$\mathbb{N}_1 == \{n : \mathbb{Z} \mid n > 0\}$
$SomaQuad == \{n,m : \mathbb{Z} \mid n>3m \bullet n^{2} + m^{2}\}$
$\{x,y : \mathbb{N} \bullet x-y\}$

Produto Cartesiano [página 106]

Em Z o produto cartesiano é definido de maneira semelhante a notação matemática. Veremos a utilização das notações de produto cartesiano através de um exemplo.

Em geral, se $T_1, ..., T_k$ são tipos em Z, onde $k \geq 2$, então $T_1 \times T_2 \times ... \times T_k$ irá definir uma k-uplas para este produto cartesiano.

Imagine que estamos querendo especificar as fila de caixas de um banco. Vamos assumir que deveremos manter informações sobre os caixas e o número de pessoas na fila. Podemos definir esta estrutura através de um produto cartesiano de um tipo simples CAIXAS e um valor numérico $\mathbb{N}$. Teríamos a seguinte definição:

[CAIXAS]
$Fila == CAIXAS \times \mathbb{N}$
$filas : \mathbb{P} Fila$

Desta maneira definimos uma estrutura para manter as informações sobre as filas. Analisando as declarações feitas acima vemos que elas não garantem duas propriedades importantes da nossa especificação. São elas:

  • Um caixa não pode ter filas de tamanhos destintos.
  • Cada caixa tem pelo menos uma fila associada a si.

Podemos resolver este problema com essas declarações adicionais.

  • $\forall n_1,n_2:\mathbb{N}; c : CAIXAS \bullet ((c,n_1) \in filas \wedge (c,n_2) \in filas \Longrightarrow n_1 = n_2)$
  • $\forall c : CAIXAS \bullet (\exists n: \mathbb{N} \bullet (c,n) \in filas)$

É importante notar a diferença entres as seguintes construções:

  • $T_1 \times T_2 \times T_3$
  • $T_1 \times (T_2 \times T_3)$
  • $(T_1 \times T_2) \times T_3$
Bibliography
1. Moura, Arnaldo Vieira. Especificações em Z: Uma introdução. Editora Unicamp, São Paulo. 2001.
2. Potter, Ben; Sinclair, Jane; Till, David. Introduction to formal specification and Z. Prentice Hall Europe. 1996.
Unless otherwise stated, the content of this page is licensed under Creative Commons Attribution-ShareAlike 3.0 License