Invariantes de classes de entidade:

Contexto da classe Pessoa
	
-numero do BI unico
-pessoa eh masculino e feminino

Context Pessoa
Inv:Pessoa.allInstances() -> forAll(p1, p2: Pessoa or p1 <> p2 implies p1.getBI() <> p2.getBI())

Inv:Pessoa.allInstances() -> forAll(p: Pessoa | p.getSexo() = 'F' or p.getSexo() = 'M')



Contexto da classe User
	
-username de uma pessoa eh unico
-user tem que ser ou administrador ou super observador ou coordenador ou equipa de salvamento
-password com mais de 6 caracteres

Context User
Inv: User.allInstances() -> forAll(u1, u2: User | u1 <> u2 implies u1.getUsername() <> u2.getUsername())

Inv: User.allInstances() -> forAll(u: User | Exist(a: Administrador | a.getUsername() = u.getUsername()) or Exist(so: SuperObservador | so.getUsername() = u.getUsername()) or Exist(c: Coordenador | c.getUsername() = u.getUsername()) or Exist(es: EquipaSalvamento | es.getUsername() = u.getUsername()))

Inv: User.allInstances() -> forAll(u: User | u.getPassword().size() >= 6)


Contexto da classe ServiçoHospitalar
	
- o numero de pacientes de um hospital tem k ser maior ou igual a zero

Context ServiçoHospitalar
Inv: ServiçoHospitalar.allInstances() -> forAll(p: ServiçoHospitalar | p.getAllPacientes().size() >= 0)