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

[Tim M. <tm...@un...>]

Hi Fabio,

You wrote:
> 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?

If I understand your question correctly, you are asking if you can 
declare a global name in one section, then include this section as a 
parent in another section, which then declares the name as global again? 
This is most definitely not permitted by Z. Global names are intended to 
be accessed without naming their parent. This allows us to change swap 
the parent specification with another one that declares the same 
names/types, without having to change the child; e.g. to use a different 
number toolkit.

I don't really think this is such a big problem. The easiest way around 
this is to do what many C programmers do: prefix all their names with 
the section name. So, instead of declaring "name" in the section 
"Field", "Field_name" (or maybe "ff_name"). This breaks the idea I 
discussed above, but is a compromise.

The other alternative is to use Object-Z and declare these are variables 
in classes. That is a pretty big step to make just to simplify naming 
though.

> (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

There is a property called "czt.path". It is a property that is set when 
you run the Java interpreter (e.g. java 
-Dczt.path="/home/me/project/module1/" czt.jar). If you set the to 
include all directories in which different files reside, then CZT will 
look through all of those. So, if you include a parent section called 
"A", CZT will look for a file called "A.tex", "A.zed", or "A.utf" (and 
whatever other file extensions it supports) in all directories in 
czt.path, and will read the first file that it matches.

I don't know how to set properties in Eclipse, but I'm sure there will 
be a way to do so.

Regards,
Tim