make all void-safe

and much more improvements

10 files changed, 164 insertions, 133 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
diff --git a/bank-eiffel/bank.e b/bank-eiffel/bank.e
index 32d10ff..7c30afb 100644
--- a/bank-eiffel/bank.e
+++ b/bank-eiffel/bank.e
@@ -10,11 +10,32 @@ class
 create
         make
 
+feature {NONE} -- Implementation
+
+        customers: ARRAYED_SET [PERSON]
+                        -- Kunden
+
+        accounts: ARRAYED_SET [ACCOUNT]
+                        -- Vorname
+
 feature {NONE} -- Initialization
 
         make
                 do
+                        create customers.make(100)
+                        create accounts.make(100)
+                end
+
+feature -- Basic operations
 
+        get_customers: FINITE [PERSON]
+                do
+                        Result := customers
+                end
+
+        get_accounts: FINITE [ACCOUNT]
+                do
+                        Result := accounts
                 end
 
 end
diff --git a/bank-eiffel/bank.ecf b/bank-eiffel/bank.ecf
index b3bf92c..1eef831 100644
--- a/bank-eiffel/bank.ecf
+++ b/bank-eiffel/bank.ecf
@@ -4,7 +4,7 @@
                 <description>FOOP Exercise #3</description>
                 <root class="APPLICATION" feature="make"/>
                 <version major="0" minor="1" release="0" build="0" product="bank"/>
-                <option warning="true" void_safety="none">
+                <option warning="true" is_attached_by_default="true" void_safety="all">
                         <assertions precondition="true" postcondition="true" check="true" invariant="true" loop="true" supplier_precondition="true"/>
                 </option>
                 <setting name="executable_name" value="bank"/>
diff --git a/bank-eiffel/person.e b/bank-eiffel/person.e
index 54e1a45..9a2b281 100644
--- a/bank-eiffel/person.e
+++ b/bank-eiffel/person.e
@@ -14,11 +14,9 @@ feature -- Access
 
         surname: STRING_8 assign set_surname
                         -- Nachname
-                attribute Result := ({like surname}).default end --| Remove line when Void Safety is properly set
 
         firstname: STRING_8 assign set_firstname
                         -- Vorname
-                attribute Result := ({like firstname}).default end --| Remove line when Void Safety is properly set
 
 feature {NONE} -- Initialization
 
@@ -33,7 +31,7 @@ feature {NONE} -- Implementation
         set_surname (a_surname: like surname)
                         -- Assign `surname' with `a_surname'.
                 require
-                        a_surname_not_empty: a_surname /= Void and then not a_surname.is_empty
+                        a_surname_not_empty: not a_surname.is_empty
                 do
                         surname := a_surname
                 ensure
@@ -43,7 +41,7 @@ feature {NONE} -- Implementation
         set_firstname (a_firstname: like firstname)
                         -- Assign `firstname' with `a_firstname'.
                 require
-                        a_firstname_not_empty: a_firstname /= Void and then not a_firstname.is_empty
+                        a_firstname_not_empty: not a_firstname.is_empty
                 do
                         firstname := a_firstname
                 ensure
@@ -51,6 +49,6 @@ feature {NONE} -- Implementation
                 end
 
 invariant
-        firstname_not_empty: firstname /= Void and then not firstname.is_empty
-        surname_not_empty: surname /= Void and then not surname.is_empty
+        firstname_not_empty: not firstname.is_empty
+        surname_not_empty: not surname.is_empty
 end
diff --git a/bank-eiffel/retiree.e b/bank-eiffel/retiree.e
index 57e5d05..7f24d89 100644
--- a/bank-eiffel/retiree.e
+++ b/bank-eiffel/retiree.e
@@ -10,4 +10,7 @@ class
 inherit
         PERSON
 
+create
+        make
+        
 end
diff --git a/bank-eiffel/retireeaccount.e b/bank-eiffel/retireeaccount.e
index 3f56fd4..cf9bc91 100644
--- a/bank-eiffel/retireeaccount.e
+++ b/bank-eiffel/retireeaccount.e
@@ -10,6 +10,16 @@ class
 inherit
         ACCOUNT
 
