royals_and_loyals.ocl

-- 
-- 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.
-- 
-- 
-- SPDX-License-Identifier: BSD-2-Clause
--

----------------------------------------------------------------------
-- Burning
----------------------------------------------------------------------
package RoyalLoyal 
  context Burning 
    inv: self.oclIsKindOf(RoyalLoyal.Transaction) = true 
    inv: self.oclIsTypeOf(RoyalLoyal.Transaction) = false 
    inv: self.oclIsTypeOf(RoyalLoyal.Burning) = true 
    inv: self.oclIsKindOf(RoyalLoyal.Burning) = true 
    inv: self.oclIsTypeOf(RoyalLoyal.Earning) = false 
    inv: self.oclIsKindOf(RoyalLoyal.Earning) = false
endpackage
--
----------------------------------------------------------------------
-- CustomerCard
----------------------------------------------------------------------
package RoyalLoyal

context CustomerCard::valid : Boolean
 init: true                             

context CustomerCard::printedName : String
 derive: owner.title.concat(' ').concat(owner.name)

 context CustomerCard 
   inv checkDates: validFrom.isBefore(validThru)

context CustomerCard 
  inv ofAge: owner.age >= 18

context CustomerCard 
   inv THIS: let correctDate : Boolean = 
  self.validFrom.isBefore(Date::now) and 
  self.validThru.isAfter(Date::now) 
 in 
  if valid then 
 correctDate = false 
 else 
  correctDate = true 
  endif

context CustomerCard 
  def: CustomerCard::getTotalPoints( d: Date ) : Integer 
       = transactions->select( date.isAfter(d) ).points->sum()

context CustomerCard::transactions:Set(Transaction) 
  init: Set{}

Attribute must be classifier-scoped in this context
context CustomerCard 
  inv: validThru.isAfter( Date::now )

context CustomerCard 
  inv: self.owner.dateOfBirth.isBefore( Date::now )

 context CustomerCard 
  inv: self.owner.programs->size() > 0

context CustomerCard 
    inv: self.transactions->select( t: Transaction| t.points > 100 )
                          ->notEmpty()

endpackage
--
----------------------------------------------------------------------
-- Customer 
----------------------------------------------------------------------
package RoyalLoyal

  context Customer
    inv:  not programs->isEmpty()

  context Customer
    inv:   self.age_m() > 21 and self.age_m() < 65 

 context Customer
    inv:   self.age_m() <= 12 xor cards->size() > 3 

 context Customer
   inv:   title = 'Mr.' or title = 'Ms.' 

  context Customer 
    inv ofAge: age >= 18

  context Customer 
    inv:  programs->size() = cards->select(c:CustomerCard|c.valid = true )
                             ->size()


 context Customer::birthdayHappens() : void
   post: age = age@pre + 1

context Customer 
  def: wellUsedCards : Set( CustomerCard ) 
 	= cards->select( transactions.points->sum() > 10000 ) 
  def: loyalToCompanies : Bag( ProgramPartner ) 
  	= programs.partners 
 def: cardsForProgram(p: LoyaltyProgram) : Sequence(CustomerCard) 
      = p.Membership.card
    
  context Customer 
    inv: cards->select( c: CustomerCard| c.valid = true )->size() > 1

  context Customer 
    inv: name = 'Mona'

 context Customer 
   inv: self.name = 'Mona'

 context Customer 
   inv: self.name = 'Mona' 
    inv: self.title = 'Ms.'

 context Customer 
    inv: self.name = 'Mona' and self.title = 'Ms.'

 context Customer 
    inv myInvariant: self.name = 'Mona'

context Customer 
def: initial : String = name.substring(1,1)

 context Customer 
   inv: Membership.account->select(a:LoyaltyAccount| a.points > 0 )
         ->isEmpty()

 context Customer 
   inv: Membership.account->reject( not (points > 0) )->isEmpty() 
   inv ANY: self.Membership.account->any( number < 10000 )->isEmpty()

context Customer
inv: self.programs->collect(lp: LoyaltyProgram | lp.partners) 
                  ->collectNested(deliveredServices )->isEmpty() 

 context Customer
 inv:  Set{1,2,3}->iterate( i: Integer; sum: Integer = 0 | sum + i ) = 0
  
  context Customer 
    inv: programs->size() = cards->select( c: CustomerCard| c.valid = true )
     	 		     ->size()
endpackage
--
----------------------------------------------------------------------
-- LoyaltyAccount
----------------------------------------------------------------------
package RoyalLoyal

context LoyaltyAccount::isEmpty(): Boolean 
  pre : true   
  post: result = (points = 0)

context LoyaltyAccount::points : Integer 
  init: 0

