blob: 0a0a767817945a0c373c8d96f808c727f2e81533 [file] [log] [blame]
--------------------------------------------------------------------------------
-- Copyright (c) 2007,2008 M.Garcia and others.
-- All rights reserved. This program and the accompanying materials
-- are made available under the terms of the Eclipse Public License v2.0
-- which accompanies this distribution, and is available at
-- http://www.eclipse.org/legal/epl-v20.html
--
-- Contributors:
-- J.Warmer, A.Kleppe - original example in 'The Object Constraint Language Second Edition'
-- M.Garcia - realisation of the example for use within Eclipse
--------------------------------------------------------------------------------
import 'RoyalAndLoyal.ecore'
package RandL
context ServiceLevel
inv invariant_ServiceLevel19 :
(Sequence{'a', 'b', 'c', 'c', 'd', 'e'}->prepend('X')) = Sequence{'X', 'a', 'b', 'c', 'c', 'd', 'e'}
inv invariant_ServiceLevel17 :
(OrderedSet{'a', 'b', 'c', 'd'}->subOrderedSet(2, 3)) = OrderedSet{'b', 'c'}
inv invariant_ServiceLevel4 :
Bag{Set{1, 2}, Set{1, 2}, Set{4, 5, 6}}->isEmpty()
inv invariant_ServiceLevel12 :
(OrderedSet{'a', 'b', 'c', 'd'}->last()) = 'd'
inv invariant_ServiceLevel18 :
(Sequence{'a', 'b', 'c', 'c', 'd', 'e'}->append('X')) = Sequence{'a', 'b', 'c', 'c', 'd', 'e', 'X'}
inv invariant_ServiceLevel1 :
self.program.partners->isEmpty()
inv invariant_ServiceLevel10 :
(Set{1, 4, 7, 10}->symmetricDifference(Set{4, 5, 7})) = Set{1, 5, 10}
inv invariant_ServiceLevel7 :
Sequence{2, 1, 2, 3, 5, 6, 4}->isEmpty()
inv invariant_ServiceLevel5 :
Bag{1, 1, 2, 2, 4, 5, 6}->isEmpty()
inv invariant_ServiceLevel16 :
(Sequence{'a', 'b', 'c', 'c', 'd', 'e'}->subSequence(3, 5)) = Sequence{'c', 'c', 'd'}
inv invariant_ServiceLevel6 :
Sequence{Set{1, 2}, Set{2, 3}, Set{4, 5, 6}}->isEmpty()
inv invariant_ServiceLevel13 :
(Sequence{'a', 'b', 'c', 'c', 'd', 'e'}->at(3)) = 'c'
inv invariant_ServiceLevel3 :
Set{1, 2, 3, 4, 5, 6}->isEmpty()
inv invariant_ServiceLevel11 :
(Sequence{'a', 'b', 'c', 'c', 'd', 'e'}->first()) = 'a'
inv invariant_ServiceLevel8 :
((Set{1, 4, 7, 10}) - Set{4, 7}) = Set{1, 10}
inv invariant_ServiceLevel2 :
Set{Set{1, 2}, Set{2, 3}, Set{4, 5, 6}}->isEmpty()
inv invariant_ServiceLevel9 :
((OrderedSet{12, 9, 6, 3}) - Set{1, 3, 2}) = OrderedSet{12, 9, 6}
inv invariant_ServiceLevel14 :
(Sequence{'a', 'b', 'c', 'c', 'd', 'e'}->indexOf('c')) = 3
inv invariant_ServiceLevel15 :
(OrderedSet{'a', 'b', 'c', 'd'}->insertAt(3, 'X')) = OrderedSet{'a', 'b', 'X', 'c', 'd'}
context Transaction
inv invariant_Transaction1 :
self.oclIsKindOf(Transaction) = true
inv invariant_Transaction3 :
self.oclIsTypeOf(Burning) = false
inv invariant_Transaction2 :
self.oclIsTypeOf(Transaction) = true
inv invariant_Transaction4 :
self.oclIsKindOf(Burning) = false
context Transaction::program() : LoyaltyProgram
post: result = self.card.Membership.programs
context LoyaltyAccount
inv invariant_points :
(self.points > 0) implies self.transactions->exists( t : Transaction | t.points > 0 )
inv invariant_transactions :
self.transactions->collect( i_Transaction : Transaction | i_Transaction.points )->exists( p : Integer | p = 500 )
inv invariant_oneOwner :
(self.transactions->collect( i_Transaction : Transaction | i_Transaction.card )->collect( i_CustomerCard : CustomerCard | i_CustomerCard.owner )->asSet()->size()) = 1
context LoyaltyAccount::points : Integer
init :
0
context LoyaltyAccount::totalPointsEarned : Integer
derive :
self.transactions->select( i_Transaction : Transaction | i_Transaction.oclIsTypeOf(Earning) )->collect( i_Transaction : Transaction | i_Transaction.points )->sum()
context LoyaltyAccount::usedServices : Set(Service)
derive :
self.transactions->collect( i_Transaction : Transaction | i_Transaction.generatedBy )->asSet()
context LoyaltyAccount::transactions : Set(Transaction)
init :
Set{}
context LoyaltyAccount::getCustomerName() : String
body: self.Membership.card.owner.name
context LoyaltyAccount::isEmpty() : Boolean
post testPostSuggestedName: result = self.points = 0
pre testPreSuggestedName: true
context ProgramPartner
inv invariant_totalPointsEarning2 :
(self.deliveredServices->collect( i_Service : Service | i_Service.transactions )->select( i_Transaction : Transaction | i_Transaction.oclIsTypeOf(Earning) )->collect( i_Transaction : Transaction | i_Transaction.points )->sum()) < 10000
inv invariant_totalPointsEarning :
(self.deliveredServices->collect( i_Service : Service | i_Service.transactions )->select( i_Transaction : Transaction | i_Transaction.oclIsTypeOf(Earning) )->collect( i_Transaction : Transaction | i_Transaction.points )->sum()) < 10000
inv invariant_nrOfParticipants :
self.numberOfCustomers = self.programs->collect( i_LoyaltyProgram : LoyaltyProgram | i_LoyaltyProgram.participants )->size()
def :
getBurningTransactions() : Set(Transaction) = self.deliveredServices.transactions->iterate(t : Transaction; resultSet : Set( Transaction) = Set{ } | if t.oclIsTypeOf(Burning) then resultSet->including(t) else resultSet endif)
inv invariant_totalPoints :
(self.deliveredServices->collect( i_Service : Service | i_Service.transactions )->collect( i_Transaction : Transaction | i_Transaction.points )->sum()) < 10000
inv invariant_ProgramPartner1 :
self.programs->collect( i_LoyaltyProgram : LoyaltyProgram | i_LoyaltyProgram.partners )->select( p : ProgramPartner | p <> self )->isEmpty()
inv invariant_nrOfParticipants2 :
self.numberOfCustomers = self.programs->collect( i_LoyaltyProgram : LoyaltyProgram | i_LoyaltyProgram.participants )->asSet()->size()
context Burning
inv invariant_Burning5 :
self.oclIsTypeOf(Earning) = false
inv invariant_Burning6 :
self.oclIsKindOf(Earning) = false
inv invariant_Burning4 :
self.oclIsKindOf(Burning) = true
inv invariant_Burning3 :
self.oclIsTypeOf(Burning) = true
inv invariant_Burning2 :
self.oclIsTypeOf(Transaction) = false
inv invariant_Burning1 :
self.oclIsKindOf(Transaction) = true
context TransactionReport
inv invariant_dates :
self.lines->collect( i_TransactionReportLine : TransactionReportLine | i_TransactionReportLine.date )->forAll( d : Date | d.isBefore(self.until) and d.isAfter(self.from) )
inv invariant_cycle :
self.card.transactions->includesAll(self.lines->collect( i_TransactionReportLine : TransactionReportLine | i_TransactionReportLine.transaction ))
context TransactionReport::balance : Integer
derive :
self.card.Membership.account.points
context TransactionReport::totalEarned : Integer
derive :
self.lines->collect( i_TransactionReportLine : TransactionReportLine | i_TransactionReportLine.transaction )->select( i_Transaction : Transaction | i_Transaction.oclIsTypeOf(Earning) )->collect( i_Transaction : Transaction | i_Transaction.points )->sum()
context TransactionReport::totalBurned : Integer
derive :
self.lines->collect( i_TransactionReportLine : TransactionReportLine | i_TransactionReportLine.transaction )->select( i_Transaction : Transaction | i_Transaction.oclIsTypeOf(Burning) )->collect( i_Transaction : Transaction | i_Transaction.points )->sum()
context TransactionReport::number : Integer
derive :
self.card.Membership.account.number
context TransactionReport::name : String
derive :
self.card.owner.name
context CustomerCard
def :
getTotalPoints(d : Date) : Integer = self.transactions->select( i_Transaction : Transaction | i_Transaction.date.isAfter(d) )->collect( i_Transaction : Transaction | i_Transaction.points )->sum()
inv invariant_CustomerCard4 :
self.transactions->select( i_Transaction : Transaction | i_Transaction.points > 100 )->notEmpty()
inv invariant_ofAge :
self.owner.age >= 18
inv invariant_CustomerCard3 :
self.owner.programs->size() > 0
inv invariant_checkDates :
self.validFrom.isBefore(self.goodThru)
--inv invariant_CustomerCard2 :
-- self.owner.dateOfBirth.isBefore(Date::now)
--inv invariant_CustomerCard1 :
-- self.goodThru.isAfter(Date::now)
--inv invariant_THIS :
-- let correctDate : Boolean = self.validFrom.isBefore(Date::now) and self.goodThru.isAfter(Date::now) in if self.valid then
--correctDate = false
--else
--correctDate = true
--endif
context CustomerCard::valid : Boolean
init :
true
context CustomerCard::printedName : String
derive :
self.owner.title.concat(' ').concat(self.owner.name)
context CustomerCard::myLevel : ServiceLevel
derive :
self.Membership.currentLevel
context CustomerCard::transactions : Set(Transaction)
init :
Set{}
context CustomerCard::getTransactions(until:Date, from:Date) : Set(Transaction)
body: self.transactions->select( i_Transaction : Transaction | i_Transaction.date.isAfter(from) and i_Transaction.date.isBefore(until) )
context Membership
def :
getCurrentLevelName() : String = self.currentLevel.name
inv invariant_Membership1 :
(self.account.points >= 0) or self.account->asSet()->isEmpty()
inv invariant_Membership2 :
self.participants.cards->collect( i_CustomerCard : CustomerCard | i_CustomerCard.Membership )->includes(self)
inv invariant_noEarnings :
programs.partners.deliveredServices->forAll(pointsEarned = 0) implies account->isEmpty()
inv invariant_correctCard :
self.participants.cards->includes(self.card)
inv invariant_Membership3 :
self.programs.levels->includes(self.currentLevel)
--inv invariant_noEarnings2 :
-- programs.isSaving implies account->isEmpty()
inv invariant_Membership4 :
self.account->asSet()->isEmpty()
inv invariant_levelAndColor :
((self.currentLevel.name = 'Silver') implies (self.card.color = RandLColor::silver) and self.currentLevel.name = 'Gold') implies self.card.color = RandLColor::gold
inv invariant_Membership5 :
self.programs.levels->includes(self.currentLevel)
context Service
inv invariant_Service5 :
'Anneke'.toUpperCase() = 'ANNEKE'
inv invariant_Service6 :
'Anneke'.toLowerCase() = 'anneke'
inv invariant_Service7 :
('Anneke and Jos'.substring(12, 14)) = 'Jos'
inv invariant_Service4 :
('Anneke '.concat('and Jos')) = 'Anneke and Jos'
inv invariant_Service1 :
(self.pointsEarned > 0) implies not (self.pointsBurned = 0)
inv invariant_Service3 :
('Anneke' = 'Jos') = false
inv invariant_Service2 :
'Anneke'.size() = 6
context Service::upgradePointsEarned(amount:Integer) :
post: self.calcPoints() = self.calcPoints() + amount
context Customer
inv invariant_Customer4 :
self.name = 'Edward'
inv invariant_Customer5 :
self.title = 'Mr.'
inv invariant_Customer10 :
self.programs->collect( i_LoyaltyProgram : LoyaltyProgram | i_LoyaltyProgram.partners )->collectNested( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->isEmpty()
inv invariant_Customer2 :
self.name = 'Edward'
inv invariant_Customer9 :
self.memberships->collect( i_Membership : Membership | i_Membership.account )->reject( i_LoyaltyAccount : LoyaltyAccount | not (i_LoyaltyAccount.points > 0) )->isEmpty()
inv invariant_myInvariant23 :
self.name = 'Edward'
inv invariant_Customer1 :
(self.cards->select( i_CustomerCard : CustomerCard | i_CustomerCard.valid = true )->size()) > 1
inv invariant_Customer7 :
(self.gender = Gender::male) implies self.title = 'Mr.'
inv invariant_Customer11 :
Set{1, 2, 3 }->iterate(i : Integer; sum : Integer = 0 | sum + i) = 0
inv invariant_ANY :
self.memberships->collect( i_Membership : Membership | i_Membership.account )->any( i_LoyaltyAccount : LoyaltyAccount | i_LoyaltyAccount.number < 10000 )->asSet()->isEmpty()
inv invariant_ofAge :
self.age >= 18
inv invariant_sizesAgree :
self.programs->size()
= self.cards
->select( i_CustomerCard : CustomerCard
| i_CustomerCard.valid = true
)
->size()
inv invariant_Customer8 :
self.memberships->collect( i_Membership : Membership | i_Membership.account )->select( i_LoyaltyAccount : LoyaltyAccount | i_LoyaltyAccount.points > 0 )->isEmpty()
inv invariant_Customer6 :
(self.name = 'Edward') and self.title = 'Mr.'
def :
wellUsedCards : Set(CustomerCard) = self.cards->select( i_CustomerCard : CustomerCard | (i_CustomerCard.transactions->collect( i_Transaction : Transaction | i_Transaction.points )->sum()) > 10000 )
inv invariant_Customer3 :
self.name = 'Edward'
def :
initial : String = self.name.substring(1, 1)
inv invariant_Customer12 :
self.programs->size() = self.cards->select( i_CustomerCard : CustomerCard | i_CustomerCard.valid = true )->size()
def :
cardsForProgram(p : LoyaltyProgram) : Sequence(CustomerCard) = p.memberships->collect( i_Membership : Membership | i_Membership.card )
def :
loyalToCompanies : Bag(ProgramPartner) = self.programs->collect( i_LoyaltyProgram : LoyaltyProgram | i_LoyaltyProgram.partners )
context Customer::birthdayHappens() :
post: self.age = self.age + 1
context TransactionReportLine::partnerName : String
derive :
self.transaction.generatedBy.partner.name
context TransactionReportLine::serviceDesc : String
derive :
self.transaction.generatedBy.description
context TransactionReportLine::points : Integer
derive :
self.transaction.points
context TransactionReportLine::amount : Real
derive :
self.transaction.amount
context TransactionReportLine::date : Date
derive :
self.transaction.date
context LoyaltyProgram
inv invariant_LoyaltyProgram18 :
self.participants->forAll( c1 : Customer | self.participants->forAll( c2 : Customer | (c1 <> c2) implies c1.name <> c2.name ) )
inv invariant_LoyaltyProgram1 :
self.levels->includesAll(self.memberships->collect( i_Membership : Membership | i_Membership.currentLevel ))
inv invariant_LoyaltyProgram17 :
self.participants->forAll( c1 : Customer, c2 : Customer | (c1 <> c2) implies c1.name <> c2.name )
inv invariant_LoyaltyProgram14 :
self.memberships->collect( i_Membership : Membership | i_Membership.account )->isUnique( acc : LoyaltyAccount | acc.number )
def :
sortedAccounts : Sequence(LoyaltyAccount) = self.memberships->collect( i_Membership : Membership | i_Membership.account )->sortedBy( i_LoyaltyAccount : LoyaltyAccount | i_LoyaltyAccount.number )
inv invariant_LoyaltyProgram10 :
Sequence{1 .. 10}->isEmpty()
inv invariant_firstLevel :
self.levels->first().name = 'Silver'
inv invariant_LoyaltyProgram8 :
Bag{1, 3, 4, 3, 5}->isEmpty()
inv invariant_knownServiceLevel :
self.levels->includesAll(self.memberships->collect( i_Membership : Membership | i_Membership.currentLevel ))
def :
getServicesByLevel(levelName : String) : Set(Service) = self.levels->select( i_ServiceLevel : ServiceLevel | i_ServiceLevel.name = levelName )->collect( i_ServiceLevel : ServiceLevel | i_ServiceLevel.availableServices )->asSet()
inv invariant_LoyaltyProgram13 :
self.memberships->collect( i_Membership : Membership | i_Membership.account )->isUnique( acc : LoyaltyAccount | acc.number )
inv invariant_minServices :
(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->size()) >= 1
inv invariant_LoyaltyProgram19 :
self.memberships->collect( i_Membership : Membership | i_Membership.account )->one( i_LoyaltyAccount : LoyaltyAccount | i_LoyaltyAccount.number < 10000 )
inv invariant_LoyaltyProgram12 :
self.participants->size() < 10000
inv invariant_LoyaltyProgram7 :
Sequence{'ape', 'nut'}->isEmpty()
inv invariant_LoyaltyProgram11 :
Sequence{1, 2, 3, 4, 5, 6, 7, 8, 9, 10}->isEmpty()
def :
isSaving : Boolean = self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->forAll( i_Service : Service | i_Service.pointsEarned = 0 )
inv invariant_LoyaltyProgram3 :
Set{1, 2, 5, 88}->isEmpty()
inv invariant_LoyaltyProgram2 :
self.levels->exists( i_ServiceLevel : ServiceLevel | i_ServiceLevel.name = 'basic' )
inv invariant_noAccounts :
(self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->forAll( i_Service : Service | (i_Service.pointsEarned = 0) and i_Service.pointsBurned = 0 )) implies self.memberships->collect( i_Membership : Membership | i_Membership.account )->isEmpty()
inv invariant_LoyaltyProgram15 :
self.memberships->collect( i_Membership : Membership | i_Membership.account )->isUnique( i_LoyaltyAccount : LoyaltyAccount | i_LoyaltyAccount.number )
inv invariant_LoyaltyProgram4 :
Set{'apple', 'orange', 'strawberry'}->isEmpty()
inv invariant_LoyaltyProgram6 :
Sequence{1, 3, 45, 2, 3}->isEmpty()
inv invariant_LoyaltyProgram9 :
Sequence{1 .. 6 + 4}->isEmpty()
inv invariant_LoyaltyProgram5 :
OrderedSet{'apple', 'orange', 'strawberry', 'pear'}->isEmpty()
inv invariant_LoyaltyProgram16 :
self.participants->forAll( i_Customer : Customer | i_Customer.age() <= 70 )
context LoyaltyProgram::selectPopularPartners(d:Date) : Set(ProgramPartner)
post: let popularTrans : Set(Transaction) = result->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->collect( i_Service : Service | i_Service.transactions )->asSet() in (popularTrans->forAll( i_Transaction : Transaction | i_Transaction.date.isAfter(d) )) and (popularTrans->select( i_Transaction : Transaction | i_Transaction.amount > 500.00 )->size()) > 20000
context LoyaltyProgram::addService(s:Service, l:ServiceLevel, p:ProgramPartner) :
pre levelsIncludesArgL: self.levels->includes(l)
post servicesIncludesArgS: self.levels->collect( i_ServiceLevel : ServiceLevel | i_ServiceLevel.availableServices )->includes(s)
pre partnersIncludesP: self.partners->includes(p)
post servicesIncludesP: self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->includes(s)
context LoyaltyProgram::getServices(pp:ProgramPartner) : Set(Service)
body: if self.partners->includes(pp) then
pp.deliveredServices
else
Set{}
endif
context LoyaltyProgram::enrollAndCreateCustomer(n : String,
d: Date ) : Customer
post: ((result.oclIsNew() and result.name = n) and result.dateOfBirth = d) and self.participants->includes(result)
pre constantlyTrue: true
context LoyaltyProgram::enroll(c:Customer) : OclVoid
--post: self.memberships->select( m : Membership | m.participants = c )->forAll( i_Membership : Membership | i_Membership.account.asSet()->notEmpty() and i_Membership.account.points = 0 )
post: self.participants = self.participants->including(c)
post: self.participants = self.participants->including(c)
pre: c.name <> ''
pre: c.name <> ''
pre: not self.participants->includes(c)
post: self.participants = self.participants->including(c)
post: self.participants = self.participants->including(c)
pre: not self.participants->includes(c)
--context LoyaltyProgram::addTransaction(accNr: Integer, pName: String, servId: Integer,
-- amnt: Real, d: Date) : OclVoid
--post: let acc : LoyaltyAccount = self.memberships->collect( i_Membership : Membership | i_Membership.account )->select( a : LoyaltyAccount | a.number = accNr )->any( i_LoyaltyAccount : LoyaltyAccount | true ) in let newT : Transaction = self.partners->select( p : ProgramPartner | p.name = pName )->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->select( s : Service | s.serviceNr = servId )->collect( i_Service : Service | i_Service.transactions )->select( i_Transaction : Transaction | (i_Transaction.date = d) and i_Transaction.amount = amnt )->any( i_Transaction : Transaction | true ) in let card : CustomerCard = self.memberships->select( m : Membership | m.account.number = accNr )->collect( i_Membership : Membership | i_Membership.card )->any( i_CustomerCard : CustomerCard | true ) in acc.points = acc.points + newT.points
context LoyaltyProgram::getServices() : Set(Service)
body: self.partners->collect( i_ProgramPartner : ProgramPartner | i_ProgramPartner.deliveredServices )->asSet()
endpackage