make all void-safe

and much more improvements

1 files changed, 10 insertions, 0 deletions

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