summaryrefslogtreecommitdiffstats
path: root/bank-eiffel
diff options
context:
space:
mode:
authormanuel <manuel@mausz.at>2011-05-22 14:04:00 +0200
committermanuel <manuel@mausz.at>2011-05-22 14:04:00 +0200
commita47510de141d3a9ec11aebfb2de1c6002c595774 (patch)
tree5489e266fb5fe1257f36315d1e3f003040328caa /bank-eiffel
parent5d104abdbeeb8dbee63218df0fe07d53ef58128f (diff)
downloadfoop-a47510de141d3a9ec11aebfb2de1c6002c595774.tar.gz
foop-a47510de141d3a9ec11aebfb2de1c6002c595774.tar.bz2
foop-a47510de141d3a9ec11aebfb2de1c6002c595774.zip
more account stuff
Diffstat (limited to 'bank-eiffel')
-rw-r--r--bank-eiffel/account.e79
1 files changed, 67 insertions, 12 deletions
diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e
index 8faabdc..7555baa 100644
--- a/bank-eiffel/account.e
+++ b/bank-eiffel/account.e
@@ -7,28 +7,71 @@ note
7class 7class
8 ACCOUNT 8 ACCOUNT
9 9
10create
11 make
12
13-- TODO
14-- interest should defined by bank (via make?)
15-- add more checks to invariant (like balance >= creditline) ?
16-- check if balance is a getter and not a setter (doesn't has an assign)
17-- + check if authorized_signers is a getter and not a setter (it doesn't has an assign)
18-- -> if not: add a getter (via Result or so..) and move them to {NONE}
19-- much other stuff to test like: lower creditline so that balance will be invalid
10 20
11feature -- Access 21feature -- Access
12 22
13 transfer_minamount: REAL_32 assign set_transfer_minamount 23 transfer_minamount: REAL_64 assign set_transfer_minamount
14 -- Mindestbetrag für jede Einzahlung, Auszahlung und Überweisung 24 -- Mindestbetrag für jede Einzahlung, Auszahlung und Überweisung
15 25
16 authorized_signers: SET [PERSON] assign set_authorized_signers 26 authorized_signers: SET [PERSON]
17 -- Zeichnungsberechtigte 27 -- Zeichnungsberechtigte
18 attribute Result := ({like authorized_signers}).default end --| Remove line when Void Safety is properly set 28 attribute Result := ({like authorized_signers}).default end --| Remove line when Void Safety is properly set
19 29
20 balance: REAL_64
21 -- Kontostand
22
23 creditline: REAL_64 assign set_creditline 30 creditline: REAL_64 assign set_creditline
24 -- Kreditrahmen 31 -- Kreditrahmen
25 32
26 interest_deposit: REAL_32 assign set_interest_deposit 33 interest_deposit: REAL_64 assign set_interest_deposit
27 -- Habenverzinsung 34 -- Habenverzinsung
28 35
29 interest_debit: REAL_32 assign set_interest_debit 36 interest_debit: REAL_64 assign set_interest_debit
30 -- Sollverzinsung 37 -- Sollverzinsung
31 38
39 balance: REAL_64
40 -- Kontostand
41
42feature -- Initialization
43
44 make (an_authorized_signer: PERSON)
45 do
46 add_authorized_signers (an_authorized_signer)
47 balance := 0
48 end
49
50feature -- Basic operations
51
52 deposit (an_amount: like transfer_minamount)
53 require
54 an_amount_positive: an_amount > 0.0
55 transfer_minamount_ok: an_amount >= transfer_minamount
56 do
57 balance := balance + an_amount
58 ensure
59 balance_increased: balance > old balance
60 deposited: balance = old balance + an_amount
61 end
62
63 withdraw (an_amount: like transfer_minamount)
64 require
65 an_amount_positive: an_amount > 0.0
66 transfer_minamount_ok: an_amount >= transfer_minamount
67 do
68 balance := balance - an_amount
69 ensure
70 balance_increased: balance < old balance
71 withdrawed: balance = old balance - an_amount
72 creditline_ok: balance >= creditline
73 end
74
32feature -- Element change 75feature -- Element change
33 76
34 set_transfer_minamount (a_transfer_minamount: like transfer_minamount) 77 set_transfer_minamount (a_transfer_minamount: like transfer_minamount)
@@ -41,14 +84,25 @@ feature -- Element change
41 transfer_minamount_assigned: transfer_minamount = a_transfer_minamount 84 transfer_minamount_assigned: transfer_minamount = a_transfer_minamount
42 end 85 end
43 86
44 set_authorized_signers (an_authorized_signers: like authorized_signers) 87 add_authorized_signers (an_authorized_signer: PERSON)
45 -- Assign `authorized_signers' with `an_authorized_signers'. 88 require
89 an_authorized_signer_attached: an_authorized_signer /= Void
90 an_authorized_signer_notinlist: not authorized_signers.has (an_authorized_signer)
91 do
92 authorized_signers.put (an_authorized_signer)
93 ensure
94 authorized_signers_assigned: authorized_signers.has (an_authorized_signer)
95 end
96
97 remove_authorized_signers (an_authorized_signer: PERSON)
46 require 98 require
47 an_authorized_signers_attached: an_authorized_signers /= Void 99 an_authorized_signer_attached: an_authorized_signer /= Void
100 an_authorized_signer_inlist: authorized_signers.has (an_authorized_signer)
101 authorized_signers_never_empty: authorized_signers.count >= 2
48 do 102 do
49 authorized_signers := an_authorized_signers 103 authorized_signers.prune (an_authorized_signer)
50 ensure 104 ensure
51 authorized_signers_assigned: authorized_signers = an_authorized_signers 105 authorized_signers_assigned: not authorized_signers.has (an_authorized_signer)
52 end 106 end
53 107
54 set_creditline (a_creditline: like creditline) 108 set_creditline (a_creditline: like creditline)
@@ -83,5 +137,6 @@ invariant
83 interest_debit_within_bounds: interest_debit >= 0.0 and interest_debit <= 1.0 137 interest_debit_within_bounds: interest_debit >= 0.0 and interest_debit <= 1.0
84 interest_deposit_within_bounds: interest_deposit >= 0.0 and interest_deposit <= 1.0 138 interest_deposit_within_bounds: interest_deposit >= 0.0 and interest_deposit <= 1.0
85 authorized_signers_attached: authorized_signers /= Void 139 authorized_signers_attached: authorized_signers /= Void
140 authorized_signers_not_empty: authorized_signers.count > 0
86 transfer_minamount_positive: transfer_minamount > 0.0 141 transfer_minamount_positive: transfer_minamount > 0.0
87end 142end