I have Z specification of Banking system, whose fragments are:andI 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?
How to prevent the change of other objects in Z specification?
formal methods;z notation