Definiciones Ejemplo context Persona def: ingresos : Integer = self.puesto.sueldo->sum() def: apodo : String = ’Gallito rojo’ Navegación y combinación de expresiones Ejemplos a) “Los casados tienen al menos 18 años de edad” context Persona inv: self.esposa- >notEmpty() implies self.esposa.edad >= 18 and self.esposo- >notEmpty() implies self.esposo.edad >= 18 b) “Una compañía tiene como mucho 50 empleados” context Companía inv: self.empleado- >size() <= 50