Construindo uma especificação do zero - Sistema Policial v.3

A terceira versão além de corrigir a falha da segunda versão, propõe uma mudança no TAD que armazena os atributos de uma pessoa, PERSON. Ao inves de tratar uma pessoa somente como um registro numerico (CPF), o registro da pessoa também deve conter o seu nome. Na especificação está mudança reflete a alteração do tipo PERSON, anteriormente definido como abreviacao de CPF, para um tipo definido em um schema.

Foi adicionado um teorema que prova que o predicado foreign? \notin population, adicionado à parte predicativa de REGISTRATION, é a precondição de REGISTRATION.

A terceira versão da especificação deste sistema pode ser encontrada em:

http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Sistema_Policial_v3.zip

Problemas da especificação anterior

Há um erro na especificação anterior (sistema_policial_v2) na operação REGISTRATION. Esta operação não verifica se o elemento que está sendo cadastrado já está cadastrado. O problema do elemento já estar cadastrado é que, foreign? pode pertencer ao conjunto offenders e a operação REGISTRATION o adicionará ao conjunto innocents. Esta operação pode, portanto, produzir um estado inválido para o sistema, onde innocents e offenders não são disjuntos. Para solucionar este problema, foi adicionado mais um predicado à parte predicativa de REGISTRATION. O predicado adicionado é: foreign? \notin population.

Construindo uma especificação do zero - Sistema Policial v.2

Para corrigir o problema da versão anterior existem duas vertentes, a primeira é assumir que PERSON não está contido em population. Esta abordagem sugere a retirada da terceira invariante do sistema (shema DATABASE).

Outra solução é assumir todas pessoas já são conhecidas pelo sistema (population), e forçar que o sistema tenha uma visão pessimista das pessoas, isto é, todas pessoas são inicialmente alocadas com antecedentes criminais. Desta forma, o ato de cadastrar uma pessoa corresponde a remove-la do conjunto offenders e coloca-la no conjunto innocents.

A primeira solução é a mais adequada, pois em um sistema computacional os dados são entrados a medida que são colhidos, isto é, as pessoas vão sendo cadastradas a medida surge esta necessidade. Não existe, a priori, um cadastro de todas pessoas com o qual o sistema policial irá operar.

Para conferir se o estado sugerido é factível, vamos propor um estado inicial INIT_DATABASE e provar o teorema da inicialização para DATABASE. Para provar este teorema utilizamos poucos comandos de prova. O comando Invoke é utilizado para realizar a expansão de um schema. Este comando pode ser utilizado recebendo ou não parâmetros.

A segunda versão da especificação deste sistema pode ser encontrada em:

http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Sistema_Policial_v2.zip

Problemas da especificação anterior

Há um problema nesta especificação (sistema_policial_v1). Para registrar uma pessoa, assume-se que esta pessoa não pertence ao conjunto da população. No entanto, esta noção não é condizente com a invariante do sistema que afirma que toda pessoa existente já pertence a população. Note inclusive, que uma pessoa nesta especificação é um número. Assim, a invariante afirma que todo elementode Z (\num) é também elemento de population.

Construindo uma especificação do zero - Sistema Policial v.1

A partir desta postagem, é esperado que o leitor já tenha realizado a leitura dos 14 primeiros capítulos do Using Z. Por ora, não é necessário ler o capitulo 13 (Promotion) nem ler e o trecho do capitulo 14 que utiliza Promotion.

Esta especificação foi desenvolvida recentemente por mim. Meu propósito foi avaliar a dificuldade de escrever uma especificação a partir do zero. Abaixo descrevo um problema fictício, que motiva o desenvolvimento da especificação:


Descrição do problema: Sistema Policial

Deve ser especificado um sistema que gerencie uma base de dados de pessoas. A chave primaria utiliza para identificar as pessoas é o número do CPF. O sistema deve permitir a classificação das pessoas cadastradas em dois grupos:

Grupo 1: pessoas sem histórico criminal.
Grupo 2: pessoas com histórico criminal.

