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

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

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

Yes, you are right but there is no way to change that property from eclipse 
because it is automatically declared a new czt.path any time a new 
specification file is created and that path is set to be the current 
directory of the new specification file. So for example if I create folder 
Goofy with goofy.zed16 inside and a folder Goofy/Mickey with a file 
mickey.zed16 inside that parents goofy I get an error because goofy is not 
visible with czt.path=/Goofy/Mickey
And neither from /Goofy it's possible to see contents in /Goofy/Mickey 
because if write in goofy.zed16 "section goofy parents mickey" I get the 
same error saying that is not possible to build an operator table for mickey 
with czt.path=/Goofy .

I think there is a problem with the czt eclipse plugin because a new 
distinct czt.path is declared for each new current directory of a 
specification instead of having a single property set to 
czt.path=project_home/*
It's also impossible to use the "linked resources" eclipse facility because 
even if I declare an environment variable in the workspace with the path to 
a resource of interest the plugin seems not able to see that variable 
because linked resources are disabled.

Moreover if I try to use Jedit instead i need some jars that are shipped 
only with the czt 1.5 source. But If i try to build it with maven following 
the instructions i get the error:

-----------------------------------
[ERROR] BUILD ERROR
[INFO] ----------------------------
[INFO] Failed to resolve artifact.

Missing:
----------
1) net.sourceforge.czt:util:jar:1.5-SNAPSHOT

  Try downloading the file manually from the project website.

  Then, install it using the command:
      mvn install:install-file -DgroupId=net.sourceforge.czt -Dartifa

  Alternatively, if you host your own repository you can deploy the f
      mvn deploy:deploy-file -DgroupId=net.sourceforge.czt -Dartifact

  Path to dependency:
        1) net.sourceforge.czt:jaxb:jar:1.5
        2) net.sourceforge.czt:util:jar:1.5-SNAPSHOT

----------
1 required artifact is missing.

for artifact:
  net.sourceforge.czt:jaxb:jar:1.5

from the specified remote repositories:
  central (http://repo1.maven.org/maven2),
  czt (http://czt.sourceforge.net/maven/repository)



[INFO] --------------------------------------------------------------
[INFO] For more information, run Maven with the -e switch
[INFO] --------------------------------------------------------------
[INFO] Total time: 1 minute 47 seconds
[INFO] Finished at: Wed Aug 01 12:18:57 CEST 2012
[INFO] Final Memory: 21M/52M
[INFO] --------------------------------------------------------------
C:\Documents and Settings\Fabio\Desktop\CZT\czt_1_5_0_src\czt_1_5_0>



I hope you could help me


Yours faithfully


Fabio De Simone

Computer Science Engineering student

Alma Mater Studiorum University of Bologna


----- Original Message ----- 
From: "Tim Miller" <tm...@un...>
To: "Fabio De Simone" <fab...@gm...>
Cc: <czt...@li...>
Sent: Tuesday, July 31, 2012 8:55 AM
Subject: Re: [CZT-Users] name clash in Z object orientation notation


> 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