+create
+        make
+
 invariant
         authorized_signers_only_one: authorized_signers.count = 1
+        authorized_signers_attached: authorized_signers.linear_representation /= Void
+        authorized_signers_only_retirees:
+                (attached authorized_signers.linear_representation as signers) implies signers.for_all(
+                        agent (person: PERSON): BOOLEAN
+                                do
+                                        Result := attached {RETIREE} person
+                                end)
 end
diff --git a/bank-eiffel/student.e b/bank-eiffel/student.e
index 2b5afd4..f910fa7 100644
--- a/bank-eiffel/student.e
+++ b/bank-eiffel/student.e
@@ -10,4 +10,7 @@ class
 inherit
         PERSON
 
+create
+        make
+
 end
diff --git a/bank-eiffel/studentaccount.e b/bank-eiffel/studentaccount.e
index a80d4bb..d1ccaef 100644
--- a/bank-eiffel/studentaccount.e
+++ b/bank-eiffel/studentaccount.e
@@ -10,6 +10,16 @@ class
 inherit
         ACCOUNT
 
+create
+        make
+
 invariant
         authorized_signers_only_one: authorized_signers.count = 1
+        authorized_signers_attached: authorized_signers.linear_representation /= Void
+        authorized_signers_only_students:
+                (attached authorized_signers.linear_representation as signers) implies signers.for_all(
+                        agent (person: PERSON): BOOLEAN
+                                do
+                                        Result := attached {STUDENT} person
+                                end)
 end
diff --git a/bank-eiffel/tests/test_account.e b/bank-eiffel/tests/test_account.e
index e0dfe4d..e1ca892 100644
--- a/bank-eiffel/tests/test_account.e
+++ b/bank-eiffel/tests/test_account.e
@@ -19,32 +19,67 @@ feature -- Test routines
                 local
                         person1: PERSON
                         person2: PERSON
-                        account: ACCOUNT
+                        person3: PERSON
+                        account1: ACCOUNT
+                        account2: ACCOUNT
                 do
                         create person1.make ("SOME_SURNAME_1", "SOME_FIRSTNAME_1")
                         create person2.make ("SOME_SURNAME_2", "SOME_FIRSTNAME_2")
+                        create person3.make ("SOME_SURNAME_3", "SOME_FIRSTNAME_3")
 
-                        create account.make (person1, 0.01, 0.02, -50.0, <<0.01, 0.022>>, <<0.01, 0.02>>, <<-100, -50>>)
-                        account.add_authorized_signer (person2)
+                        create account1.make (person1, 0.01, 0.02, -50.0, [0.01, 0.022], [0.01, 0.02], [-100.0, -50.0])
+                        assert("CREATE_EDIT_ACCOUNT_SIGNER_1", account1.get_authorized_signers.count = 1)
+                        account1.add_authorized_signer (person2)
+                        account1.add_authorized_signer (person2)
+                        account1.add_authorized_signer (person3)
+                        account1.remove_authorized_signer (person3)
+                        assert("CREATE_EDIT_ACCOUNT_SIGNER_2", account1.get_authorized_signers.count = 2)
 
+                        assert("CREATE_EDIT_ACCOUNT_BALANCE_1", account1.balance = 0.0)
+                        account1.deposit (50.0, person1)
+                        account1.deposit (50.0, person2)
+                        -- balance = 100.0
+                        account1.advance
+                        -- balance = 100.0 + 1% deposit
+                        account1.withdraw (100.0 + 100.0 * 0.01 + 50.0, person1)
+                        -- balance = -50.0
+                        account1.creditline := -100.0
+                        account1.withdraw (50.0, person1)
+                        -- balance = -100.0
+                        account1.advance
+                        -- balance = -100.0 + 2% debit
+                        assert("CREATE_EDIT_ACCOUNT_BALANCE_2", account1.balance = -102.0)
 
