blob: 154a1fa842a75552ee4a0f12bbaed8eec484af4e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
|
note
description: "Summary description for {ACCOUNT}."
author: ""
date: "$Date$"
revision: "$Revision$"
class
ACCOUNT
create
make
-- TODO
-- interest should defined by bank (via make?)
-- add more checks to invariant (like balance >= creditline) ?
-- check if balance is a getter and not a setter (doesn't has an assign)
-- + check if authorized_signers is a getter and not a setter (it doesn't has an assign)
-- -> if not: add a getter (via Result or so..) and move them to {NONE}
-- much other stuff to test like: lower creditline so that balance will be invalid
feature -- Access
transfer_minamount: REAL_64 assign set_transfer_minamount
-- Mindestbetrag für jede Einzahlung, Auszahlung und Überweisung
authorized_signers: ARRAYED_SET [PERSON]
-- Zeichnungsberechtigte
attribute Result := ({like authorized_signers}).default end --| Remove line when Void Safety is properly set
creditline: REAL_64 assign set_creditline
-- Kreditrahmen
interest_deposit: REAL_64 assign set_interest_deposit
-- Habenverzinsung
interest_debit: REAL_64 assign set_interest_debit
-- Sollverzinsung
balance: REAL_64
-- Kontostand
feature {NONE} -- Initialization
make (an_authorized_signer: PERSON)
do
create authorized_signers.make(1)
add_authorized_signer (an_authorized_signer)
transfer_minamount := 2
balance := 0
end
feature -- Basic operations
deposit (an_amount: like transfer_minamount)
require
an_amount_positive: an_amount > 0.0
transfer_minamount_ok: an_amount >= transfer_minamount
do
balance := balance + an_amount
ensure
balance_increased: balance > old balance
deposited: balance = old balance + an_amount
end
withdraw (an_amount: like transfer_minamount)
require
an_amount_positive: an_amount > 0.0
transfer_minamount_ok: an_amount >= transfer_minamount
do
balance := balance - an_amount
ensure
balance_decreased: balance < old balance
withdrawed: balance = old balance - an_amount
creditline_ok: balance >= creditline
end
transfer(an_amount: like transfer_minamount; an_account: like Current)
require
an_amount_positive: an_amount > 0.0
transfer_minamount_ok: an_amount >= transfer_minamount
an_account_attached: an_account /= Void
do
withdraw (an_amount)
an_account.deposit (an_amount)
end
add_authorized_signer (an_authorized_signer: PERSON)
require
an_authorized_signer_attached: an_authorized_signer /= Void
an_authorized_signer_notinlist: not authorized_signers.has (an_authorized_signer)
do
authorized_signers.put (an_authorized_signer)
ensure
authorized_signers_assigned: authorized_signers.has (an_authorized_signer)
end
remove_authorized_signer (an_authorized_signer: PERSON)
require
an_authorized_signer_attached: an_authorized_signer /= Void
an_authorized_signer_inlist: authorized_signers.has (an_authorized_signer)
authorized_signers_never_empty: authorized_signers.count >= 2
do
authorized_signers.prune (an_authorized_signer)
ensure
authorized_signers_assigned: not authorized_signers.has (an_authorized_signer)
end
feature {NONE} -- Implementation
set_transfer_minamount (a_transfer_minamount: like transfer_minamount)
-- Assign `transfer_minamount' with `a_transfer_minamount'.
require
a_transfer_minamount_positive: a_transfer_minamount > 0.0
do
transfer_minamount := a_transfer_minamount
ensure
transfer_minamount_assigned: transfer_minamount = a_transfer_minamount
end
set_creditline (a_creditline: like creditline)
-- Assign `creditline' with `a_creditline'.
do
creditline := a_creditline
ensure
creditline_assigned: creditline = a_creditline
end
set_interest_deposit (an_interest_deposit: like interest_deposit)
-- Assign `interest_deposit' with `an_interest_deposit'.
require
an_interest_deposit_within_bounds: an_interest_deposit >= 0.0 and an_interest_deposit <= 1.0
do
interest_deposit := an_interest_deposit
ensure
interest_deposit_assigned: interest_deposit = an_interest_deposit
end
set_interest_debit (an_interest_debit: like interest_debit)
-- Assign `interest_debit' with `an_interest_debit'.
require
an_interest_debit_within_bounds: an_interest_debit >= 0.0 and an_interest_debit <= 1.0
do
interest_debit := an_interest_debit
ensure
interest_debit_assigned: interest_debit = an_interest_debit
end
invariant
interest_debit_within_bounds: interest_debit >= 0.0 and interest_debit <= 1.0
interest_deposit_within_bounds: interest_deposit >= 0.0 and interest_deposit <= 1.0
authorized_signers_attached: authorized_signers /= Void
authorized_signers_not_empty: authorized_signers.count > 0
transfer_minamount_positive: transfer_minamount > 0.0
end
|
