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