czt-users — For end-users of the CZT tools

[CZT-Users] Trouble defining a Pre-Operator

[Frank D. <fr...@do...>]

I am in transition from ZRM/fuzz to ISO-Z/czt (typechecker) and
experience some difficulties in defining my own operators. I use
LaTeX-Files as source. Here is my example:

\newcommand{\dsum}{\zpreop{\Sigma}}
%%Zprechar \dsum U+03A3
\begin{zed}
  \function (\dsum~\varg)
\end{zed}

\begin{gendef}[I]
  \dsum : (I \ffun \arithmos) \fun \arithmos
  \where
  ...
\end{gendef}

LaTeX compiles succesfully, but the typechecker reports on the first
line in the generic definition (\dsum : (I \ffun ...):

"Σ is declared as an operator, and cannot be used as a declaration
name"

I have used a similar setup for infix operators which eventually
worked after a lot of experiments. I have tried different characters
for \dsum and even the word "SUM", but the problem remains.

Thanks in advance for help
Frank



-- 
Frank Dordowsky
Säntisstr. 37
81825 München

Re: [CZT-Users] Is Z specification dead?

[Mark U. <bm....@gm...>]

Hi James

Very timely question - we are just starting to update the CZT project, with
a new Steering Committee, moving to GitHub, updating the build process etc.
We will post news here as we make progress.


But for your larger question about Z, it is probably true that it is less
widely used now than a decade or two ago.
I think this is largely because there are so many more specification
languages/tools now, many of which offer strong reasoning support to prove
properties of your specifications.

The best specification option varies, depending upon what kind of system
you are specifying.

For example, Alloy (http://alloytools.org) was partly inspired by Z, but
has better support for exploring properties, by using automated SAT solvers
to check properties of small subsets of the system and generate
counter-examples of properties when they are false.
For other projects, I sometimes use an interactive theorem prover like
Isabelle/HOL, or a system with automated prover support like the
Dafny-Boogie-Z3 tools.

If you are using Z you might like to check out the Z plugin for MS Word:
 * https://sourceforge.net/projects/zwordtools/

Cheers
Mark

On Tue, 1 Mar 2022 at 05:11, James Coulter <cou...@gm...> wrote:

> While I am relatively new to Z, I have found it to be an excellent
> language for specification.  However, I've noticed that books, academic
> sites, and even CZT, all have shown a steady decline in new material in
> recent years.
>
> Is Z being abandoned?  If so, what is replacing it?  For example, are
> people generally preferring other tools such as TLA+ or similar?  Or is
> formal specification struggling overall?  I will continue to both use and
> promote formal specification, but I think it's important to use tools that
> have an active community.  Should I continue to invest in Z or look
> elsewhere?
>
> Regards, James
>
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users
>

[CZT-Users] Is Z specification dead?

[James C. <cou...@gm...>]

While I am relatively new to Z, I have found it to be an excellent language
for specification.  However, I've noticed that books, academic sites, and
even CZT, all have shown a steady decline in new material in recent years.

Is Z being abandoned?  If so, what is replacing it?  For example, are
people generally preferring other tools such as TLA+ or similar?  Or is
formal specification struggling overall?  I will continue to both use and
promote formal specification, but I think it's important to use tools that
have an active community.  Should I continue to invest in Z or look
elsewhere?

Regards, James

Re: [CZT-Users] Eclipse 4.14 CZT plugins installation problem

[Julian R. <jro...@gm...>]

I found Eclipse 4.8 (photon) will run on my PC but with the same results
for CZT as 4.14.
Anything older refuses to run, as per 4.2 (Juno).

Please find attached a log snapshot from my Eclipse
~/workspace/.metadata/.log in which framework errors are reported.
This is not the entire log dump, just those parts for CZT.
Hope this helps someone.

With thanks,
julian


On Tue, 18 Feb 2020 at 12:10, Julian Rose <jro...@gm...> wrote:

> Hello,
>
> Sorry for the newbie question but I cannot get CZT Eclipse plugins to run.
> On the plus side the czt.jar from
> https://sourceforge.net/projects/czt/files/czt-ide/nightly/ standalone
> works perfectly well.
>
>
> After downloading the latest Eclipse 4.14 and installing the CZT nightly
> updates:
> From Help->About Eclipse SDK I see the CZT logo and in ->Installation
> Details I see CZT-Core, CZT for Eclipse and Z/Eves Prover Integration for
> CZT.
> However, there is nothing else Z in Eclipse at all. No perspective. No New
> CZT Project.
>
> My windows version is 64-bit 10, 1909 updates
> My jdk version is 11.0.1
>
> I downloaded Eclipse 4.14 from
> https://download.eclipse.org/eclipse/downloads/ (as linked to from
> www.vogella.com).
> I used the Update Manager, Help->InstallNewSoftware identifying the plugin
> from http://czt.sourceforge.net/eclipse/updates/nightly/ and then
> re-started Eclipse.
>
> Alternatively I tried downloading Eclipse IDE from
> https://www.eclipse.org/eclipseide/ that comes with more Java, Maven,
> etc, and got exactly the same results for the CZT plugins as for plain
> Eclipse 4.14..
>
> I also downloaded the pre-built czt-ide-1.6 but this doesn't run. It
> outputs an error and a configuration sub-directory log file.
> Seperately downloadingplain plain old version 4.2 (Juno) of Eclipse
> produces exactly the same error as the pre-built czt-ide-1.6.
> So I assume the 4.2 versions are no longer compatible with Windows 10,
> java 11.
>
> I did a quick scan through czt-users posts but didn't find any help there.
> I am sure there is a simple explanation and it is probably my mistake.
> I'll keep trying but Any clues?
>
> With thanks,
> julian
>
>

[CZT-Users] Eclipse 4.14 CZT plugins installation problem

[Julian R. <jro...@gm...>]

Hello,

Sorry for the newbie question but I cannot get CZT Eclipse plugins to run.
On the plus side the czt.jar from
https://sourceforge.net/projects/czt/files/czt-ide/nightly/ standalone
works perfectly well.


After downloading the latest Eclipse 4.14 and installing the CZT nightly
updates:
>From Help->About Eclipse SDK I see the CZT logo and in ->Installation
Details I see CZT-Core, CZT for Eclipse and Z/Eves Prover Integration for
CZT.
However, there is nothing else Z in Eclipse at all. No perspective. No New
CZT Project.

My windows version is 64-bit 10, 1909 updates
My jdk version is 11.0.1

I downloaded Eclipse 4.14 from
https://download.eclipse.org/eclipse/downloads/ (as linked to from
www.vogella.com).
I used the Update Manager, Help->InstallNewSoftware identifying the plugin
from http://czt.sourceforge.net/eclipse/updates/nightly/ and then
re-started Eclipse.