context LoyaltyAccount::transactions : Set(Transaction) 
 init: Set{}

 context LoyaltyAccount::getCustomerName() : String 
   body: Membership.card.owner.name

 context LoyaltyAccount 
  inv oneOwner: transactions.card.owner->asSet()->size() = 1

 context LoyaltyAccount 
   inv: transactions->size() = 1



context LoyaltyAccount::totalPointsEarned : Integer 
  derive: transactions->select( oclIsTypeOf( RoyalLoyal.Earning ) ) 
  .points->sum()

context LoyaltyAccount 
   inv Points: points > 0 
               implies 
               transactions->exists(t:Transaction | t.points > 0)

  context LoyaltyAccount 
   inv Transactions: transactions.points->exists(p : Integer | 
                                                p = 500 )

endpackage
--
----------------------------------------------------------------------
-- LoyaltyProgram
----------------------------------------------------------------------
package RoyalLoyal
context LoyaltyProgram::getServices(): Set(Service) 
  body: partners.deliveredServices->asSet()

context LoyaltyProgram::getServices(pp: ProgramPartner): Set(Service) 
 body: if partners->includes(pp) 
	  then pp.deliveredServices 
        else Set{} 
	 	endif

context LoyaltyProgram 
 def: getServicesByLevel(levelName: String): Set(Service) 
 = levels->select( name = levelName ).availableServices->asSet()

context LoyaltyProgram 
inv knownServiceLevel: levels->includesAll(Membership.currentLevel)

context LoyaltyProgram 
  inv minServices: partners.deliveredServices ->size() >= 1


 context LoyaltyProgram 
   inv noAccounts: partners.deliveredServices->forAll( 
			  pointsEarned = 0 and pointsBurned = 0 ) 
				  implies Membership.account->isEmpty() 


context LoyaltyProgram 
 inv : levels->first() = levels->first()
 inv firstLevel: levels->first().name = 'Silver'

 context LoyaltyProgram::enroll(c : Customer) : Boolean
   pre : c.name <> '' 

  context LoyaltyProgram::enroll(c : Customer) : Boolean
    post: participants = participants@pre->including( c ) 


context LoyaltyProgram::addTransaction( accNr: Integer, 
 	pName: String, servId: Integer, amnt: Real, 
	d: Date ) : Boolean
  post: let acc : LoyaltyAccount = 
				  Membership.account->select( a | a.number = accNr )->any(true), 
			newT : Transaction = 
				  partners-> select(p | p.name = pName).deliveredServices 
					  ->select(s | s.serviceNr = servId).transactions 
						  ->select( date = d and amount = amnt )->any(true), 
			card : CustomerCard = 
				  Membership->select( m | m.account.number = accNr ).card->any(true)
	    in acc.points = acc.points@pre + newT.points and 
		   newT.oclIsNew() and 
		   amnt = 0 implies newT.oclIsTypeOf( Burning ) and 
		   amnt > 0 implies newT.oclIsTypeOf( Earning ) and 
		   acc.transactions - acc.transactions@pre = Set{ newT } and 
		   card.transactions - card.transactions@pre = Set{ newT } 
 
context LoyaltyProgram 
  def: isSaving : Boolean = 
	partners.deliveredServices->forAll(pointsEarned = 0)

 context LoyaltyProgram 
  inv: partners.deliveredServices->forAll(s:Service| 
                                          s.pointsEarned = 0) 
	   and 
	   Membership.card->forAll(c:CustomerCard| 
			c.validThru = Date::fromYMD(2000,1,1)) 
	   and 
	   participants->forAll(c:Customer| c.age_m() > 55)

  context LoyaltyProgram 
    inv: partners.deliveredServices->forAll(s: Service| 
                                   s.pointsEarned = 0) 
     inv: participants->forAll(p:Customer | p.age_m() > 55)

context LoyaltyProgram::selectPopularPartners( d: Date )
                                         : Set(ProgramPartner) 
  post: let popularTrans : Set(Transaction) = 
 			result.deliveredServices.transactions->asSet()
		in 
	  popularTrans->forAll( date.isAfter(d) ) and 
	  popularTrans->select( amount > 500.00e1 )->size() > 20000


 context LoyaltyProgram::enroll(c : Customer):Boolean 
   pre : not participants->includes(c) 

 context LoyaltyProgram::enroll(c : Customer):Boolean 
   post: participants = participants@pre->including(c)

