class GetraenkeAutomat

types

Money = ℕ

functions

sum : ℕ_{1}-set → ℕ sum (s) \underline{△}

if s = {}

then 0

else let m ∈ s in

m + sum (s \ {m})

types

Coin = one | two | five | ten | twenty | fifty; CoinValues = Coin →^{m} Money

inv cv \underline{△} ∀ c : Coin · c ∈ dom cv

values

WORTH : CoinValues = {

one ↦ 1, two ↦ 2, five ↦ 5, ten ↦ 10, twenty ↦ 20, fifty ↦ 50}

types

Cash = Coin →^{m} ℕ

functions

valueOf : Cash → Money valueOf (ca) \underline{△}

sum ({WORTH (co) × ca (co) | co ∈ dom ca}); numOfCoinsInCash : Cash × Coin → ℕ numOfCoinsInCash (ca, co) \underline{△}

if co ∈ dom ca

then ca (co)

else 0; possibleChanges : Cash → Cash-set possibleChanges (ch) \underline{△}

{c | c : Cash · (dom c ⊆ dom ch) ∧

(∀ c-elem ∈ dom c ·

c (c-elem) ≤ ch (c-elem))};

coinCombinations : Money → Cash-set coinCombinations (m) \underline{△}

{c | c : Cash · valueOf (c) = m}

types

Drink = Tea-or-coffee | chocolate;

Tea-or-coffee :: flavor : tea | coffee
white : 𝔹
sweet : 𝔹;

Ingredient = tea | coffee | chocolate | milk | sugar | water; Prices = Drink →^{m} Money; Stock = Ingredient →^{m} ℕ

inv s \underline{△} ∀ i : Ingredient · i ∈ dom s

values

INGREDIENTS : Drink →^{m} Ingredient-set = {chocolate ↦ {chocolate, water}}⋃^{m}

{d ↦ {d.flavor, water} ∪ (if d.white then {milk} else {}) ∪ (if d.sweet then {sugar} else {}) |

d : Tea-or-coffee}

instance variables

balance : Money := 0; stock : Stock := {i ↦ 0 | i : Ingredient}; cups : ℕ := 0; takings : Cash := {c ↦ 0 | c : Coin}; prices : Prices := {d ↦ 0 | d : Drink};

operations

do-service : Stock × ℕ × Cash × Prices →^{o} () do-service (newStock, newCups, newTakings, newPrices) \underline{△}

is not yet specified

pre balance = 0

post

stock = newStock ∧ cups = newCups ∧ takings = newTakings ∧ prices = newPrices

values

c1 : char^{∗} = "Eine Muenze einwerfen"

operations

insertCoin : Coin →^{o} () insertCoin (c) \underline{△}

is not yet specified

pre true

post

(balance = \begin{matrix}↼− \\ balance \end{matrix} + WORTH (c)) ∧

(takings = \begin{matrix}↼− \\ takings \end{matrix} † \{c ↦ \begin{matrix}↼− \\ takings \end{matrix} (c) + 1\})

values

c2 : char^{∗} = "Getraenke-Auswahlknopf betaetigen"

operations

getDrink : Drink →^{o} Drink getDrink (d) \underline{△}

is not yet specified

pre (balance ≥ prices (d)) ∧ (cups > 0) ∧ (∀ i ∈ INGREDIENTS (d) · stock (i) > 0)

post

(balance = \begin{matrix}↼− \\ balance \end{matrix} − prices (d)) ∧ (cups = \begin{matrix}↼− \\ cups \end{matrix} − 1) ∧

(stock = \begin{matrix}↼− \\ stock \end{matrix}†\{i ↦ \begin{matrix}↼− \\ stock \end{matrix} (i)−1 | i ∈ INGREDIENTS (d)\})∧

(RESULT = d)

values

c3 : char^{∗} = "Restgeld-Auswurfknopf betaetigen"

operations

getChange : () →^{o} Cash getChange () \underline{△}

is not yet specified

pre coinCombinations (balance) ∩ possibleChanges (takings) ≠ {}

post

(RESULT ∈ coinCombinations (balance) ∩ possibleChanges (takings)) ∧ (balance = 0) ∧

(∀ c ∈ dom RESULT · RESULT (c)+takings (c) = \begin{matrix}↼− \\ takings \end{matrix} (c))

end GetraenkeAutomat