Alternatively I tried downloading Eclipse IDE from
https://www.eclipse.org/eclipseide/ that comes with more Java, Maven, etc,
and got exactly the same results for the CZT plugins as for plain Eclipse
4.14..

I also downloaded the pre-built czt-ide-1.6 but this doesn't run. It
outputs an error and a configuration sub-directory log file.
Seperately downloadingplain plain old version 4.2 (Juno) of Eclipse
produces exactly the same error as the pre-built czt-ide-1.6.
So I assume the 4.2 versions are no longer compatible with Windows 10, java
11.

I did a quick scan through czt-users posts but didn't find any help there.
I am sure there is a simple explanation and it is probably my mistake.
I'll keep trying but Any clues?

With thanks,
julian

[CZT-Users] Build fail with an xsd error

[Mercier J. <jme...@ge...>]

Dear,

I am trying to build czt such as:

#  git clone git://git.code.sf.net/p/czt/code

# cd code

# ./buildall.sh


Unfortunately the build fail:

[INFO] CZT Corejava Z Pattern ............................. FAILURE [  3.297 s]


Taking a look to the stacktrace :

|schema_reference.4:Failedto read schema document 'Z.xsd',because 1)could 
notfind the document;2)the document could notbe read;3)the root element 
of the document isnot<xsd:schema>.|


If I edit all xsd into :

code/corejava/corejava-circusconf/target/generated-resources/xml/xslt/

such as for each xs:import I provide the absolute full path to the 
attribute schemaLocation  the build succeed .

|Maybe use xs:include instead xs:import solve this issue.

Currently I have not yet a successful build of czt

Thanks for your help

Best regards
|

-- 

Jonathan MERCIER
Bioinformatics PhD student
Genoscope / LABGeM

[CZT-Users] serval problems for czt

[ecamy <ec...@16...>]

Hi, 


I am using the czt-ide-1.6.0.201410201751-win32.win32.x86_64(in windows8). And I install the Z-EVES2.1 in my virtual machine(in windows xp). Some troubles of launching Z/EVES is as the blow:


1. my state of Z/EVES prover is always Not available. 
2. I try to connect to my Z/EVES Remote, But always failure.
3. If i use CZT whose version is higher than 201410201751, the CZT UI can't occur in Eclipse interface.
    
So, 
1. Whether Z/EVES is really integrated in CZT or not?  
2. Is the version of Z/EVES limited to above 2.3, I only have Z/EVES 2.1, How can I do?
3. How I can find out the CZT UI in eclipse when I use higher version of CZT?


By the way, Thanks for your CZT,  The conversation to latex is so convenient for me. Thanks so much.


Best.
Emily Wang






 

[CZT-Users] serval problems for czt

[ecamy <ec...@16...>]

Hi, 


I am using the czt-ide-1.6.0.201410201751-win32.win32.x86_64(in windows8). And I install the Z-EVES2.1 in my virtual machine(in windows xp). Some troubles of launching Z/EVES is as the blow:


1. my state of Z/EVES prover is always Not available. 
2. I try to connect to my Z/EVES Remote, But always failure.
3. If i use CZT whose version is higher than 201410201751, the CZT UI can't occur in Eclipse interface.
    
So, 
1. Whether Z/EVES is really integrated in CZT or not?  
2. Is the version of Z/EVES limited to above 2.3, I only have Z/EVES 2.1, How can I do?
3. How I can find out the CZT UI in eclipse when I use higher version of CZT?


By the way, Thanks for your CZT,  The conversation to latex is so convenient for me. Thanks so much.


Best.
Emily Wang

[CZT-Users] CZT font on Mac OS X - "system validation" error

