Cleanup: outdated commented stuff.
This commit is contained in:
parent
f10028567c
commit
1ab1de4a5e
|
|
@ -38,33 +38,33 @@ 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::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
|
||||
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:
|
||||
let sum_income : Integer = self.Job.salary->sum() in
|
||||
if isUnemployed then
|
||||
sum_income < 100
|
||||
else sum_income >= 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(tile:String | title = t)
|
||||
|
||||
|
||||
context Person inv:
|
||||
|
|
@ -100,8 +100,8 @@ 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.gender = Gender::female
|
||||
|
||||
|
||||
context Person inv:
|
||||
|
|
@ -113,33 +113,33 @@ context Company inv:
|
|||
self.employee->size() <= 50
|
||||
|
||||
|
||||
-- [hol-ocl (AssocCallExpr)] context Person inv:
|
||||
-- [hol-ocl (AssocCallExpr)] self.Job->size() <= 2
|
||||
context Person inv:
|
||||
self.Job->size() <= 2
|
||||
|
||||
|
||||
-- context Person inv:
|
||||
-- self.employeeRanking[bosses].score->sum() > 0
|
||||
|
||||
|
||||
-- context Person inv:
|
||||
-- self.employeeRanking[employees].score->sum() > 0
|
||||
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 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)
|
||||
|
||||
|
||||
|
||||
|
|
@ -149,33 +149,33 @@ self.allInstances()->forAll(p1:Person, p2:Person |
|
|||
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 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:
|
||||
|
|
|
|||
Reference in New Issue