Added the famous royals and loyals example.
This commit is contained in:
parent
84edb3fbb7
commit
dd01af52d4
|
|
@ -0,0 +1,9 @@
|
|||
# The Royals and Loyals
|
||||
The famous royals-and-loyals example from the OCL book.
|
||||
|
||||
## Data Sheet
|
||||
* Format: ArgoUML 0.26
|
||||
* Language: UML/OCL
|
||||
|
||||
For further information (license, citation, etc.), please look at the [README.md](../README.md)
|
||||
of the main directory.
|
||||
|
|
@ -0,0 +1,545 @@
|
|||
--
|
||||
-- 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.
|
||||
--
|
||||
----------------------------------------------------------------------
|
||||
-- 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
|
||||
|
||||
-- [Derive] context CustomerCard::printedName : String
|
||||
-- [Derive] derive: owner.title.concat(' ').concat(owner.name)
|
||||
|
||||
context CustomerCard
|
||||
inv checkDates: validFrom.isBefore(validThru)
|
||||
|
||||
context CustomerCard
|
||||
inv ofAge: owner.age >= 18
|
||||
|
||||
-- [ASTGen] Attribute must be classifier-scoped in this context
|
||||
-- [ASTGen] context CustomerCard
|
||||
-- [ASTGen] inv THIS: let correctDate : Boolean =
|
||||
-- [ASTGen] self.validFrom.isBefore(Date::now) and
|
||||
-- [ASTGen] self.validThru.isAfter(Date::now)
|
||||
-- [ASTGen] in
|
||||
-- [ASTGen] if valid then
|
||||
-- [ASTGen] correctDate = false
|
||||
-- [ASTGen] else
|
||||
-- [ASTGen] correctDate = true
|
||||
-- [ASTGen] endif
|
||||
|
||||
-- [Def] context CustomerCard
|
||||
-- [Def] def: CustomerCard::getTotalPoints( d: Date ) : Integer
|
||||
-- [Def] = transactions->select( date.isAfter(d) ).points->sum()
|
||||
|
||||
-- [ASTGen] context CustomerCard::transactions:Set(Transaction)
|
||||
-- [ASTGen] init: Set{}
|
||||
|
||||
-- [ASTGen] Attribute must be classifier-scoped in this context
|
||||
-- [ASTGen] context CustomerCard
|
||||
-- [ASTGen] inv: validThru.isAfter( Date::now )
|
||||
|
||||
-- [ASTGen] context CustomerCard
|
||||
-- [ASTGen] 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
|
||||
|
||||
-- [Def] context Customer
|
||||
-- [Def] def: wellUsedCards : Set( CustomerCard )
|
||||
-- [Def] = cards->select( transactions.points->sum() > 10000 )
|
||||
-- [Def] def: loyalToCompanies : Bag( ProgramPartner )
|
||||
-- [Def] = programs.partners
|
||||
-- [Def] def: cardsForProgram(p: LoyaltyProgram) : Sequence(CustomerCard)
|
||||
-- [Def] = 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'
|
||||
|
||||
-- [Def] context Customer
|
||||
-- [Def] def: initial : String = name.substring(1,1)
|
||||
|
||||
-- Association Class:
|
||||
-- [Enc/XMI] context Customer
|
||||
-- [Enc/XMI] inv: Membership.account->select(a:LoyaltyAccount| a.points > 0 )
|
||||
-- [Enc/XMI] ->isEmpty()
|
||||
|
||||
-- Association Class:
|
||||
-- [Enc/XMI] context Customer
|
||||
-- [Enc/XMI] inv: Membership.account->reject( not (points > 0) )->isEmpty()
|
||||
-- [Enc/XMI] inv ANY: self.Membership.account->any( number < 10000 )->isEmpty()
|
||||
|
||||
-- [AstGen] context Customer
|
||||
-- [AstGen] inv: self.programs->collect(lp: LoyaltyProgram | lp.partners)
|
||||
-- [AstGen] ->collectNested(deliveredServices )->isEmpty()
|
||||
|
||||
-- [Enc/XMI] context Customer
|
||||
-- [Enc/XMI] 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
|
||||
|
||||
-- [AstGen] context LoyaltyAccount::transactions : Set(Transaction)
|
||||
-- [AstGen] 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
|
||||
|
||||
|
||||
|
||||
-- [Derive] context LoyaltyAccount::totalPointsEarned : Integer
|
||||
-- [Derive] derive: transactions->select( oclIsTypeOf( RoyalLoyal.Earning ) )
|
||||
-- [Derive] .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
|
||||
-- [returns_coll] context LoyaltyProgram::getServices(): Set(Service)
|
||||
-- [returns_coll] body: partners.deliveredServices->asSet()
|
||||
|
||||
-- [returns_coll] context LoyaltyProgram::getServices(pp: ProgramPartner): Set(Service)
|
||||
-- [returns_coll] body: if partners->includes(pp)
|
||||
-- [returns_coll] then pp.deliveredServices
|
||||
-- [returns_coll] else Set{}
|
||||
-- [returns_coll] endif
|
||||
|
||||
-- [Def] context LoyaltyProgram
|
||||
-- [Def] def: getServicesByLevel(levelName: String): Set(Service)
|
||||
-- [Def] = levels->select( name = levelName ).availableServices->asSet()
|
||||
|
||||
-- [Enc/XMI] context LoyaltyProgram
|
||||
-- [Enc/XMI] inv knownServiceLevel: levels->includesAll(Membership.currentLevel)
|
||||
|
||||
context LoyaltyProgram
|
||||
inv minServices: partners.deliveredServices ->size() >= 1
|
||||
|
||||
|
||||
-- [Enc/XMI] context LoyaltyProgram
|
||||
-- [Enc/XMI] inv noAccounts: partners.deliveredServices->forAll(
|
||||
-- [Enc/XMI] pointsEarned = 0 and pointsBurned = 0 )
|
||||
-- [Enc/XMI] 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 )
|
||||
|
||||
|
||||
--[Enc/XMI] context LoyaltyProgram::addTransaction( accNr: Integer,
|
||||
--[Enc/XMI]y pName: String, servId: Integer, amnt: Real,
|
||||
--[Enc/XMI] d: Date ) : Boolean
|
||||
--[Enc/XMI] post: let acc : LoyaltyAccount =
|
||||
--[Enc/XMI] Membership.account->select( a | a.number = accNr )->any(true),
|
||||
--[Enc/XMI] newT : Transaction =
|
||||
--[Enc/XMI] partners-> select(p | p.name = pName).deliveredServices
|
||||
--[Enc/XMI] ->select(s | s.serviceNr = servId).transactions
|
||||
--[Enc/XMI] ->select( date = d and amount = amnt )->any(true),
|
||||
--[Enc/XMI] card : CustomerCard =
|
||||
--[Enc/XMI] Membership->select( m | m.account.number = accNr ).card->any(true)
|
||||
--[Enc/XMI] in acc.points = acc.points@pre + newT.points and
|
||||
--[Enc/XMI] newT.oclIsNew() and
|
||||
--[Enc/XMI] amnt = 0 implies newT.oclIsTypeOf( Burning ) and
|
||||
--[Enc/XMI] amnt > 0 implies newT.oclIsTypeOf( Earning ) and
|
||||
--[Enc/XMI] acc.transactions - acc.transactions@pre = Set{ newT } and
|
||||
--[Enc/XMI] card.transactions - card.transactions@pre = Set{ newT }
|
||||
|
||||
-- [Def] context LoyaltyProgram
|
||||
-- [Def] def: isSaving : Boolean =
|
||||
-- [Def] partners.deliveredServices->forAll(pointsEarned = 0)
|
||||
|
||||
-- [ASTGen] expected operation 'fromYMD inside Classifier Date to be a class operation (not instance level)
|
||||
-- [ASTGen] context LoyaltyProgram
|
||||
-- [ASTGen] inv: partners.deliveredServices->forAll(s:Service|
|
||||
-- [ASTGen] s.pointsEarned = 0)
|
||||
-- [ASTGen] and
|
||||
-- [ASTGen] Membership.card->forAll(c:CustomerCard|
|
||||
-- [ASTGen] c.validThru = Date::fromYMD(2000,1,1))
|
||||
-- [ASTGen] and
|
||||
-- [ASTGen] 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)
|
||||
|
||||
-- [Model] context LoyaltyProgram::selectPopularPartners( d: Date )
|
||||
-- [Model] : Set(ProgramPartner)
|
||||
-- [Model] post: let popularTrans : Set(Transaction) =
|
||||
-- [Model] result.deliveredServices.transactions->asSet()
|
||||
-- [Model] in
|
||||
-- [Model] popularTrans->forAll( date.isAfter(d) ) and
|
||||
-- [Model] 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)
|
||||
|
||||
-- [Enc/XMI] context LoyaltyProgram
|
||||
-- [Enc/XMI] inv: levels->includesAll( Membership.currentLevel )
|
||||
|
||||
context LoyaltyProgram
|
||||
inv: self.levels->exists(sl:ServiceLevel| sl.name = 'basic')
|
||||
|
||||
-- [Enc/XMI] context LoyaltyProgram
|
||||
-- [Enc/XMI] inv testSET: Set { 1 , 2 , 5 , 88 } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Set { 'apple' , 'orange', 'strawberry' } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Sequence { 1, 3, 45, 2, 3 } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Sequence { 'ape', 'nut' } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Bag {1 , 3 , 4, 3, 5 } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Sequence{ 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 } ->isEmpty()
|
||||
|
||||
-- [Enc/XMI] context LoyaltyProgram
|
||||
-- [Enc/XMI] inv: Sequence{ 1..(6 + 4) } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Sequence{ 1..10 } ->isEmpty()
|
||||
|
||||
context LoyaltyProgram
|
||||
inv: self.participants->size() < 10000
|
||||
|
||||
-- [Enc/XMI] context LoyaltyProgram
|
||||
-- [Enc/XMI] inv: self.Membership.account
|
||||
-- [Enc/XMI] ->isUnique( acc: LoyaltyAccount | acc.number )
|
||||
|
||||
-- [Def] context LoyaltyProgram
|
||||
-- [Def] def: sortedAccounts : Sequence(LoyaltyAccount) =
|
||||
-- [Def] 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 ))
|
||||
|
||||
-- [Enc/XMI] context LoyaltyProgram
|
||||
-- [Enc/XMI] 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)
|
||||
|
||||
-- [Model-AssocClass] context LoyaltyProgram::enroll(c : Customer):Boolean
|
||||
-- [Model-AssocClass] post: Membership->select(m : Membership | m.participants = c)->
|
||||
-- [Model-AssocClass] forAll( account->notEmpty() and
|
||||
-- [Model-AssocClass] account.points = 0 and
|
||||
-- [Model-AssocClass] account.transactions->isEmpty() )
|
||||
|
||||
endpackage
|
||||
--
|
||||
----------------------------------------------------------------------
|
||||
-- Membership
|
||||
----------------------------------------------------------------------
|
||||
package RoyalLoyal
|
||||
|
||||
-- [Model-AssocClass] context Membership
|
||||
-- [Model-AssocClass] inv correctCard: participants.cards->includes(self.card)
|
||||
|
||||
-- [Def] context Membership
|
||||
-- [Def] def : getCurrentLevelName() : String = currentLevel.name
|
||||
|
||||
-- [Model-Enum] context Membership
|
||||
-- [Model-Enum] inv levelAndColor:
|
||||
-- [Model-Enum] currentLevel.name = 'Silver' implies card.color = Color::silver
|
||||
-- [Model-Enum] and
|
||||
-- [Model-Enum] currentLevel.name = 'Gold' implies card.color = Color::gold
|
||||
|
||||
-- [Model-AssocClass] context Membership
|
||||
-- [Model-AssocClass] inv noEarnings: programs.partners.deliveredServices
|
||||
-- [Model-AssocClass] ->forAll(pointsEarned = 0) implies account
|
||||
-- [Model-AssocClass] ->isEmpty()
|
||||
|
||||
-- [Model-AssocClass] context Membership
|
||||
-- [Model-AssocClass] inv noEarnings2: programs.isSaving
|
||||
-- [Model-AssocClass] implies account->isEmpty()
|
||||
|
||||
context Membership
|
||||
inv: account.points >= 0 or account->isEmpty()
|
||||
|
||||
-- [Model-AssocClass] context Membership
|
||||
-- [Model-AssocClass] inv: participants.cards.Membership->includes( self )
|
||||
|
||||
-- [Model-AssocClass] context Membership
|
||||
-- [Model-AssocClass] inv: programs.levels->includes( currentLevel )
|
||||
|
||||
context Membership
|
||||
inv: account->isEmpty()
|
||||
|
||||
-- [Model-AssocClass] context Membership
|
||||
-- [Model-AssocClass] 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()
|
||||
|
||||
-- [Def] context ProgramPartner
|
||||
-- [Def] def: getBurningTransactions(): Set(Transaction) =
|
||||
-- [Def] self.deliveredServices.transactions->iterate(
|
||||
-- [Def] t : Transaction;
|
||||
-- [Def] resultSet : Set(Transaction) = Set{} |
|
||||
-- [Def] if t.oclIsTypeOf( RoyalLoyal.Burning ) then
|
||||
-- [Def] resultSet->including( t )
|
||||
-- [Def] else
|
||||
-- [Def] resultSet
|
||||
-- [Def] endif
|
||||
-- [Def] )
|
||||
|
||||
endpackage
|
||||
--
|
||||
----------------------------------------------------------------------
|
||||
-- ServiceLevel
|
||||
----------------------------------------------------------------------
|
||||
package RoyalLoyal
|
||||
|
||||
context ServiceLevel
|
||||
inv: program.partners ->isEmpty()
|
||||
-- [AstGen] inv: Set { Set { 1, 2 }, Set { 2, 3 }, Set { 14, 5, 6 } } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Set { 1, 2, 3, 4, 5, 6 } ->isEmpty()
|
||||
-- [AstGen] inv: Bag { Set { 1, 2 }, Set { 1, 2 }, Set { 4, 5, 6 } } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Bag { 1, 1, 2, 2, 4, 5, 6 } ->isEmpty()
|
||||
-- [AstGen] inv: Sequence { Set { 1, 2 }, Set { 2, 3 }, Set { 4, 5, 6 } } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Sequence { 2, 1, 2, 3, 5, 6, 4 } ->isEmpty()
|
||||
-- [Enc/XMI] inv: Set{1,4,7,10} - Set{4,7} = Set{1,10}
|
||||
-- [Enc/XMI] inv: Set{1,4,7,10}->symmetricDifference(Set{4,5,7}) = Set{1,5,10}
|
||||
-- [Enc/XMI] inv: Sequence{'a','b','c','c','d','e'}->first() = 'a'
|
||||
-- [Enc/XMI] inv: Sequence{'a','b','c','c','d','e'}->at( 3 ) = 'c'
|
||||
-- [Enc/XMI] inv: Sequence{'a','b','c','c','d','e'}->indexOf( 'c' ) = 3
|
||||
-- [Enc/XMI] inv: Sequence{'a','b','c','c','d','e'}->subSequence( 3, 5 ) =
|
||||
-- [Enc/XMI] Sequence{'c','c','d'}
|
||||
-- [Enc/XMI] inv: Sequence{'a','b','c','c','d','e'}->append( 'X' ) =
|
||||
-- [Enc/XMI] Sequence{'a','b','c','c','d','e','X'}
|
||||
-- [Enc/XMI] inv: Sequence{'a','b','c','c','d','e'}->prepend( 'X' ) =
|
||||
-- [Enc/XMI] Sequence{'X','a','b','c','c','d','e'}
|
||||
--
|
||||
-- Dresden-OCL does not implement OrderedSets ...
|
||||
-- [OrderedSet] inv: OrderedSet{12,9,6,3} - Set{1,3,2} = OrderedSet{12,9,6}
|
||||
-- [OrderedSet] inv: OrderedSet{'a','b','c','d'}->last() = 'd'
|
||||
-- [OrderedSet] inv: OrderedSet{'a','b','c','d'}->insertAt( 3, 'X' ) =
|
||||
-- [OrderedSet] OrderedSet{'a','b','X','c','d'}
|
||||
-- [OrderedSet] inv: OrderedSet{'a','b','c','d'}->subOrderedSet( 2, 3 ) =
|
||||
-- [OrderedSet] 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
|
||||
-- [Model-AssocClass] context Transaction::program() : LoyaltyProgram
|
||||
-- [Model-AssocClass] 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
|
||||
Binary file not shown.
Binary file not shown.
Reference in New Issue