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