# How to prevent the change of other objects in Z specification?

I have Z specification of Banking system, whose fragments are:

and

I think that the specification is OK, but my professor says that this specifiction is completely wrong, because AddAccount operation allows to change the information about other clients (i.e. the information about accounts of other clients) and information about bank's customers generally (e.g. he says that operation allows add or delete other customers to the Bank). I can not see this permission and what I need to correct. Maybe some advice is available?

• Don't use images as main content of your post. This makes your question impossible to search and inaccessible to the visually impaired; we don't like that. Please transcribe text and mathematics (note that you can use LaTeX) and don't forget to give proper attribution to your sources! – Raphael Aug 5 '16 at 12:09
• I'm sorry I can't help with Z specification, but why is the account balance a real number? Wouldn't a whole number of cents in $\mathbb{N}$ or $\mathbb{Z}$ be better? – Lieuwe Vinkhuijzen Aug 7 '16 at 0:15
• @Lieuwe Vinkhuijzen this is a rational number, not a deprecated for this purpose generic machine floating point value representation. So, it may be ok, if some local specifications aren't directly against that, a lot of currencies haven't any "cents" and can be divided unlimited finite times. – Les Aug 12 '16 at 9:55
• This specification of the AddAccount operation admits implementations that are probably not intended. For instances, one could erase every pre-existing account and just have a single account, namely the one to be added. To fix this I'd suggest to describe the final state of the Bank in terms of its initial state and the inputs. – Kai Nov 27 '16 at 12:03