package bank
-- OCL constraints (see course) associated to a bank system

-- Account
context Account 
inv balanceCorrect : self.balance >= self.min
inv negativeMin : min <= 0
inv existingId : accountNumber->notEmpty()

context Account::credit(amount : Integer)
pre positiveAmount : amount > 0
post creditDone : balance = balance@pre + amount  

context Account::balance : Integer
init : 0

context Person
-- a junior person does not own accounts
inv hasAccount : self.age < 18 implies account->isEmpty()
-- more precisely, any major person owns an account
inv hasAccount2 : if age < 18  
                 then account->isEmpty()
                 else account->notEmpty()
                 endif
-- an administrator does not manage its own accounts
inv : self.managedAccount->forAll 
    (c  | c.owner <> self)
-- idem
inv : self.managedAccount->forAll(owner <> self)
-- the counsellor of a client manages at least one of its accounts
inv : self.account->exists(c | c.administrator->includes(counsellor)) 


context Agency
-- any agency must house clients with low income
inv : self.client->select(p | p.income < 100)->notEmpty()

context Agency::ageClients() : Set(Integer)
body : client.age->asSet()

context Agency::createAccount(p : Person) : Account
pre : client->includes(p)
post : result.oclIsNew() and 
       client = client@pre->including(p) and
       p.account = p.account@pre->including(result)

endpackage