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:
- Define X como o nome do novo tipo.
- Declara os nomes das constantes $n_1, ..., n_k$, todas do tipo X.
- 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$
