Added the company model.

README.md

@@ -6,6 +6,7 @@ models were developed in the context of the original HOL-OCL and
 SecureUML.
 
 ## Models
+* **[Company:](./company)** A simple company model, inspired by the OCL standard.
 * **[Royals and Loyals:](./royals_and_loyals)** The famous royals-and-loyals example.
 * **[Stack:](./stack)** A simple stack.
 

company/README.md

@@ -0,0 +1,10 @@
+# Company
+A simple company example, inspired by the company model in the 
+OCL 2.0 standard (see Chapter 7 of 03-10-14).
+
+## Data Sheet
+* Format:               ArgoUML 0.26
+* Language:             UML/OCL
+
+For further information (license, citation, etc.), please look at the [README.md](../)
+of the main directory. 

company/company.ocl

@@ -0,0 +1,236 @@
+-- Copyright (c) 2003-2007 ETH Zurich, Switzerland
+--                    2016 The University of Sheffield, UK
+-- 
+-- All rights reserved.
+-- 
+-- Redistribution and use in source and binary forms, with or without
+-- modification, are permitted provided that the following conditions are met:
+-- 
+-- * Redistributions of source code must retain the above copyright notice, this
+--   list of conditions and the following disclaimer.
+-- 
+-- * Redistributions in binary form must reproduce the above copyright notice,
+--   this list of conditions and the following disclaimer in the documentation
+--   and/or other materials provided with the distribution.
+-- 
+-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+-- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+-- IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+-- DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+-- FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+-- DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+-- SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+-- CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+-- OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+-- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+-- 
+
+package Company    
+    
+context Company 
+inv: self.numberOfEmployees > 50   
+    
+context Company inv:
+self.numberOfEmployees > 50
+        
+    
+context Person::income(date : Date) : Integer
+  post:  result = 5000
+        
+    
+-- context Person::getCurrentSpouse() : Person
+-- pre:   self.isMarried = true
+-- body:
+-- self.marriage[wife]->select( m | m.ended = false )->
+--                                 one(true).husband
+        
+    
+-- context Person::income2 : Integer
+-- init:   (parents.income2->sum() * 1/100).round() -- pocket allowance
+-- derive:  if underAge
+--       then (parents.income2->sum() * 1/100).round() 
+--       else job.salary->sum()       
+--       endif
+        
+    
+-- [hol-ocl (AssocCallExpr)] context Person inv:
+-- [hol-ocl (AssocCallExpr)] let sum_income : Integer = self.Job.salary->sum() in
+-- [hol-ocl (AssocCallExpr)] if isUnemployed then
+-- [hol-ocl (AssocCallExpr)]    sum_income < 100
+-- [hol-ocl (AssocCallExpr)] else sum_income >= 100 
+-- [hol-ocl (AssocCallExpr)] endif
+        
+    
+-- [hol-ocl (AssocCallExpr)] context Person
+-- [hol-ocl (AssocCallExpr)] def: income : Integer = self.Job.salary->sum() 
+-- [hol-ocl (AssocCallExpr)] def: nickname : String = 'Little Red Rooster'
+-- def: hasTitle(t : String) : Boolean = self.Job->exists(tile:String | title = t)
+        
+    
+context Person inv:
+self.age > 0
+        
+    
+context Person::income (date: 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
+        
+    
+-- [hol-ocl (AssocCallExpr)] context Person inv:
+-- [hol-ocl (AssocCallExpr)] self.Job->size() <= 2 
+        
+    
+-- context Person inv:
+-- self.employeeRanking[bosses].score->sum() > 0
+        
+    
+-- context Person inv:
+-- self.employeeRanking[employees].score->sum() > 0
+        
+    
+        
+    
+        
+    
+-- context Job
+-- inv: self.employer.numberOfEmployees >= 1
+-- inv: self.employee.age > 21
+        
+    
+-- context Bank inv: 
+-- not self.customer->exists(underAge = true)
+        
+    
+-- context Bank inv:
+-- self.customer[8764423]->forAll(underAge = false)
+
+        
+    
+context Person inv:
+self.allInstances()->forAll(p1:Person, p2:Person |
+                                 p1 <> p2 implies 
+                                 p1.lastName <> p2.lastName)
+        
+    
+-- context Person::birthdayHappens()
+-- post: age = age@pre + 1
+        
+    
+-- context Company::hireEmployee(p : Person)
+-- post: employee = employee@pre->including(p) and
+--                stockPrice() = stockPrice@pre() + 10
+        
+    
+-- context Person def:
+-- statistics : Bag(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(e:Person | e.age > 50)->notEmpty()
+        
+    
+context Company inv: 
+self.employee->select(e:Person | e.age > 50)->notEmpty()
+context Company inv: 
+self.employee->select(p: Person | p.age > 50)->notEmpty()
+        
+    
+context Company inv: 
+self.employee->select(p : Person | p.age > 50)->notEmpty()
+        
+    
+context Company inv: 
+self.employee->reject( p:Person | p.isMarried )->isEmpty()
+        
+    
+        
+    
+inv: self.employee->collect(p:Person | p.birthDate)->size() > 0
+inv: self.employee.birthDate->size() > 0
+        
+    
+context Company 
+inv:     self.employee->forAll(p:Person | p.age <= 65 )
+inv:     self.employee->forAll( p:Person | p.age <= 65 )
+inv:     self.employee->forAll( p : Person | p.age <= 65 )
+        
+    
+context Company inv: 
+self.employee->forAll( e1 :Person , e2 : Person |
+                 e1 <> e2 implies e1.firstName <> e2.firstName)
+        
+    
+context Company inv: 
+self.employee->forAll (e1 :Person | self.employee->forAll (e2:Person |
+                   e1 <> e2 implies e1.firstName <> e2.firstName))
+        
+    
+context Company inv: 
+self.employee->exists( p:Person | p.firstName = 'Jack' )
+        
+    
+context Company inv: 
+self.employee->exists( p :Person | p.firstName = 'Jack' )
+context Company inv: 
+self.employee->exists( p : Person | p.firstName = 'Jack' )
+        
+    
+context Person inv:
+employer->forAll( e:Company | e.employee->exists( p:Person|p.lastName = e.name) )
+context Person
+inv: employer->forAll( c:Company | c.employee->exists( p : Person | p.lastName = c.name) ) 
+        
+endpackage