summaryrefslogtreecommitdiffstats
path: root/bank-eiffel/account.e
diff options
context:
space:
mode:
Diffstat (limited to 'bank-eiffel/account.e')
-rw-r--r--bank-eiffel/account.e75
1 files changed, 75 insertions, 0 deletions
diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e
new file mode 100644
index 0000000..578aec2
--- /dev/null
+++ b/bank-eiffel/account.e
@@ -0,0 +1,75 @@
1note
2 description: "Summary description for {ACCOUNT}."
3 author: ""
4 date: "$Date$"
5 revision: "$Revision$"
6
7class
8 ACCOUNT
9
10inherit
11
12
13feature -- Access
14
15 authorized_signers: SET [PERSON] assign set_authorized_signers
16 -- Zeichnungsberechtigte
17 attribute Result := ({like authorized_signers}).default end --| Remove line when Void Safety is properly set
18
19 balance: REAL_64
20 -- Kontostand
21
22 creditline: REAL_64 assign set_creditline
23 -- Kreditrahmen
24
25 interest_deposit: REAL_32 assign set_interest_deposit
26 -- Habenverzinsung
27
28 interest_debit: REAL_32 assign set_interest_debit
29 -- Sollverzinsung
30
31feature -- Element change
32
33 set_authorized_signers (an_authorized_signers: like authorized_signers)
34 -- Assign `authorized_signers' with `an_authorized_signers'.
35 require
36 an_authorized_signers_attached: an_authorized_signers /= Void
37 do
38 authorized_signers := an_authorized_signers
39 ensure
40 authorized_signers_assigned: authorized_signers = an_authorized_signers
41 end
42
43 set_creditline (a_creditline: like creditline)
44 -- Assign `creditline' with `a_creditline'.
45 do
46 creditline := a_creditline
47 ensure
48 creditline_assigned: creditline = a_creditline
49 end
50
51 set_interest_deposit (an_interest_deposit: like interest_deposit)
52 -- Assign `interest_deposit' with `an_interest_deposit'.
53 require
54 an_interest_deposit_within_bounds: an_interest_deposit >= 0.0 and an_interest_deposit <= 1.0
55 do
56 interest_deposit := an_interest_deposit
57 ensure
58 interest_deposit_assigned: interest_deposit = an_interest_deposit
59 end
60
61 set_interest_debit (an_interest_debit: like interest_debit)
62 -- Assign `interest_debit' with `an_interest_debit'.
63 require
64 an_interest_debit_within_bounds: an_interest_debit >= 0.0 and an_interest_debit <= 1.0
65 do
66 interest_debit := an_interest_debit
67 ensure
68 interest_debit_assigned: interest_debit = an_interest_debit
69 end
70
71invariant
72 interest_debit_within_bounds: interest_debit >= 0.0 and interest_debit <= 1.0
73 interest_deposit_within_bounds: interest_deposit >= 0.0 and interest_deposit <= 1.0
74 authorized_signers_attached: authorized_signers /= Void
75end