[Russell T. <rus...@me...>]

I am trying to install CZT_ 1_5_0.ttf on Mac OS X Yosemite 10.10.5 and I get
a ³serious² error: ³system validation².  How can this be fixed?

I have tried to save the font as .otf using the utility Typelight, and also
renaming the font, but neither fix the problem.

Thanks,

Russ Thomas

[CZT-Users] Cartesian product question

[Michael L. <leu...@cs...>]

Hi,

Another question concerning ZLive; shouldn’t this evaluate to true:

ZLiveDefault> eval \{\} \cross \{1\} = \nat \cross \{\}
false

(A REPL is a great way of testing a tool ;-) I used it extensively to test ProB as well ;-))
Kind regards,
Michael

PS: We did find a similar error in TLC (which has now been fixed; TLC evaluated to \{\} \cross \{1\} = \{1\} \cross \{\} false. 
Here ZLive gives the correct answer:
ZLiveDefault> eval \{\} \cross \{1\} = \{1\} \cross \{\}
true

[CZT-Users] ZLive eval questions

[Michael L. <leu...@cs...>]

HI,

I have been experimenting with the eval option of ZLive. It is nice to have a REPL where one can type in expressions and predicates.


I have a few questions concerning set comprehensions in Z / Z Live, as I may be doing something wrong.

I started ZLive like this, and many tests worked flawlessly:

$ rlwrap java -jar czt.jar zlive
ZLiveDefault> version
ZLive version 1.6-SNAPSHOT, (C) 2006, Mark Utting


1)
First, there are a few set comprehensions where ZLive complains:

ZLiveDefault> eval \# \{f : (0 \upto 1) \fun (0 \upto 1)| f(0)=0  \}
Undefined!  Mu expression has no solutions: (mu

  tmp38 == 0;                   %% tmp38=tmp37,:0..0,    
  tmp37 = tmp38;                %% tmp37:0..0,    
  %%---------------
  p{1=0} in f :: 0.0 ;          %% p={1=tmp37, 2=tmp39},    
  tmp37 = p.1;
  tmp39 = p.2                   %% tmp39:0..0,    
@ tmp39
)

According to my understanding, the equivalent B expression would be card({f| f:0..1 --> 0..1 & f(0)=1})
which is defined and whose value is 2 (you can try this out here http://stups.hhu.de/ProB/w/ProB_Logic_Calculator).
Am I missing a difference between Z and B ?
I actually assume it is related to the issue 3) below.

