545 lines
17 KiB
Plaintext
545 lines
17 KiB
Plaintext
--
|
|
-- 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
|