Information Technology Reference
In-Depth Information
method is specified as unguarded design. For such a style of modelling and their
formal integration, we refer to our paper [7]. The protocol of use case process a
sale
UC1
is modelled by the sequence diagram in Fig. 6 and its state diagram
is given in Fig. 7.
The specification of the functions of the use case and the component invariant
are given as follows.
Use Case
UC 1: Process Sale
Class
Cashdesk
Method
enableExpress()
pre
:
true
post
:
ExMode' = true
Method
disableExpress()
pre
:
true
post
:
ExMode' = false
Method
startSale()
pre
:
true
post
:/*anew
sale
is created, and its
line items
initialized to empty,
and the date correctly recorded */
sale
=
Sale.New(false/complete, empty/lines, clock.date()/date)
Method
enterItem(Barcode c, int qty)
pre
: /* there exists a product with the input barcode
c
*/
store.catalog
.find(c)
=
null
post
:/*anew
line
is created with its
barcode c
and
quantity qty
*/
line
=
LineItem.New(c/barcode,qty/quantity)
;
line.subtotal
=
store.catalog.
find(
c
)
.price × qty
;
sale.lines
.add(
line
)
Method
finishSale()
pre
:
true
post
:
sale.complete
=
true
∧ sale.total
=
sum
[[
l.subtotal | l ∈ sale.lines
]]
Method
cashPay(double a; double c)
pre:
a ≥ sale.total
post:
sale.pay
=
CashPayment.New(a/amount, a-sale.total/change)
/* the completed
sale
is logged in
store
,and*/
;
store.sales
.add(
sale
); /* the inventory is updated */
∀l ∈ sale.lines,p∈ store.catalog •
(
if
p.barcode
=
l.barcode
then
p.amount
=
p.amount
−
l.quantity
)
Method
cardPay(Card c)
pre
:
Bank.authorize(c,sale.total)
post:
sale.pay
=
CardPayment.New(c/card)
;
store.sales
.add(
sale
);
∀l ∈ sale.lines,p∈ store.catalog •
(
if
p.barcode
=
l.barcode
then
p.amount
=
p.amount − l.quantity
)
invariant
store
=
null
∧
store.catalog
=
null
∧
(
exmode = true
∨
exmode = false
)
The structure of the data and classes of the objects are declared as class decla-
rations in rCOS and can be illustrated by a UML class diagram. Then the state
Search WWH ::
Custom Search