context LoyaltyProgram 
  inv: levels->includesAll( Membership.currentLevel ) 

  context LoyaltyProgram 
    inv: self.levels->exists(sl:ServiceLevel| sl.name = 'basic')

  context LoyaltyProgram
  inv testSET:  Set { 1 , 2 , 5 , 88 } ->isEmpty()
    inv:  Set { 'apple' , 'orange', 'strawberry' } ->isEmpty()
    inv:  Sequence { 1, 3, 45, 2, 3 } ->isEmpty()
    inv:  Sequence { 'ape', 'nut' } ->isEmpty()
    inv:  Bag {1 , 3 , 4, 3, 5 } ->isEmpty()
    inv:  Sequence{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 } ->isEmpty()

 context LoyaltyProgram
   inv:  Sequence{ 1..(6 + 4) } ->isEmpty()
   inv:  Sequence{ 1..10 } ->isEmpty()

  context LoyaltyProgram 
    inv: self.participants->size() < 10000

context LoyaltyProgram 
  inv: self.Membership.account
              ->isUnique( acc: LoyaltyAccount | acc.number )

context LoyaltyProgram 
  def: sortedAccounts : Sequence(LoyaltyAccount) = 
       self.Membership.account->sortedBy( number )

context LoyaltyProgram 
  inv: participants->forAll( c:Customer | c.age_m() <= 70 )

context LoyaltyProgram 
  inv: self.participants->forAll(c1 : Customer, c2:Customer | 
       c1 <> c2 implies c1.name <> c2.name)

context LoyaltyProgram 
  inv: self.participants->forAll( c1 : Customer| 
       self.participants->forAll( c2 : Customer | 
         c1 <> c2 implies c1.name <> c2.name ))

context LoyaltyProgram 
  inv: self.Membership.account->one( number < 10000 ) 

 context LoyaltyProgram::enroll(c : Customer):Boolean
  pre : not (participants->includes(c)) 

 context LoyaltyProgram::enroll(c : Customer):Boolean
   post: participants = participants@pre->including(c) 

 context LoyaltyProgram::enroll(c : Customer):Boolean
  post: Membership->select(m : Membership | m.participants = c)-> 
        forAll( account->notEmpty() and 
         account.points = 0 and 
         account.transactions->isEmpty() )

endpackage
--
----------------------------------------------------------------------
-- Membership
----------------------------------------------------------------------
package RoyalLoyal

context Membership 
 inv correctCard: participants.cards->includes(self.card)

context Membership 
  def : getCurrentLevelName() : String = currentLevel.name

context Membership 
 inv levelAndColor: 
 currentLevel.name = 'Silver' implies card.color = Color::silver
 and 
 currentLevel.name = 'Gold' implies card.color = Color::gold

context Membership 
 inv noEarnings: programs.partners.deliveredServices 
              ->forAll(pointsEarned = 0) implies account
                           ->isEmpty()

context Membership 
 inv noEarnings2: programs.isSaving 
     implies account->isEmpty()

 context Membership 
   inv: account.points >= 0 or account->isEmpty()

context Membership 
  inv: participants.cards.Membership->includes( self )

context Membership 
inv: programs.levels->includes( currentLevel )

 context Membership 
  inv: account->isEmpty() 

context Membership 
 inv: programs.levels ->includes(currentLevel)

endpackage
--
----------------------------------------------------------------------
-- ProgramPartner
----------------------------------------------------------------------
package RoyalLoyal

 context ProgramPartner 
 inv nrOfParticipants: numberOfCustomers = programs.participants->size()
 inv:  numberOfCustomers = programs->collect(p:LoyaltyProgram| p.participants)
                           ->size()

  context ProgramPartner 
  inv nrOfParticipants2: 
  numberOfCustomers = programs.participants->asSet()->size()

 context ProgramPartner 
   inv totalPoints: 
   deliveredServices.transactions.points->sum() < 10000

context ProgramPartner 
  inv:  deliveredServices->collect(s:Service| s.transactions)
               ->select(t:Transaction|t.oclIsTypeOf(RoyalLoyal.Earning))
      		       ->collect(t:Transaction|t.points)->size()>0


  /* the following invariant states that the maximum number of points 
  that may be earned by all services of a program partner is equal 
  to 10,000 
  */
  context ProgramPartner 
    inv totalPointsEarning2: 
    deliveredServices.transactions -- all transactions 
    ->select(t:Transaction|t.oclIsTypeOf(RoyalLoyal.Earning) ) -- select earning ones 
    .points->sum() -- sum all points 
    < 10000 -- sum smaller than 10,000

   context ProgramPartner 
     inv: self.programs.partners->select(p : ProgramPartner | p <> self)
             ->isEmpty()

context ProgramPartner 
  def: getBurningTransactions(): Set(Transaction) = 
  self.deliveredServices.transactions->iterate( 
				  t : Transaction; 
				  resultSet : Set(Transaction) = Set{} | 
					  if t.oclIsTypeOf( RoyalLoyal.Burning ) then 
					  	resultSet->including( t ) 
					  else 
					  	resultSet 
					  endif 
       			  )

