1 files changed, 62 insertions, 89 deletions

diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e
index 61145f0..d0a3fc4 100644
--- a/bank-eiffel/account.e
+++ b/bank-eiffel/account.e
@@ -10,32 +10,10 @@ class
 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
 
-feature {NONE} -- Access
-
-        creditline_range: ARRAY[REAL_64]
-                attribute Result := ({like creditline_range}).default end --| Remove line when Void Safety is properly set
-
-        interest_debit_range: ARRAY[REAL_64]
-                attribute Result := ({like interest_debit_range}).default end --| Remove line when Void Safety is properly set
-
-        interest_deposit_range: ARRAY[REAL_64]
-                        -- min/max for interest_deposit
-                attribute Result := ({like interest_deposit_range}).default end --| Remove line when Void Safety is properly set
-
-        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
+        balance: REAL_64
+                        -- Kontostand
 
         creditline: REAL_64 assign set_creditline
                         -- Kreditrahmen
@@ -46,25 +24,36 @@ feature {NONE} -- Access
         interest_debit: REAL_64 assign set_interest_debit
                         -- Sollverzinsung
 
-        balance: REAL_64
-                        -- Kontostand
+        transfer_minamount: REAL_64 assign set_transfer_minamount
+                        -- Mindestbetrag fuer jede Einzahlung, Auszahlung und Ueberweisung
+
+feature {NONE} -- Implementation
+
+        creditline_range: TUPLE [min: like creditline; max: like creditline]
+                        -- min/max for creditline
+
+        interest_deposit_range: TUPLE [min: like interest_deposit; max: like interest_deposit]
+                        -- min/max for interest_deposit
+
+        interest_debit_range: TUPLE [min: like interest_debit; max: like interest_debit]
+                        -- min/max for interest_debit
+
+        authorized_signers: ARRAYED_SET [PERSON]
+                        -- Zeichnungsberechtigte
 
 feature {NONE} -- Initialization
 
         make (an_authorized_signer: PERSON;
-                  an_interest_deposit: REAL_64;
-                  an_interest_debit: REAL_64;
-                  a_credit_line: REAL_64;
-                  an_interest_deposit_range: ARRAY[REAL_64];
-                  an_interest_debit_range: ARRAY[REAL_64];
-                  a_credit_line_range: ARRAY[REAL_64])
+                  an_interest_deposit: like interest_deposit;
+                  an_interest_debit: like interest_debit;
+                  a_credit_line: like creditline;
+                  an_interest_deposit_range: like interest_deposit_range;
+                  an_interest_debit_range: like interest_debit_range;
+                  a_credit_line_range: like creditline_range)
                 require
-                        a_credit_line_range.count() = 2
-                        an_interest_debit_range.count() = 2
-                        an_interest_deposit_range.count() = 2
-                        a_credit_line_range.item (1) < a_credit_line_range.item (2)
-                        an_interest_debit_range.item (1) < an_interest_debit_range.item (2)
-                        an_interest_deposit_range.item (1) < an_interest_deposit_range.item (2)
+                        a_credit_line_range.min < a_credit_line_range.max
+                        an_interest_debit_range.min < an_interest_debit_range.max
+                        an_interest_deposit_range.min < an_interest_deposit_range.max
                 do
                         create authorized_signers.make(1)
                         add_authorized_signer (an_authorized_signer)
@@ -82,9 +71,8 @@ feature -- Basic operations
 
         deposit (an_amount: like transfer_minamount; an_authorized_signer: PERSON)
                 require
-                        an_authorized_signer_authorized: has_authorized_signer (an_authorized_signer)
-                        an_amount_positive: an_amount > 0.0
-                        transfer_minamount_ok: an_amount >= get_transfer_minamount
+                        an_authorized_signer_authorized: get_authorized_signers.has (an_authorized_signer)
+                        transfer_minamount_ok: an_amount >= transfer_minamount
                 do
                         balance := balance + an_amount
                 ensure
@@ -94,71 +82,55 @@ feature -- Basic operations
 
         withdraw (an_amount: like transfer_minamount; an_authorized_signer: PERSON)
                 require
-                        an_authorized_signer_authorized: has_authorized_signer (an_authorized_signer)
-                        an_amount_positive: an_amount > 0.0
-                        transfer_minamount_ok: an_amount >= get_transfer_minamount
+                        an_authorized_signer_authorized: get_authorized_signers.has (an_authorized_signer)
+                        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
+                        balance_beneath_creditline: balance >= creditline
                 end
 