A partir desta definição, propus a primeira versão da especificação. A especificação é apresentada utilizando as conveções LaTex para Z. Estas convenções podem ser encontradas no Reference Card, distribuido junto com o Z/Eves. A sequencia de passos para compor esta especificação foi:

1. Definir um tipo dado para o nome das pessoas:

[NOME]

2. Para armazenar os numeros de CPF, é adequado utilizar números inteiros. Para tornar mnemonica a especificação defini uma abreviação para inteiros:

CPF == \num

3. Para representar as pessoas é utilizado o número do CPF. Para tornar mnemonica a especificação defini uma abreviação para CPF:

PERSON == CPF

4. O sistema deve armazenar as pessoas e classificá-las nos dois grupos. Os grupos 1 e 2 são distintos. O schema DATABASE foi usado para modelar o estado do sistema. Os atributos utilizados foram:

population - conjunto de todas pessoas cadastradas no sistema
offenders - conjunto de pessoas com antecendentes criminais
innocents - conjunto de pessoas sem ntecedentes criminais

5. Uma operação de registro de pessoas foi especificada. O schema REGISTRATION foi usado para modelar esta operação. Esta operação tem como entrada uma pessoa, denotada por foreign?. Quando uma pessoa é registrada ela é inserida nos conjuntos population e innocents. O conjunto offenders não sofre modificação nesta operação.

6. Uma operação de mudança de status foi especificada. Esta operação tem como entrada uma pessoa, denotada por p?. Se esta pessoa pertencer ao conjunto offenders, ela será removida do conjunto offenders e inserida no conjunto innocents. Se esta pessoa pertencer ao conjunto innocents, ela será removida do conjunto innocents e inserida no conjunto offenders.

7. Foi provado um teorema que afirma que toda pessoa satisfazendo as condições do estado do sistema, deve pertencer ao conjunto innocents ou então deve pertencer ao conjunto offenders.

A primeira versão da especificação deste sistema pode ser encontrada em:

http://www.dcc.ufba.br/~diego052/experimento/zevesblog/Sistema_Policial_v1.zip

Z/Eves no Windows (Mouse scroll)

A interface gráfica do Z/Eves para Windows possui bugs e costuma travar quando o scroll do mouse é utilizado. Se este problema ocorrer na sua instalação, desabilite o scroll do mouse através do painel de controle do Windows, no item "Mouse".

No Linux este problema não ocorre ;-)

The Z/EVES User’s Guide

Para compreender a interface gráfica e as funcionalidades providas pelo Z/Eves, você deve realizar a leitura do The Z/EVES 2.0 User’s Guide.

Este documento é distribuido com o software Z/Eves. Se você já baixou um pacote de instalação do Z/Eves, após instalá-lo você terá acesso a este documento.

O User's Guide ilustra o uso do Z/Eves através de especificações que usam Schemas. Schemas são abordados no capitulo 12 do Using Z. Por ora, não se preocupe com o entendimento da especificação exemplo do User's Guide, pois ela se tornará clara quando você avançar na leitura do Using Z. É suficiente neste primeiro momento que você note o que o Z/Eves pode lhe oferecer a principio: uma janela para interagir com a especificação (pag. 1-17), Type Checking e Domain Checking. (pag. 19-22).


Aconselho que a leitura do capitulo seis e posteriores do Using Z seja acompanhada do uso do Z/Eves. O que fizemos no MEFES foi: paralelo a leitura destes capitulos, escrevemos as especificações vistas no livro no Z/Eves. Esta é uma forma de habituar-se gradualmente ao ambiente do Z/Eves.

Onde encontrar o Python?

Uma versão do Python compativel com a versão 2.3.1 para Windows pode ser encontrada a partir do link:

http://www.dcc.ufba.br/~diego052/experimento/softwares/zeves/

Por que instalar o Python 2.3?

Você deve ter o Python instalado para poder usar a interface gráfica do Z/Eves. Caso não possua o Python, apenas poderá usar o Z/Eves em modo texto.