2)
Another example I tried was this:
ZLiveDefault> eval \{ x : \power( (0\upto 4) \cross (0\upto 4)) | \#(x)=4 \land \dom x = 1 \upto 4 \land \ran x = \{2\} \}
WARNING: changing x id from 2142 to 2182
WARNING: changing x id from 2142 to 2186
Error: Cannot generate members of SetComp: { x in x :: 1000.0 ;
tmp276 = x.1 @ tmp276 }
while evaluating&printing the result: { tmp267 == 0;                  %% tmp267:0..0,    
...
(The corresponding B expression is according to my understanding:{x|x : POW((0..4)*(0..4)) & card(x)=4 & dom(x)=1..4 & ran(x)={2}} ).


3)
Now are a few examples where I feel the result is wrong.


ZLiveDefault> eval  \{f : (0 \upto 1) \fun (0 \upto 1)| \{0 \mapsto 0\} \subseteq f  \}
\{ \{ ( 0 , 0 ) \} , \{ ( 0 , 0 ) , ( 1 , 0 ) \} , \{ ( 0 , 0 ) , ( 1 , 1 ) \} , \\
 \{ ( 0 , 0 ) , ( 1 , 0 ) , ( 1 , 1 ) \} , \{ ( 0 , 0 ) , ( 0 , 1 ) \} , \\
 \{ ( 0 , 0 ) , ( 0 , 1 ) , ( 1 , 0 ) \} , \{ ( 0 , 0 ) , ( 0 , 1 ) , ( 1 , 1 ) \} , \\
 \{ ( 0 , 0 ) , ( 0 , 1 ) , ( 1 , 0 ) , ( 1 , 1 ) \} \}
ZLiveDefault> eval  \# \{f : (0 \upto 1) \fun (0 \upto 1)| \{0 \mapsto 0\} \subseteq f  \}
8

I tried to re-code the set comprehension slightly differently, but get the same result:

ZLiveDefault> eval  \# \{f : \power((0 \upto 1) \cross (0 \upto 1))| f\in (0\upto 1) \fun (0\upto 1) \land \{0 \mapsto 0\} \subseteq f  \}
8

According to my understanding the equivalent version in B is this:

>>> card({f|f:0..1 --> 0..1 & {0|->0} <: f})
 ⇝  card({f|f ∈ 0 ‥ 1 → 0 ‥ 1 ∧ 0 ↦ 0 ∈ f})
Expression Value = 
2


To me it seems that ZLive is treating \fun, \bij, … all like \rel :

ZLiveDefault> eval  \# \{f : \power((0 \upto 1) \cross (0 \upto 1))| f\in (0\upto 1) \bij (0\upto 1)  \}
16

Indeed, I get:

ZLiveDefault> eval (0\upto 1)\fun (0\upto1)
\power ( \{ 0 , 1 \} \cross \{ 0 , 1 \} )
ZLiveDefault> eval (0\upto 1)\bij (0\upto1)
\power ( \{ 0 , 1 \} \cross \{ 0 , 1 \} )

Kind Regards,
Michael Leuschel

[CZT-Users] License on czt.sty file

[David H. <dh...@op...>]

The CZT project is licensed under GPL.   Does this apply as well to the czt.sty LaTeX style files?
No license is specified in the czt.sty file itself or in its download area.

This would seem to imply that if you create a product that, for example, prints Z-specifications using this file, you would need to license your entire project under GPL.

Is this correct?

The CZT LaTeX

--David

[CZT-Users] Support for reals in CZT

[Nuno A. <nun...@gm...>]

Hi, 

What is the current support for reals in CZT?

I believe that currently reals are not support in CZT. Is that right? 

Could you provide some guidance on having a basic support for reals in a CZT supported Z specification?

Many Thanks,

--
Nuno Amálio

[CZT-Users] Help with launching Z-Eves

[Maria U S. <acp...@sh...>]

Hi,

I have installed standalone CZT ide. However I got problem with launching
Z/Eves. I did not know what is to input in "Z/Eves executable" as well as
in "Working directory". I have tried to input the location of czt
application in my machine. But, the launching did not success.

Best,
Maria

[CZT-Users] Examples of z specifiacation

[<zar...@ya...>]

Hi,

Can you please send me examples of Z specifications on my personal e-mail zar...@ya... so that I can load them in CZT application. Any language (Standard Z, Object Z, Circus or Z Rules) or markup (Latex, UTF 8, UTF 16, XML) is fine, but I'd prefer to get one that can be animated in CZT.

Thanks in advance,
Zarko

[CZT-Users] Z Word Tools Release 3.2

[Anthony H. <an...@an...>]

Dear Z users

 

There is a new release of the Z Word Tools, Release 3.2 

 

Release 3.2 includes a tool to convert from Spivey Z to Standard Z. As well
as converting specifications in Word, this can be downloaded separately to
convert LaTeX files on any system. It can be used stand-alone or as a Java
class incorporated into other Standard-based tools.

Other changes make it easier to avoid corrupting the document structure, fix
some problems with erratic behaviour of the automatic formatting, and
improve the load/unload behaviour.

The release works with all versions of Word, including Word 2013 (currently
in preview).

The tools are available from http://sourceforge.net/projects/zwordtools/

 

I hope you find this useful. Of course, please let me know if you find any
problems.

 

Anthony

 

Anthony Hall

22 Hayward Road

Oxford OX2 8LW

UK

+44 (0) 7779 255147

 <mailto:an...@an...> an...@an... 

 <http://anthonyhall.org> http://anthonyhall.org 

 

 

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 

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

[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

Re: [CZT-Users] CZT - Looking for help with Z Live

[Yves L. <Yve...@im...>]

Dear CZters,

I have tried to answer Bernard's questions, but some problems
remain. Can you please give us some hints on the use of ZLive? Thanks!

Le 12/07/2012 23:11, Bernard Londeix a écrit :
> Dear Yves,
>
> Thank you very much for your kind introduction to ZLive. The NatVar.zed is
> running very well on my machine and this gave me a good idea about what
> should happen.
> I understand this is not your preferred tool but I would like to give a
> chance to ZLive because of the GUI associated with it. It seems to make the
> running tidier than the "Command Prompt" on my MS Windows environment.
> If later I discover that I cannot get what I need out of ZLive I will follow
> your example with Jaza.
>
> To build on the NatVar.zed success I created with Zword a very small case
> with 1 state variable and 4 Schemas. My small case doesn't work even by
> running it the same way as for NatVar.zed.
>
> I note that:
> (i) - I cannot get a file suffix .zed as you do. I am getting a .zed8. Is it
> important?
Actually my .zed file is a file in the latex format. The suffix could 
also be .tex.

It seems that .zed8 means that the file is using Unicode markup  (which 
I don't use). I guess that you should change the markup setting of zlive
by typing something like

set markup UNICODE

before you load your file.


> (ii) - my "do Schema" gives my an error message:
> Error: evaluation too difficult/large: Cannot find mode . . .

I have the same problem with the file door.zed (attached to this file).
I don't understand this error message. Maybe another member of the list 
can help us...

> (iii) - a command "set variable value" gives me unknown setting as if my
> variable were not known or defined.

The set <var> <value> only concerns the variables of zlive: markup,
section, givensetsize,... not the variables of your specification.


> (iv) - Other error (When my variable 'door' is very well declared):
> abc01> eval door = close
> term contains type errors
> "StringSource", line 1: Undeclared name: door
>
eval is aimed at evaluating expressions outside the context of
a schema. For example

ZLiveDefault> eval 1+1
2

But eval does not see the variables declared in your schemas. I guess
it is the same for evalp.

If you want to check that your door is closed, you can write a schema
like

\begin{zed}
Boolean ::= Vrai| Faux
\end{zed}

\begin{schema}
\Xi MyDoorSchema
r! : Boolean
\where
(door = close) \implies r! = Vrai\\
(door \neq close) \implies r! = Faux\\
\end{schema}

(see files door.zed and doorJaza.zed in attachment.

I am unable to run door.zed but I get the following results with Jaza:

JAZA> load doorJaza.zed
Loading 'doorJaza.zed' ...
Added 5 definitions.
JAZA> do DoorInit
\lblot door'==close \rblot
JAZA> ; EvalDoor
\lblot door'==close, r!==Vrai \rblot



> Would you know of which steps should I follow to clarify this problem?
>

I hope that some czters will help us do the same in Zlive

Sincerely yours

Yves

PS: I'll be out of office in the coming weeks
> Thanks for the guidance,
>
> Kind regards,
>
> Bernard
>
>
> -----Original Message-----
> From: Yves Ledru [mailto:Yve...@im...]
> Sent: 11 July 2012 11:36
> To: czt...@li...; blo...@te...
> Subject: Re: [CZT-Users] CZT - Looking for help with Z Live
>
> Dear Bernard,
>
> I am not so much used to CZT/ZLive. I use Jaza (the ancestor of ZLive).
> http://www.cs.waikato.ac.nz/~marku/jaza/
>
> At this point, it seems that Jaza still covers a larger subset of Z than
> ZLive.
>
> But I can try to help you to get started with ZLive.
> To illustrate the use of ZLive I'll use
> a simple specification of a natural variable which can be incremented,
> decremented,... (see attached file).
> Here are the first commands to issue.
>
> First you call ZLive:
>
> java -jar czt.jar zlive
>
> then it is good practice to do "reset"
>
> ZLiveDefault> reset
> All specifications cleared...
>
> Now you load your specification
>
> ZLiveDefault> load NatVar.zed
> Loading section NatVar
> Setting section to NatVar
>
> Use the "do" command to start an animation. Here I start it by calling the
> init operation
>
> NatVar> do XVarInit
> (I skip the warning messages)
> 1: \lblot x == 0 , x' == 0 \rblot
>
> It answers by giving the assignment of all schema variables (here x and x').
>
> You can then start from this resulting state to call an operation. This is
> done by using ";" followed by the name of the schema. Let us increment x...
>
> NatVar> ; XVarInc
> 1: \lblot x == 0 , x' == 1 \rblot
>
> Let us do it a second time
>
> NatVar> ; XVarInc
> 1: \lblot x == 1 , x' == 2 \rblot
>
>
> I add some difficulties to call an operation with input and output
> parameters (in Jaza you simply call ; XVarAdd [i? := 5]) , finally, I found
> the following solution based on schema conjunction (maybe ZLive experts can
> point to a simpler way to assign values to input parameters):
>
> NatVar> ; XVarAdd \land [i? : \num \where i? = 5]
> 1: \lblot x == 2 , x' == 7 , i? == 5 , r! == 7 \rblot
>
> Finally to close these examples, let us restart from the init state and try
> to decrement natural variable x
>
> NatVar> do XVarInit
> 1: \lblot x == 0 , x' == 0 \rblot
> NatVar> ; XVarDec
> no more solutions
>
> Which says that it does not find solutions (because x may not take negative
> values).
>
> I hope this helps getting started with ZLive. (you might want to do the same
> with Jaza, but for Jaza you need to change the init operation as follows:
>
> \begin{schema}{XVarInit}
> \Delta XVar
> \where
> x' = 0
> \end{schema}
>
> Sincerely yours
>
> Yves
>
> Le 09/07/2012 23:36, Bernard Londeix a écrit :
>> Dear Sir,
>>
>> I am trying to animate a very small Z specification which is type
>> checked correctly with Z Word.
>>
>> Unfortunately I am getting nowhere with Z Live. This is probably due
>> to my not understanding correctly the Help. See below:
>>
>> Would you have a user guide for real beginners?
>>
>> What are the 3 or 4 first commands to issue to CZT Live in order to
>> Animate a small specification?
>>
>> Thanks,
>>
>> Best regards,
>>
>> *Bernard Londeix*
>>
>> ----------------------------------------------------------------------
>> -----
>>
>> *Telmaco Ltd*
>>
>> *M: +44 7768 588 419*
>>
>> *E: blo...@te... <mailto:blo...@te...>*
>>
>> *Em: blo...@ho... <mailto:blo...@ov...>*
>>
>> *IM: SkypeName:  bernard.londeix*
>>
>> *W: http://www.telmaco.co.uk <http://www.telmaco.co.uk/>*
>>
>> *Tw: http://www.twitter.com/Telmaco*
>>
>> *Tw: http://www.twitter.com/MeterIT*
>>
>> ----------------------------------------------------------------------
>> -----
>>
>> **
>>
>> --------------- ZLive Commands ---------------
>>
>> load file.tex     -- Read a Z specification into ZLive
>>
>> eval <expr>       -- Evaluate an expression
>>
>> evalp <pred>      -- Evaluate a predicate (synonym for eval)
>>
>> do <expr>         -- Evaluate a schema/set and show one member
>>
>> next/curr/prev    -- Show next/current/previous state of a schema/set
>>
>> ; schemaExpr      -- Compose the current state with schemaExpr
>>
>> undo              -- Undo the last 'do' or ';' command.
>>
>> why               -- Show the internal code of the last do or ';' command
>>
>> set               -- Show all current settings
>>
>> set <var> <value> -- Sets <var> to <value>.
>>
>> show              -- Show name & type of defns in current section
>>
>> conjectures       -- Evaluate all conjectures in the current section
>>
>> reset             -- Remove all loaded specifications
>>
>> version           -- Display the version of ZLive
>>
>> help              -- Display this help summary
>>
>> quit              -- Exit the ZLive program
>>
>>     env             -- Show internal defn/operator tables
>>
>>     unfold term     -- Show term after initial unfolding (debug)
>>
>>     apply rule expr -- Try to rewrite expr using rule (debug)
>>
>> --------------- End of ZLive Commands ---------------
>>
>>
>>
>> ----------------------------------------------------------------------
>> --------
>> Live Security Virtual Conference
>> Exclusive live event will cover all the ways today's security and
>> threat landscape has changed and how IT managers can respond.
>> Discussions will include endpoint security, mobile security and the
>> latest in malware threats.
>> http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
>>
>>
>>
>> _______________________________________________
>> CZT-Users mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-users
>>
>
>
> --
>    ___ Yves LEDRU _______________________________________________________
> | Professeur à l'Université Joseph Fourier (Grenoble-1)
> | LIG, Domaine Universitaire, BP 72,         Tel: + 33 4 76 82 72 16
> | F-38402 St Martin D'Heres Cedex            e-mail: Yve...@im...
> | FRANCE                http://www-lsr.imag.fr/Les.Personnes/Yves.Ledru
> |______________________________________________________________________
>
>
>


-- 
  ___ Yves LEDRU _______________________________________________________
| Professeur à l'Université Joseph Fourier (Grenoble-1)
| LIG, Domaine Universitaire, BP 72,         Tel: + 33 4 76 82 72 16
| F-38402 St Martin D'Heres Cedex            e-mail: Yve...@im...
| FRANCE                http://www-lsr.imag.fr/Les.Personnes/Yves.Ledru
|______________________________________________________________________

Re: [CZT-Users] CZT - Looking for help with Z Live

[Yves L. <Yve...@im...>]

Dear Bernard,

I am not so much used to CZT/ZLive. I use Jaza (the ancestor of ZLive).
http://www.cs.waikato.ac.nz/~marku/jaza/

At this point, it seems that Jaza still covers a larger subset of Z than
ZLive.

But I can try to help you to get started with ZLive.
To illustrate the use of ZLive I'll use
a simple specification of a natural variable which can be
incremented, decremented,... (see attached file).
Here are the first commands to issue.

First you call ZLive:

java -jar czt.jar zlive

then it is good practice to do "reset"

ZLiveDefault> reset
All specifications cleared...

Now you load your specification

ZLiveDefault> load NatVar.zed
Loading section NatVar
Setting section to NatVar

Use the "do" command to start an animation. Here I start it by calling 
the init operation

NatVar> do XVarInit
(I skip the warning messages)
1: \lblot x == 0 , x' == 0 \rblot

It answers by giving the assignment of all schema variables (here
x and x').

You can then start from this resulting state to call an operation. This
is done by using ";" followed by the name of the schema. Let us 
increment x...

NatVar> ; XVarInc
1: \lblot x == 0 , x' == 1 \rblot

Let us do it a second time

NatVar> ; XVarInc
1: \lblot x == 1 , x' == 2 \rblot


I add some difficulties to call an operation with input and output 
parameters (in Jaza you simply call ; XVarAdd [i? := 5]) ,
finally, I found the following solution based on schema conjunction
(maybe ZLive experts can point to a simpler way to assign values to
input parameters):

NatVar> ; XVarAdd \land [i? : \num \where i? = 5]
1: \lblot x == 2 , x' == 7 , i? == 5 , r! == 7 \rblot

Finally to close these examples, let us restart from the init
state and try to decrement natural variable x

NatVar> do XVarInit
1: \lblot x == 0 , x' == 0 \rblot
NatVar> ; XVarDec
no more solutions

Which says that it does not find solutions (because x may not
take negative values).

I hope this helps getting started with ZLive. (you might want
to do the same with Jaza, but for Jaza you need to change
the init operation as follows:

\begin{schema}{XVarInit}
\Delta XVar
\where
x' = 0
\end{schema}

Sincerely yours

Yves

Le 09/07/2012 23:36, Bernard Londeix a écrit :
> Dear Sir,
>
> I am trying to animate a very small Z specification which is type
> checked correctly with Z Word.
>
> Unfortunately I am getting nowhere with Z Live. This is probably due to
> my not understanding correctly the Help. See below:
>
> Would you have a user guide for real beginners?
>
> What are the 3 or 4 first commands to issue to CZT Live in order to
> Animate a small specification?
>
> Thanks,
>
> Best regards,
>
> *Bernard Londeix*
>
> ---------------------------------------------------------------------------
>
> *Telmaco Ltd*
>
> *M: +44 7768 588 419*
>
> *E: blo...@te... <mailto:blo...@te...>*
>
> *Em: blo...@ho... <mailto:blo...@ov...>*
>
> *IM: SkypeName:  bernard.londeix*
>
> *W: http://www.telmaco.co.uk <http://www.telmaco.co.uk/>*
>
> *Tw: http://www.twitter.com/Telmaco*
>
> *Tw: http://www.twitter.com/MeterIT*
>
> ---------------------------------------------------------------------------
>
> **
>
> --------------- ZLive Commands ---------------
>
> load file.tex     -- Read a Z specification into ZLive
>
> eval <expr>       -- Evaluate an expression
>
> evalp <pred>      -- Evaluate a predicate (synonym for eval)
>
> do <expr>         -- Evaluate a schema/set and show one member
>
> next/curr/prev    -- Show next/current/previous state of a schema/set
>
> ; schemaExpr      -- Compose the current state with schemaExpr
>
> undo              -- Undo the last 'do' or ';' command.
>
> why               -- Show the internal code of the last do or ';' command
>
> set               -- Show all current settings
>
> set <var> <value> -- Sets <var> to <value>.
>
> show              -- Show name & type of defns in current section
>
> conjectures       -- Evaluate all conjectures in the current section
>
> reset             -- Remove all loaded specifications
>
> version           -- Display the version of ZLive
>
> help              -- Display this help summary
>
> quit              -- Exit the ZLive program
>
>    env             -- Show internal defn/operator tables
>
>    unfold term     -- Show term after initial unfolding (debug)
>
>    apply rule expr -- Try to rewrite expr using rule (debug)
>
> --------------- End of ZLive Commands ---------------
>
>
>
> ------------------------------------------------------------------------------
> Live Security Virtual Conference
> Exclusive live event will cover all the ways today's security and
> threat landscape has changed and how IT managers can respond. Discussions
> will include endpoint security, mobile security and the latest in malware
> threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
>
>
>
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users
>


-- 
  ___ Yves LEDRU _______________________________________________________
| Professeur à l'Université Joseph Fourier (Grenoble-1)
| LIG, Domaine Universitaire, BP 72,         Tel: + 33 4 76 82 72 16
| F-38402 St Martin D'Heres Cedex            e-mail: Yve...@im...
| FRANCE                http://www-lsr.imag.fr/Les.Personnes/Yves.Ledru
|______________________________________________________________________

[CZT-Users] CZT - Looking for help with Z Live

[Bernard L. <blo...@te...>]

Dear Sir,

 

I am trying to animate a very small Z specification which is type checked
correctly with Z Word. 

Unfortunately I am getting nowhere with Z Live. This is probably due to my
not understanding correctly the Help. See below:

Would you have a user guide for real beginners?

What are the 3 or 4 first commands to issue to CZT Live in order to Animate
a small specification?

 

Thanks,

Best regards,

 

Bernard Londeix 

---------------------------------------------------------------------------

Telmaco Ltd

M: +44 7768 588 419

E:  <mailto:blo...@te...> blo...@te...

Em:  <mailto:blo...@ov...> blo...@ho...

IM: SkypeName:  bernard.londeix

W:  <http://www.telmaco.co.uk/> http://www.telmaco.co.uk

Tw:  <http://www.twitter.com/Telmaco> http://www.twitter.com/Telmaco

Tw:  <http://www.twitter.com/MeterIT> http://www.twitter.com/MeterIT

---------------------------------------------------------------------------

 

 

--------------- ZLive Commands ---------------

load file.tex     -- Read a Z specification into ZLive

eval <expr>       -- Evaluate an expression

evalp <pred>      -- Evaluate a predicate (synonym for eval)

do <expr>         -- Evaluate a schema/set and show one member

next/curr/prev    -- Show next/current/previous state of a schema/set

; schemaExpr      -- Compose the current state with schemaExpr

undo              -- Undo the last 'do' or ';' command.

why               -- Show the internal code of the last do or ';' command

set               -- Show all current settings

set <var> <value> -- Sets <var> to <value>.

show              -- Show name & type of defns in current section

conjectures       -- Evaluate all conjectures in the current section

reset             -- Remove all loaded specifications

version           -- Display the version of ZLive

help              -- Display this help summary

quit              -- Exit the ZLive program

  env             -- Show internal defn/operator tables

  unfold term     -- Show term after initial unfolding (debug)

  apply rule expr -- Try to rewrite expr using rule (debug)

--------------- End of ZLive Commands ---------------

 

[CZT-Users] define a lattice in Object-Z

[Janine S. <ma...@ja...>]

Hello, 

I am writing an Object-Z specification in latex and want to define a lattice. 
Could someone please look at the example below and tell me if this is correct?


\begin{class}{Test}
\\
\begin{state}
r :  \mathbb{P} \ ROLE\\
rh: (r, \geq)
\ST
rh : nurse \geq doctor  \geq chief physician
\end{state} \\
\begin{init}
r = \left\{nurse, doctor, chief physician\right\}\\
rh = \left\{(nurse, doctor), (doctor, chief physician)\right\}
\end{init} \\
\end{class}

r : set of roles in a hospital 
RH : role hierarchy in a hospital (lattice)


Thanks a lot for your help!





Kind regards, 

Janine

Re: [CZT-Users] typchecking oz error mesages + convert oz to java/c++

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

Hi Janine,

Sure. Decidability is not a small topic, and it is not one that I have a 
good handle on myself. Basically, Object-Z is built on a first-order 
logic that is not decidable. This means that there is no algorithm than 
can determine whether an Object-Z predicate is true or not, for all 
Object-Z predicates. There are algorithms that can determine that *some* 
predicates are true, but it is impossible that an algorithm can 
determine this for all predicates in the language. You can read about 
decidability on wikipedia: http://en.wikipedia.org/wiki/Decidability_(logic)

The consequence for you is that, if we cannot determine whether some 
predicates are true, then automatically translating such predicates into 
programs that terminate would also be impossible.

I hope that helps.

Regards,
Tim

On 01/06/12 07:34, Janine Seifert wrote:
> Hi Tim,
> thanks a lot for the quick and useful reply. I did not got the point
> regarding the undecidability of Object-Z. Could you please explain this
> more in detail or point me to a resource that could help me in
> understanding it.
> Regards,
> Janine
>
>     ----- Original Message -----
>     *From:* Tim Miller <mailto:tm...@un...>
>     *To:* Janine Seifert <mailto:ma...@ja...>
>     *Cc:* czt...@li...
>     <mailto:czt...@li...>
>     *Sent:* Thursday, May 31, 2012 3:45 AM
>     *Subject:* Re: [CZT-Users] typchecking oz error mesages + convert oz
>     to java/c++
>
>     Hi Janine,
>
>      > I am a beginner in OZ and the CZT eclipse plugin. I am writing an
>      > Object-Z specification in latex, but the typchecker reports some
>     errors.
>      > Could someone please explain me the error messages?
>      >
>     The CZT tools (including the Object-Z ones) are based on the Z
>     standard.
>     Much of the Object-Z literature was written prior to the Z standard, so
>     there are some catches that you'll have to be aware of.
>
>     The errors you see are:
>
>     - There is no "\real" set in standard Z. You can create one using:
>
>     %%Zword \real real
>
>     \begin{axdef}
>     \real : \power \arithmos
>     \end{axdef}
>
>     The first line tells the parser some stuff, and the paragraph below
>     declares \real as a power set of 'arithmos' -- the base numbers in
>     standard Z.
>
>     - The problem with the 'colour' variable is that all paragraphs in an
>     Object-Z specification must be declared as standard Z paragraphs. So
>     you'll need to use an axdef for that the same way that you did for the
>     variable 'perim'.
>
>     Fixing these results in another problem: you'll need a '\where' symbol
>     between the line that declares dx? and dy?, and the predicate that uses
>     them.
>
>      > Am I right that the CTZ Tools are not able to convert the OZ code to
>      > Java/C++ ? If thats the case, could you point me to a tool or lib
>     that
>      > is able to accomplish that task? I not only need to typecheck my
>     OZ code
>      > but also have to convert it to C++ code/classes.
>      >
>     You're right that CZT doesn't do this. I've not heard of a tool that
>     does, and in any case, the conversion would be highly restricted
>     because
>     Object-Z is undecidable.
>
>     I hope this helps.
>
>     Regards,
>     Tim

Re: [CZT-Users] typchecking oz error mesages + convert oz to java/c++

[Janine S. <ma...@ja...>]

Hi Tim, 

thanks a lot for the quick and useful reply. I did not got the point regarding the undecidability of Object-Z. Could you please explain this more in detail or point me to a resource that could help me in understanding it.

Regards, 
Janine



  ----- Original Message ----- 
  From: Tim Miller 
  To: Janine Seifert 
  Cc: czt...@li... 
  Sent: Thursday, May 31, 2012 3:45 AM
  Subject: Re: [CZT-Users] typchecking oz error mesages + convert oz to java/c++


  Hi Janine,

  > I am a beginner in OZ and the CZT eclipse plugin. I am writing an
  > Object-Z specification in latex, but the typchecker reports some errors.
  > Could someone please explain me the error messages?
  >
  The CZT tools (including the Object-Z ones) are based on the Z standard. 
  Much of the Object-Z literature was written prior to the Z standard, so 
  there are some catches that you'll have to be aware of.

  The errors you see are:

  - There is no "\real" set in standard Z. You can create one using:

  %%Zword \real real

  \begin{axdef}
     \real : \power \arithmos
  \end{axdef}

    The first line tells the parser some stuff, and the paragraph below 
  declares \real as a power set of 'arithmos' -- the base numbers in 
  standard Z.

  - The problem with the 'colour' variable is that all paragraphs in an 
  Object-Z specification must be declared as standard Z paragraphs. So 
  you'll need to use an axdef for that the same way that you did for the 
  variable 'perim'.

  Fixing these results in another problem: you'll need a '\where' symbol 
  between the line that declares dx? and dy?, and the predicate that uses 
  them.

  > Am I right that the CTZ Tools are not able to convert the OZ code to
  > Java/C++ ? If thats the case, could you point me to a tool or lib that
  > is able to accomplish that task? I not only need to typecheck my OZ code
  > but also have to convert it to C++ code/classes.
  >
  You're right that CZT doesn't do this. I've not heard of a tool that 
  does, and in any case, the conversion would be highly restricted because 
  Object-Z is undecidable.

  I hope this helps.

  Regards,
  Tim