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/studentaccount.e | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'bank-eiffel/studentaccount.e') 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 -- cgit v1.2.3