context Company inv:
self.numberOfEmployees > 50
        
    
context c : Company inv:
c.numberOfEmployees > 50
        
    
context Person::income(d : Date) : Integer
post:  result = 5000
        
    
context Person::getCurrentSpouse() : Person
pre:   self.isMarried = true
body:  self.mariages->select( m | m.ended = false ).spouse
        
    
context Person::income : Integer
init:   parents.income->sum() * 1% -- pocket allowance
derive:  if underAge
       then parents.income->sum() * 1% -- pocket allowance
       else job.salary                    -- income from regular job
       endif
        
    
context Person inv:
let income : Integer = self.job.salary->sum() in
if isUnemployed then
   income < 100
elseincome >= 100 
endif
        
    
context Person
def: income : Integer = self.job.salary->sum() 
def: nickname : String = 'Little Red Rooster'
def: hasTitle(t : String) : Boolean = self.job->exists(title = t)
        
    
context Person inv:
self.age > 0
        
    
aPerson.income(aDate).bonus = 300 and
aPerson.income(aDate).result = 5000
        
    
context Person::income (d: Date) : Integer
post: result = age * 1000
        
    
context Company inv:
self.stockPrice() > 0
        
    
context Company 
inv: self.manager.isUnemployed = false
inv: self.employee->notEmpty() 
        
    
context Person inv:
self.employer->size() < 3
        
    
context Person inv:
self.employer->isEmpty()
        
    
context Company inv:
self.manager->size() = 1
        
    
context Company inv:
self.manager.age > 40
        
    
context Person inv: 
self.wife->notEmpty() implies self.wife.gender = Gender::female
        
    
context Person inv:
self.wife->notEmpty() implies self.wife.age >= 18 and
self.husband->notEmpty() implies self.husband.age >= 18
        
    
context Company inv:
self.employee->size() <= 50
        
    
context Person inv:
self.job 
        
    
context Person inv:
self.employeeRanking[bosses]->sum() > 0
        
    
context Person inv:
self.employeeRanking[employees]->sum() > 0
        
    
context Person inv:
self.employeeRanking->sum() > 0 -- INVALID!
        
    
context Person inv:
self.job[employer] 
        
    
context Job
inv: self.employer.numberOfEmployees >= 1
inv: self.employee.age > 21
        
    
context Bank inv: 
self.customer
        
    
context Bank inv:
self.customer[8764423]
        
    
context Person inv:
Person.allInstances()->forAll(p1, p2 |
                                 p1 <> p2 implies 
                                 p1.name <> p2.name)
        
    
context Person::birthdayHappens()
post: age = age@pre + 1
        
    
context Company::hireEmployee(p : Person)
post: employees = employees@pre->including(p) and
          stockprice() = stockprice@pre() + 10
        
    
context Person def:
attr statistics : Set(TupleType(company: Company, 
                                numEmployees: Integer, 
                                wellpaidEmployees: Set(Person), 
                                totalSalary: Integer)) = 
      managedCompanies->collect(c | 
       Tuple { company: Company = c,
           numEmployees: Integer = c.employee->size(), 
           wellpaidEmployees: Set(Person) = 
                        c.job->select(salary>10000).employee->asSet(),
           totalSalary: Integer = c.job.salary->sum()
          }
      )
        
    
context Person inv:
statistics->sortedBy(totalSalary)->
    last().wellpaidEmployees->includes(self)
        
    
context Company inv: 
self.employee->select(age > 50)->notEmpty()
        
    
context Company inv: 
self.employee->select(age > 50)->notEmpty()
context Company inv: 
self.employee->select(p | p.age > 50)->notEmpty()
        
    
context Company inv: 
self.employee.select(p : Person | p.age > 50)->notEmpty()
        
    
context Company inv: 
self.employee->reject( isMarried )->isEmpty()
        
    
self.employee->collect( birthDate )
self.employee->collect( person | person.birthDate )
self.employee->collect( person : Person | person.birthDate )
self.employee->collect( birthDate )->asSet()
        
    
self.employee->collect(birthdate)
self.employee.birthdate
        
    
context Company 
inv:     self.employee->forAll( age <= 65 )
inv:     self.employee->forAll( p | p.age <= 65 )
inv:     self.employee->forAll( p : Person | p.age <= 65 )
        
    
context Company inv: 
self.employee->forAll( e1, e2 : Person |
                 e1 <> e2 implies e1.forename <> e2.forename)
        
    
context Company inv: 
self.employee->forAll (e1 | self.employee->forAll (e2 |
                   e1 <> e2 implies e1.forename <> e2.forename))
        
    
context Company inv: 
self.employee->exists( forename = 'Jack' )
        
    
context Company inv: 
self.employee->exists( p | p.forename = 'Jack' )
context Company inv: 
self.employee->exists( p : Person | p.forename = 'Jack' )
        
    
context Person inv:
employer->forAll( employee->exists( lastName = name) )
context Person
inv: employer->forAll( employee->exists( p | p.lastName = name) ) 
inv: employer->forAll( employee->exists( self.lastName = name) )