endpackage
--
----------------------------------------------------------------------
-- ServiceLevel
----------------------------------------------------------------------
package RoyalLoyal

context ServiceLevel 
 inv: program.partners ->isEmpty()
inv: Set { Set { 1, 2 }, Set { 2, 3 }, Set { 14, 5, 6 } } ->isEmpty()
  inv: Set { 1, 2, 3, 4, 5, 6 } ->isEmpty()
inv: Bag { Set { 1, 2 }, Set { 1, 2 }, Set { 4, 5, 6 } } ->isEmpty()
  inv:  Bag { 1, 1, 2, 2, 4, 5, 6 } ->isEmpty()
inv: Sequence { Set { 1, 2 }, Set { 2, 3 }, Set { 4, 5, 6 } } ->isEmpty()
  inv: Sequence { 2, 1, 2, 3, 5, 6, 4 } ->isEmpty()
  inv: Set{1,4,7,10} - Set{4,7} = Set{1,10} 
  inv: Set{1,4,7,10}->symmetricDifference(Set{4,5,7}) = Set{1,5,10} 
  inv: Sequence{'a','b','c','c','d','e'}->first() = 'a' 
  inv: Sequence{'a','b','c','c','d','e'}->at( 3 ) = 'c' 
  inv: Sequence{'a','b','c','c','d','e'}->indexOf( 'c' ) = 3 
  inv: Sequence{'a','b','c','c','d','e'}->subSequence( 3, 5 ) = 
	Sequence{'c','c','d'} 
  inv: Sequence{'a','b','c','c','d','e'}->append( 'X' ) = 
			Sequence{'a','b','c','c','d','e','X'} 
  inv: Sequence{'a','b','c','c','d','e'}->prepend( 'X' ) = 
			Sequence{'X','a','b','c','c','d','e'}

et{12,9,6,3} - Set{1,3,2} = OrderedSet{12,9,6} 
inv: OrderedSet{'a','b','c','d'}->last() = 'd' 
inv: OrderedSet{'a','b','c','d'}->insertAt( 3, 'X' ) = 
 					       OrderedSet{'a','b','X','c','d'} 
inv: OrderedSet{'a','b','c','d'}->subOrderedSet( 2, 3 ) = 
			OrderedSet{'b','c'} 
endpackage
--
----------------------------------------------------------------------
-- Service 
----------------------------------------------------------------------
package RoyalLoyal
  context Service::upgradePointsEarned(amount: Integer): void 
  post: self.calcPoints() = self@pre.calcPoints() + amount
  
context Service 
  inv: self.pointsEarned > 0 implies not (self.pointsBurned = 0) 
  inv: not true 
  inv:   description = 'Foobar' 
  inv:   512 * 2 + 3 =  1027 
  inv:   2654 * 4.3 + 101 = 11513.2 
  inv:  2654 * 4.3e1 + 101 = 11513.2e1 
  inv:   (3.2).floor() / 3 = 1 
  inv:   (3.2e1).floor() / 3 = 1 
  inv:   1.175 * (-8.9).abs() - 10 = 0.4575 
  inv:   1.175e1 * (-8.9e1).abs() - 10 = 0.4575e1 
  inv:   (12 > 22.7) = false  
  inv:   12.max(33) = 33 
  inv:   33.max(12) = 33 
  inv:   13.mod(2)  = 1 
  inv:   13.div(2)  = 6 
  inv:   33.7.min(12) = 12.0 
  inv:   -24.abs() = 24 
  inv: (-2.4).floor() = -3 
  inv:  (2.4).floor() = 2 
  inv:   'Isabelle'.size() = 9 
  inv:   ('Isabelle' = 'HOL-OCL') = false 
  inv:   'Isabelle'.concat('/HOL-OCL') = 'Isabelle/HOL-OCL' 
  inv:   'Isabelle/HOL-OCL'.toUpper() = 'ISABELLE/HOL-OCL' 
  inv:   'Isabelle/HOL-OCL'.toLower() = 'isabelle/hol-ocl' 
  inv:   'Isabelle/HOL-OCL'.substring(1, 13) = 'Isabelle/HOL'
endpackage
--
----------------------------------------------------------------------
-- Transaction 
----------------------------------------------------------------------
package RoyalLoyal

-- Navigation over path expressions/association class
context Transaction::program() : LoyaltyProgram 
  post: result = self.card.membership.programs

  context Transaction 
    inv: self.oclIsKindOf(RoyalLoyal.Transaction) = true 
    inv: self.oclIsTypeOf(RoyalLoyal.Transaction) = true 
    inv: self.oclIsTypeOf(RoyalLoyal.Burning) = false 
    inv: self.oclIsKindOf(RoyalLoyal.Burning) = false

endpackage