[CZT-Users] name clash in Z object orientation notation

[Fabio De S. <fab...@gm...>]

Good Morning CZT staff,

I'm an Italian computer science engineering student and I'm trying to build a complex software system using software engineering metodology.
After learning what the word "analysis" really means I've come to the conclusion that a formal specification of expected external behaviour of a component in necessary for the software engineering development methodology to make sense.
So I've chosen the Z language to do that and I would like to use your CZT framework to build that formal specification. I've found a good paper ("Utting,Wang: Object Orientation without extending Z) that suggest a notation particularly useful to specify modular projects. 
But I've been blocked by a problem: if I use AXIOMATIC DEFINITION to specify a class that has a property "name", then I cannot specify another distinct class in a different package that has it's own property named "name" because that symbol had already been used to define the property of another class. This is a very big problem in a complex project. So I'm writing that mail to you to ask how to overcome that axiom name clash problem. 
I think It could be solved by a good use of the "section ... parents" mechanism but I've not been able to find out how to say to the czt Z interpreter to change it's SectTypeEnv mappings to avoid name clash with imported (parent) sections. (For example if I have a section that specify a class "Message" with a property "name" and that section parents another section specifying a class "Field" with it's own "name" property I would like to refer to the latter using for instance "Field.name" in the section that contains "Message" specification. This could avoid the name clash with the axiom defining the property "name" of Message like a total function from Message to (for instance) seq char.

Could you Help me please?


(I'm using the czt eclipse plugin for writing the specification)

P.S. I've another question: I've noticed that If a section parents another one, the latter must be in the same directory of the first, or the Z interpreter cannot find it. There exists a way to put pieces of the specification in different folders and then to say to the Z interpreter a path to look for the parent resources? I've tried in many ways but I've not been able to overcome the problem and I've been forced to put all the specification files in the same folder. That is a problem if one have to specify a complex system.


I hope you could help me


Yours faithfully


Fabio De Simone

Computer Science Engineering student

Alma Mater Studiorum University of Bologna