note description: "Summary description for {ACCOUNT}." author: "" date: "$Date$" revision: "$Revision$" class ACCOUNT feature -- Access transfer_minamount: REAL_32 assign set_transfer_minamount -- Mindestbetrag für jede Einzahlung, Auszahlung und Überweisung authorized_signers: SET [PERSON] assign set_authorized_signers -- 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 interest_deposit: REAL_32 assign set_interest_deposit -- Habenverzinsung interest_debit: REAL_32 assign set_interest_debit -- Sollverzinsung feature -- Element change 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 transfer_minamount := a_transfer_minamount ensure transfer_minamount_assigned: transfer_minamount = a_transfer_minamount end set_authorized_signers (an_authorized_signers: like authorized_signers) -- Assign `authorized_signers' with `an_authorized_signers'. require an_authorized_signers_attached: an_authorized_signers /= Void do authorized_signers := an_authorized_signers ensure authorized_signers_assigned: authorized_signers = an_authorized_signers end set_creditline (a_creditline: like creditline) -- Assign `creditline' with `a_creditline'. do creditline := a_creditline ensure creditline_assigned: creditline = a_creditline 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 do interest_deposit := an_interest_deposit ensure interest_deposit_assigned: interest_deposit = an_interest_deposit end 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 interest_debit_assigned: interest_debit = an_interest_debit end invariant interest_debit_within_bounds: interest_debit >= 0.0 and interest_debit <= 1.0 interest_deposit_within_bounds: interest_deposit >= 0.0 and interest_deposit <= 1.0 authorized_signers_attached: authorized_signers /= Void transfer_minamount_positive: transfer_minamount > 0.0 end