-        transfer(an_amount: like transfer_minamount; an_authorized_signer: PERSON; an_account: like Current; another_authorized_signer: PERSON;)
-                require
-                        an_account_attached: an_account /= Void
+        transfer(an_amount: like transfer_minamount; an_authorized_signer: PERSON;
+                         an_account: like Current; another_authorized_signer: PERSON)
                 do
                         withdraw (an_amount, an_authorized_signer)
                         an_account.deposit (an_amount, another_authorized_signer)
                 end
 
         add_authorized_signer (an_authorized_signer: PERSON)
-                require
-                        an_authorized_signer_attached: an_authorized_signer /= Void
-                        an_authorized_signer_notinlist: not has_authorized_signer (an_authorized_signer)
                 do
-                        authorized_signers.put (an_authorized_signer)
+                        if not authorized_signers.has (an_authorized_signer) then
+                                authorized_signers.put (an_authorized_signer)
+                        end
                 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: has_authorized_signer (an_authorized_signer)
-                        authorized_signers_never_empty: authorized_signers_count >= 2
+                        authorized_signers_never_empty: get_authorized_signers.count >= 2
                 do
-                        authorized_signers.prune (an_authorized_signer)
+                        if authorized_signers.has (an_authorized_signer) then
+                                authorized_signers.prune (an_authorized_signer)
+                        end
                 ensure
                         authorized_signers_assigned: not authorized_signers.has (an_authorized_signer)
                 end
 
-        has_authorized_signer  (an_authorized_signer: PERSON) : BOOLEAN
+        get_authorized_signers: FINITE [PERSON]
                 do
-                        Result := authorized_signers.has (an_authorized_signer)
-                end
-
-        authorized_signers_count : INTEGER
-                do
-                        Result := authorized_signers.count
-                end
-
-        get_transfer_minamount : REAL_64
-                do
-                        Result := transfer_minamount
-                end
-
-        get_balance : REAL_64
-                do
-                        Result := balance
+                        Result := authorized_signers
                 end
 
         advance
                 do
-                        if balance < 0.0 then -- debit
+                        if balance < 0.0 then
+                                -- debit
                                 balance := balance + (balance * interest_debit)
-                        else -- deposit
+                        else
+                                -- deposit
                                 balance := balance + (balance * interest_deposit)
                         end
                 end
@@ -166,7 +138,6 @@ feature -- Basic operations
 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
@@ -176,7 +147,9 @@ feature {NONE} -- Implementation
                 end
 
         set_creditline (a_creditline: like creditline)
-                        -- Assign `creditline' with `a_creditline'.
+                require
+                        a_creditline_within_bounds: a_creditline >= creditline_range.min
+                                and a_creditline <= creditline_range.max
                 do
                         creditline := a_creditline
                 ensure
@@ -184,9 +157,9 @@ feature {NONE} -- Implementation
                 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
+                        an_interest_deposit_within_bounds: interest_deposit >= interest_deposit_range.min
+                                and interest_deposit <= interest_deposit_range.max
                 do
                         interest_deposit := an_interest_deposit
                 ensure
@@ -194,7 +167,9 @@ feature {NONE} -- Implementation
                 end
 
         set_interest_debit (an_interest_debit: like interest_debit)
-                        -- Assign `interest_debit' with `an_interest_debit'.
+                require
+                        an_interest_deposit_within_bounds: interest_debit >= interest_debit_range.min
+                                and interest_debit <= interest_debit_range.max
                 do
                         interest_debit := an_interest_debit
                 ensure
@@ -202,14 +177,12 @@ feature {NONE} -- Implementation
                 end
 
 invariant
-        interest_debit_within_bounds:
-                interest_debit >= interest_debit_range.item (1) and
-                interest_debit <= interest_debit_range.item (2)
-        interest_deposit_within_bounds:
-                interest_deposit >= interest_deposit_range.item (1) and
-                interest_deposit <= interest_deposit_range.item (2)
-        authorized_signers_attached: authorized_signers /= Void
         authorized_signers_not_empty: authorized_signers.count > 0
         transfer_minamount_positive: transfer_minamount > 0.0
-        creditline_range_correct: creditline >= creditline_range.item (1) and creditline <= creditline_range.item (2)
+        creditline_within_bounds: creditline >= creditline_range.min
+                and creditline <= creditline_range.max
+        interest_debit_within_bounds: interest_debit >= interest_debit_range.min
+                and interest_debit <= interest_debit_range.max
+        interest_deposit_within_bounds: interest_deposit >= interest_deposit_range.min
+                and interest_deposit <= interest_deposit_range.max
 end