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:
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
Nenhum comentário:
Postar um comentário