From e03195a9325d2671208efc45f4a4d083664eafe2 Mon Sep 17 00:00:00 2001 From: manuel Date: Mon, 23 May 2011 19:28:45 +0200 Subject: make all void-safe and much more improvements --- bank-eiffel/account.e | 151 ++++++++++++++++----------------------- bank-eiffel/bank.e | 21 ++++++ bank-eiffel/bank.ecf | 2 +- bank-eiffel/person.e | 10 ++- bank-eiffel/retiree.e | 3 + bank-eiffel/retireeaccount.e | 10 +++ bank-eiffel/student.e | 3 + bank-eiffel/studentaccount.e | 10 +++ bank-eiffel/tests/test_account.e | 65 +++++++++++++---- bank-eiffel/tests/test_person.e | 22 ------ 10 files changed, 164 insertions(+), 133 deletions(-) (limited to 'bank-eiffel') 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 @@ FOOP Exercise #3 - 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 -- cgit v1.2.3