1) Initialement toutes les personnes doivent être des femmes

context Person::gender : Gender
init: Gender.female


2) Initialement le salaire d’un employé est de 1000 euros.

context Job::salary : Integer
init: 1000


3) Le directeur d’une société doit avoir plus de 40 ans.
context Company
inv: self.manager.age > 40


4. L’âge d’un individu est fonction du moment présent et de sa date de naissance.
context: Person::age: int
derive: Date.now() – self.birthdate


5. Si le chiffre d’affaires (turnover) d’une société est supérieur à 1 million d’euros, elle doit avoir plus que 10 employés.
context Company
inv: (NOT(self.turnover() > 1 000 000) OR (self.numberOfEmployees > 10))
ou
inv: (self.turnOver() > 1 000 000) implies (self.numberOfEmployees > 10)


6. Tous les employés d’une société doivent avoir plus de 18 ans.
context Person
inv: (self.isUnemployed() = FALSE) IMPLIES (self.age > 18)

context Job
inv: self.employee.age > 18


7. On ne peut pas commencer à travailler avant sa date de naissance.
context Job
inv: self->employee.birthDate < Job.startDate()


8. Un homme est marié avec une femme et une femme avec un homme.
context Marriage
inv: self.husband.gender = Gender.male AND self.wife.gender = Gender.female


9. Pour être mariés, il faut avoir plus que 18 ans.
context Person
inv: (self.isMaried() = TRUE) IMPLIES (self.age > 18)

context Marriage
inv: (self.husband.age > 18) AND (self.wife.age > 18)


10. Le fils a le même nom de famille que son père


11. On ne peut pas commencer à travailler le jour de son mariage.
context Job
inv: (self.employee.isMarried = FALSE) OR NOT(self.startDate = self.employee.marriage.date