From be3258068761a7c9eba329d205195f4cb3dd1eef Mon Sep 17 00:00:00 2001 From: totycro Date: Sun, 22 May 2011 22:13:33 +0200 Subject: Added preset ranges for values to accout --- bank-eiffel/account.e | 34 ++++++++++++++++++++++++++++++---- 1 file changed, 30 insertions(+), 4 deletions(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index 3ef7a8b..0a7d202 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -20,6 +20,16 @@ create feature -- 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 @@ -41,12 +51,24 @@ feature -- Access feature {NONE} -- Initialization - make (an_authorized_signer: PERSON) + 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]) do create authorized_signers.make(1) add_authorized_signer (an_authorized_signer) transfer_minamount := 2 balance := 0 + creditline := a_credit_line + interest_debit := an_interest_debit + interest_deposit := an_interest_deposit + interest_deposit_range := an_interest_deposit_range + interest_debit_range := an_interest_debit_range + creditline_range := a_credit_line_range end feature -- Basic operations @@ -137,8 +159,6 @@ feature {NONE} -- Implementation set_interest_debit (an_interest_debit: like interest_debit) -- Assign `interest_debit' with `an_interest_debit'. - require - an_interest_debit_within_bounds: an_interest_debit >= 0.0 and an_interest_debit <= 1.0 do interest_debit := an_interest_debit ensure @@ -146,9 +166,15 @@ feature {NONE} -- Implementation end invariant - interest_debit_within_bounds: interest_debit >= 0.0 and interest_debit <= 1.0 + interest_debit_within_bounds: + interest_debit >= interest_debit_range.item (0) and + interest_debit <= interest_debit_range.item (1) + interest_deposit_within_bounds: + interest_deposit >= interest_deposit_range.item (0) and + interest_deposit <= interest_deposit_range.item (1) interest_deposit_within_bounds: interest_deposit >= 0.0 and interest_deposit <= 1.0 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 (0) and creditline <= creditline_range.item (1) end -- cgit v1.2.3 From 3d70ca15591e4f4db578ba44fda674e6e44a7e56 Mon Sep 17 00:00:00 2001 From: totycro Date: Sun, 22 May 2011 23:12:59 +0200 Subject: members should be private --- bank-eiffel/account.e | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index 0a7d202..78a293f 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -18,7 +18,7 @@ create -- -> 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 -- cgit v1.2.3 From 559387cc3c179943d9b064b59c0ba10164bcef55 Mon Sep 17 00:00:00 2001 From: totycro Date: Mon, 23 May 2011 00:53:33 +0200 Subject: Fixed access to privates Added preconditions --- bank-eiffel/account.e | 39 +++++++++++++++++++++++++++++++-------- 1 file changed, 31 insertions(+), 8 deletions(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index 78a293f..39e4167 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -58,6 +58,13 @@ feature {NONE} -- Initialization an_interest_deposit_range: ARRAY[REAL_64]; an_interest_debit_range: ARRAY[REAL_64]; a_credit_line_range: ARRAY[REAL_64]) + require + a_credit_line_range.count() = 2 + an_interest_debit_range.count() = 2 + an_interest_deposit_range.count() = 2 + a_credit_line_range.item (0) < a_credit_line_range.item (1) + an_interest_debit_range.item (0) < an_interest_debit_range.item (1) + an_interest_deposit_range.item (0) < an_interest_deposit_range.item (1) do create authorized_signers.make(1) add_authorized_signer (an_authorized_signer) @@ -75,9 +82,9 @@ feature -- Basic operations deposit (an_amount: like transfer_minamount; an_authorized_signer: PERSON) require - an_authorized_signer_authorized: authorized_signers.has (an_authorized_signer) + an_authorized_signer_authorized: has_authorized_signer (an_authorized_signer) an_amount_positive: an_amount > 0.0 - transfer_minamount_ok: an_amount >= transfer_minamount + transfer_minamount_ok: an_amount >= get_transfer_minamount do balance := balance + an_amount ensure @@ -87,9 +94,9 @@ feature -- Basic operations withdraw (an_amount: like transfer_minamount; an_authorized_signer: PERSON) require - an_authorized_signer_authorized: authorized_signers.has (an_authorized_signer) + an_authorized_signer_authorized: has_authorized_signer (an_authorized_signer) an_amount_positive: an_amount > 0.0 - transfer_minamount_ok: an_amount >= transfer_minamount + transfer_minamount_ok: an_amount >= get_transfer_minamount do balance := balance - an_amount ensure @@ -109,7 +116,7 @@ feature -- Basic operations add_authorized_signer (an_authorized_signer: PERSON) require an_authorized_signer_attached: an_authorized_signer /= Void - an_authorized_signer_notinlist: not authorized_signers.has (an_authorized_signer) + an_authorized_signer_notinlist: not has_authorized_signer (an_authorized_signer) do authorized_signers.put (an_authorized_signer) ensure @@ -119,14 +126,31 @@ feature -- Basic operations remove_authorized_signer (an_authorized_signer: PERSON) require an_authorized_signer_attached: an_authorized_signer /= Void - an_authorized_signer_inlist: authorized_signers.has (an_authorized_signer) - authorized_signers_never_empty: authorized_signers.count >= 2 + an_authorized_signer_inlist: has_authorized_signer (an_authorized_signer) + authorized_signers_never_empty: authorized_signers_count >= 2 do authorized_signers.prune (an_authorized_signer) ensure authorized_signers_assigned: not authorized_signers.has (an_authorized_signer) end + has_authorized_signer (an_authorized_signer: PERSON) : BOOLEAN + 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 + + feature {NONE} -- Implementation set_transfer_minamount (a_transfer_minamount: like transfer_minamount) @@ -172,7 +196,6 @@ invariant interest_deposit_within_bounds: interest_deposit >= interest_deposit_range.item (0) and interest_deposit <= interest_deposit_range.item (1) - interest_deposit_within_bounds: interest_deposit >= 0.0 and interest_deposit <= 1.0 authorized_signers_attached: authorized_signers /= Void authorized_signers_not_empty: authorized_signers.count > 0 transfer_minamount_positive: transfer_minamount > 0.0 -- cgit v1.2.3 From 3d0cdbe62989a59975938d4a0ab734d3e7f41be8 Mon Sep 17 00:00:00 2001 From: totycro Date: Mon, 23 May 2011 01:21:19 +0200 Subject: added advance --- bank-eiffel/account.e | 34 +++++++++++++++++++++++----------- 1 file changed, 23 insertions(+), 11 deletions(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index 39e4167..61145f0 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -62,14 +62,14 @@ feature {NONE} -- Initialization a_credit_line_range.count() = 2 an_interest_debit_range.count() = 2 an_interest_deposit_range.count() = 2 - a_credit_line_range.item (0) < a_credit_line_range.item (1) - an_interest_debit_range.item (0) < an_interest_debit_range.item (1) - an_interest_deposit_range.item (0) < an_interest_deposit_range.item (1) + 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) do create authorized_signers.make(1) add_authorized_signer (an_authorized_signer) - transfer_minamount := 2 - balance := 0 + transfer_minamount := 2.0 + balance := 0.0 creditline := a_credit_line interest_debit := an_interest_debit interest_deposit := an_interest_deposit @@ -139,7 +139,6 @@ feature -- Basic operations Result := authorized_signers.has (an_authorized_signer) end - authorized_signers_count : INTEGER do Result := authorized_signers.count @@ -150,6 +149,19 @@ feature -- Basic operations Result := transfer_minamount end + get_balance : REAL_64 + do + Result := balance + end + + advance + do + if balance < 0.0 then -- debit + balance := balance + (balance * interest_debit) + else -- deposit + balance := balance + (balance * interest_deposit) + end + end feature {NONE} -- Implementation @@ -191,13 +203,13 @@ feature {NONE} -- Implementation invariant interest_debit_within_bounds: - interest_debit >= interest_debit_range.item (0) and - interest_debit <= interest_debit_range.item (1) + 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 (0) and - interest_deposit <= interest_deposit_range.item (1) + 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 (0) and creditline <= creditline_range.item (1) + creditline_range_correct: creditline >= creditline_range.item (1) and creditline <= creditline_range.item (2) end -- cgit v1.2.3 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 +++++++++++++++++++++----------------------------- 1 file changed, 62 insertions(+), 89 deletions(-) (limited to 'bank-eiffel/account.e') 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 -- cgit v1.2.3 From 1daf62f05c19e6f96d16d3688055dfd20d89d2b8 Mon Sep 17 00:00:00 2001 From: manuel Date: Mon, 23 May 2011 20:37:54 +0200 Subject: - add tests - remove notes - fix minamount for subaccounts --- bank-eiffel/account.e | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index d0a3fc4..1fc62fb 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -1,9 +1,3 @@ -note - description: "Summary description for {ACCOUNT}." - author: "" - date: "$Date$" - revision: "$Revision$" - class ACCOUNT @@ -57,14 +51,15 @@ feature {NONE} -- Initialization do create authorized_signers.make(1) add_authorized_signer (an_authorized_signer) - transfer_minamount := 2.0 - balance := 0.0 creditline := a_credit_line interest_debit := an_interest_debit interest_deposit := an_interest_deposit interest_deposit_range := an_interest_deposit_range interest_debit_range := an_interest_debit_range creditline_range := a_credit_line_range + + set_default_transfer_minamount + balance := 0.0 end feature -- Basic operations @@ -146,6 +141,11 @@ feature {NONE} -- Implementation transfer_minamount_assigned: transfer_minamount = a_transfer_minamount end + set_default_transfer_minamount + do + set_transfer_minamount (2.0) + end + set_creditline (a_creditline: like creditline) require a_creditline_within_bounds: a_creditline >= creditline_range.min -- cgit v1.2.3 From 9a787349e121be1ad9e83d4086244cd90422ee0e Mon Sep 17 00:00:00 2001 From: manuel Date: Mon, 23 May 2011 21:30:40 +0200 Subject: more tests --- bank-eiffel/account.e | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index 1fc62fb..7c127ec 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -105,7 +105,8 @@ feature -- Basic operations remove_authorized_signer (an_authorized_signer: PERSON) require - authorized_signers_never_empty: get_authorized_signers.count >= 2 + authorized_signers_never_empty: (get_authorized_signers.has (an_authorized_signer) + and get_authorized_signers.count >= 2) or True do if authorized_signers.has (an_authorized_signer) then authorized_signers.prune (an_authorized_signer) -- cgit v1.2.3 From ccfe458b09dd900c12b0421f19abdf9887d5b912 Mon Sep 17 00:00:00 2001 From: manuel Date: Thu, 26 May 2011 14:11:46 +0200 Subject: more bank example app: - add persistent store - implement ranges --- bank-eiffel/account.e | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index 7c127ec..fe9cc3b 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -23,13 +23,15 @@ feature -- Access feature {NONE} -- Implementation - creditline_range: TUPLE [min: like creditline; max: like creditline] + range: detachable TUPLE [min: REAL_64; max: REAL_64] + + creditline_range: attached like range -- min/max for creditline - interest_deposit_range: TUPLE [min: like interest_deposit; max: like interest_deposit] + interest_deposit_range: attached like range -- min/max for interest_deposit - interest_debit_range: TUPLE [min: like interest_debit; max: like interest_debit] + interest_debit_range: attached like range -- min/max for interest_debit authorized_signers: ARRAYED_SET [PERSON] -- cgit v1.2.3 From cf31e1f2788869624a9a363f7579838ddae369a2 Mon Sep 17 00:00:00 2001 From: manuel Date: Thu, 26 May 2011 19:55:22 +0200 Subject: finall commit hopefully --- bank-eiffel/account.e | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) (limited to 'bank-eiffel/account.e') diff --git a/bank-eiffel/account.e b/bank-eiffel/account.e index fe9cc3b..a6e30ef 100644 --- a/bank-eiffel/account.e +++ b/bank-eiffel/account.e @@ -81,16 +81,19 @@ feature -- Basic operations require an_authorized_signer_authorized: get_authorized_signers.has (an_authorized_signer) transfer_minamount_ok: an_amount >= transfer_minamount + balance_beneath_creditline: balance - an_amount >= creditline do balance := balance - an_amount ensure + balance_beneath_creditline: balance >= creditline balance_decreased: balance < old balance withdrawed: balance = old balance - an_amount - 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 + recipient_account_not_same: Current /= an_account do withdraw (an_amount, an_authorized_signer) an_account.deposit (an_amount, another_authorized_signer) @@ -107,12 +110,10 @@ feature -- Basic operations remove_authorized_signer (an_authorized_signer: PERSON) require - authorized_signers_never_empty: (get_authorized_signers.has (an_authorized_signer) - and get_authorized_signers.count >= 2) or True + authorized_signer_exists: (get_authorized_signers.has (an_authorized_signer)) + authorized_signers_not_empty: get_authorized_signers.count >= 2 do - if authorized_signers.has (an_authorized_signer) then - authorized_signers.prune (an_authorized_signer) - end + authorized_signers.prune (an_authorized_signer) ensure authorized_signers_assigned: not authorized_signers.has (an_authorized_signer) end -- cgit v1.2.3