| -------------------------------------------------------------------------------- |
| -- 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 |