Harnessing rCOS for Tool Support—The CoCoME Experience - Formal Methods and Hybrid Real-Time Systems - page 103

<< Inventory >>

CashDeskIf

ManageIf

<< Application >>

OrderIf

StoreIf

<< Data >>

:Store

1

*

sale

*

order

*

cat

:Sale
complete: Boolean
total: Double
date: Date

:Order
complete: Boolean

:Item
barcode: Long
price. Double
amount: Long

pay

1 0..1

1

lines :Payment

*

:LineItem
barcode: Long
quantity: Long
subtotal: Double

:CashPa y ment
amount: Double
change: Double

:CardPayment
card: Card

JDBC

<< DataBase >>

Fig. 12. The components of Inventory

Significant algorithms for specifications of methods of classes are designed.
Such a method usually does not need to call methods outside its owning class.
The specification of such a algorithms often uses quantifications over elements
of a multi-object (or a container object). In rCOS, this is resolved through stan-
dard patterns like iteration. The correctness of those patterns has been formally
proved in previous rCOS literature.
This representation allows almost direct translation into Java. We invite the
reader to observe the introduction of the intermediate classes which finally break
down the store.catalog.find() in class Cashdesk down to the set -implementation,
which is given again as a purely functional specification, under the assumption
that a corresponding data structure is available in the target language:

class Cashdesk :: enterItem(Barcode code, int qty) {
if find(code) = null then {
line := LineItem.New(code, qty) ;
line.setSubtotal(find(code).price × qty) ;
sale.addLine(line) }
else { throw exception e }}
find(Barcode code; Product r) { r:= store.find(code)}
class Store :: find(Barcode code; Product r) { r:= catalog.find(code)}
class set(Product) :: find(Barcode code; Product returns)
Pre ∃p : Product • ( p.barcode = code ∧ contains ( p ))
Post returns.barcode' = code

class Sale ::

addLine(LineItem l) {lines.add(l)}

class LineItem ::

setSubtotal(double a) {subtotal :=a }

class Cashdesk :: finishSale()

{ sale.setComplete() ; sale.setTotal() }

class Sale ::

setComplete() { complete := true }
setTotal() { total:= lines.sum() }