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.