-                        --assert ("not_implemented", False)
+                        create account2.make(person3, 0.01, 0.02, -50, [0.01, 0.022], [0.01, 0.02], [-100.0, -50.0])
+                        account2.deposit (102.0, person3)
+                        account2.transfer (102.0, person3, account1, person1)
+                        assert("CREATE_EDIT_ACCOUNT_BALANCE_3", account1.balance = 0.0 and account2.balance = 0.0)
+
+                        account1.interest_deposit := 0.01
+                        account1.interest_deposit := 0.022
+                        account1.interest_debit := 0.01
+                        account1.interest_debit := 0.02
+                        account1.creditline := -100.0
+                        account1.creditline := -50.0
+                        account1.transfer_minamount := 10.0
                 end
 
-        ADVANCE
+        CREATE_STUDENTACCOUNT
                 local
-                        person1: PERSON
-                        account: ACCOUNT
-                        b : REAL_64
+                        person: STUDENT
+                        account: STUDENTACCOUNT
                 do
-                        create person1.make ("SOME_SURNAME_1", "SOME_FIRSTNAME_1")
-                        create account.make (person1, 0.01, 0.02, -50.0, <<0.01, 0.022>>, <<0.01, 0.02>>, <<-100, -50>>)
-
-                        account.deposit (100.0, person1)
-                        account.advance
-                        
-                        assert("balance not correct", account.get_balance = 101.0)
+                        create person.make("SOME_SURNAME", "SOME_FIRSTNAME")
+                        create account.make(person, 0.01, 0.02, -50.0, [0.01, 0.022], [0.01, 0.02], [-100.0, -50.0])
                 end
 
+        CREATE_RETIREEACCOUNT
+                local
+                        person: RETIREE
+                        account: RETIREEACCOUNT
+                do
+                        create person.make("SOME_SURNAME", "SOME_FIRSTNAME")
+                        create account.make(person, 0.01, 0.02, -50.0, [0.01, 0.022], [0.01, 0.02], [-100.0, -50.0])
+                end
 end
 
diff --git a/bank-eiffel/tests/test_person.e b/bank-eiffel/tests/test_person.e
index a501deb..67aea34 100644
--- a/bank-eiffel/tests/test_person.e
+++ b/bank-eiffel/tests/test_person.e
@@ -41,23 +41,12 @@ feature -- Test routines
                                 doretry := False
                                 assert("CREATE_EDIT_PERSON_EMPTY_SURNAME_1", False)
                         elseif retry_count = 1 then
-                                create person.make(void, "SOME_FIRSTNAME")
-                                doretry := False
-                                assert("CREATE_EDIT_PERSON_EMPTY_SURNAME_2", False)
-                        elseif retry_count = 2 then
                                 doretry := False
                                 create person.make("SOME_SURNAME", "SOME_FIRSTNAME")
                                 doretry := True
                                 person.surname := ""
                                 doretry := False
                                 assert("CREATE_EDIT_PERSON_EMPTY_SURNAME_3", False)
-                        elseif retry_count = 3 then
-                                doretry := False
-                                create person.make("SOME_SURNAME", "SOME_FIRSTNAME")
-                                doretry := True
-                                person.surname := void
-                                doretry := False
-                                assert("CREATE_EDIT_PERSON_EMPTY_SURNAME_4", False)
                         else
                                 doretry := False
                         end
@@ -80,23 +69,12 @@ feature -- Test routines
                                 doretry := False
                                 assert("CREATE_EDIT_PERSON_EMPTY_FIRSTNAME_1", False)
                         elseif retry_count = 1 then
-                                create person.make("SOME_SURNAME", void)
-                                doretry := False
-                                assert("CREATE_EDIT_PERSON_EMPTY_FIRSTNAME_2", False)
-                        elseif retry_count = 2 then
                                 doretry := False
                                 create person.make("SOME_SURNAME", "SOME_FIRSTNAME")
                                 doretry := True
                                 person.firstname := ""
                                 doretry := False
                                 assert("CREATE_EDIT_PERSON_EMPTY_FIRSTNAME_3", False)
-                        elseif retry_count = 3 then
-                                doretry := False
-                                create person.make("SOME_SURNAME", "SOME_FIRSTNAME")
-                                doretry := True
-                                person.firstname := void
-                                doretry := False
-                                assert("CREATE_EDIT_PERSON_EMPTY_FIRSTNAME_4", False)
                         else
                                 doretry := False
                         end