## Why the Object-Z specification is invalid?

Help
2013-11-05
2014-05-21

• Daijie Zhang
2013-11-05

Dear ：

I'm now using the CZT to produce a Z specification for a few days, but I have a few problems. I have installed the software in accordance with the method of http://www.cs.waikato.ac.nz/~marku/czt/eclipse.html. But when I write the z specifications, I found the color of part of the file is red and it is invalid. Meanwhile, when I write the object-z specifications, the color of the entire file is red. For example, a schema of “GENTBL”, the color of 1,2,3,13 line is red. And a class “GENTBL1”, the color of 1 to 14 lines is red. I hope you could help me .There are two examples.
Example 1:

1 \documentclass{article}

2 \usepackage{oz} % oz or z-eves or fuzz styles

3 \begin{document}

4 \begin{zsection}

5 \SECTION GENTBL \parents standard_toolkit

6 \end{zsection}

7 \begin{schema}{GENTBL}[ K,D ]

8 keys: \finset K \

9 tbl: K \ffun D

10 \where

11 keys=\dom tbl

12 \end{schema}

13 \end{document}

Examle 2:

1 \documentclass{article}

2 \usepackage{oz} % oz or z-eves or fuzz styles

3 \begin{document}

4 \begin{class}{GENTBL1}

5 \project ( INIT , TBLContainsKey , AddTBLEntry , GetTBLEntry , DelTBLEntry , OverwriteTBLEntry )\

7 \begin{state}

8 keys: \finset K \

9 tbl: K \ffun D

10 \where

11 keys=\dom tbl

12 \end{state}

13 \end{class}

14 \end{document}

Kind regards

Daijie Zhang

2013.11.5

Last edit: Daijie Zhang 2013-11-05
• Hi Daijie Zhang,

Which CZT Eclipse version did you use? The one from Mark's website that you indicated or the latest CZT Eclipse release? The newest versions are available from the official CZT website at http://czt.sourceforge.net/eclipse/download.html. You can find a bit more information about CZT Eclipse at http://czt.sourceforge.net/eclipse/.

Also, I tried the first specification example - there are a couple typos there. First, the underscore symbol in LaTeX must be typeset as \_ (escaped with backslash). So it should be standard\_toolkit in line 5. Also, line 8 is missing a newline backslash: it should end with \\, not just \. With these fixed, the whole specification compiles successfully for me..

Do you still get the error with the latest CZT version and these fixes?

• Daijie Zhang
2013-11-06

Dear ：
Thank you for your help. With your help, about "\" and "_" mistakes corrected. But some problems is still there.

I also installed the latest CZT Eclipse version, but the new version of the CZT still can't check object-Z error, all object-Z grammar is invalid.The color of The first few lines and last few lines of article is still red. For example,"\documentclass{article}"," \usepackage{oz} % oz or z-eves or fuzz styles" and "\begin{document}","\end{document}".

Therefore, I want to ask, whether CZT support object-Z? If I want to write specification about object-Z and let the red content effectively in my article, whether I need to install other things, such as "plugins", "LATEX" environment, or "macro package". Hope you could give me some advice again. Looking forward to your reply.

Kind regards
Daijie Zhang
2013.11.6

Last edit: Daijie Zhang 2013-11-06

• Leo Freitas
2013-11-06

Hi,

Perhaps I could help by saying that the Eclipse extension is mostly for Z.

Object Z tools are well developed for the command line, and a bit within Eclipse
and jEdit frontends. But please set your expectations right: OZ on Eclipse is not even
experimental yet. Would you be interested in contributing?

Best,
Leo

On 6 Nov 2013, at 14:54, Daijie Zhang zhangdaijie@users.sf.net
wrote:

Dear ：
Thank you for your help. With your help, about "\" and "_" mistakes corrected. But some problems is still there.

I also installed the latest CZT Eclipse version, but the new version of the CZT still can't check object-Z error, all object-Z grammar is invalid.The color of The first few lines and last few lines of article is still red. For example,"\documentclass{article}"、
" \usepackage{oz} % oz or z-eves or fuzz styles" and "\begin{document}"、"\end{document}"

Therefore, I want to ask, whether CZT support object-Z? If I want to write specification about object-Z and let the red content effectively in my article, whether I need to install other things, such as "plugins", "LATEX" environment, or "macro package". Hope you could give me some advice again. Looking forward to your reply.

Kind regards
Daijie Zhang
2013.11.6

Why the Object-Z specification is invalid?

Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-11-07

Hi,

Thanks for you help, I have solve my problems.

Kind regards
Daijie Zhang
2013.11.7

• Hi,

You need to select Object-Z dialect within CZT Eclipse - in Preferences > CZT > Compiler. If I remember correctly, Object-Z dialect is "oz". See the help page for more details. By default, the "z" dialect is used. Also remember to reload the open editors after switching the dialect.

With the correct dialect, are you still getting the problems? If so, could you attach a minimal example? Because the first example you posted is parsed and checked correctly for me.

Also, if you get an error, could you tell us what it says? Either hover your mouse over the error - the error will be displayed in the tooltip, or use the Problems view to see the list of errors.

Let us know how it goes!

• Daijie Zhang
2013-11-07

Dear,

With the correct dialect, I have solve the problems. Thanks !

Kind regards
Daijie Zhang
2013.11.7

• Daijie Zhang
2013-11-19

Dear,

With the help of you , I have successfully wrote some specification with the latest version CZT Eclipse that you told me. But I met a problem again recently, I hope you could help me again.

When I write the specification use the " forward declaration" of a variable . I know the specification is right ,but the latest version CZT Eclipse reports an error, ,the old version will not reports the error . I don't know the reason.

There is a picture about the error .
Kind regards
Daijie Zhang

Last edit: Daijie Zhang 2013-11-19
Attachments
• Hi,

Can you try checking the property PROP_TYPECHECK_RECURSIVE_TYPES in the Z compiler preferences?

Remember to restart the editor after changing the property. Does this solve your problem?

Sorry for the delay in replying.

• Daijie Zhang
2013-11-21

Dear ,

I am glad to receive you reply . Before I write the last mail , I have tried the property PROP_TYPECHECK_RECURSIVE_TYPES , but it is valid . I also compare the difference between the old version and new version , I found the old version is different , it is the property PROP_TYPECHECK_USE_BEFORE_DECL ,it is valid.

Why is it? Could you tell me ?

There are two pictures about the difference.

Kind regards
Daijie Zhang

Last edit: Daijie Zhang 2013-11-21
Attachments
• Hi,

Can you attach your specification file to test ourselves?

• Daijie Zhang
2013-11-21

This is the specification file .

Attachments
• Hi,

Thanks - this is a bug. I can reproduce it on my system. The problem is that the compiler options were not applied correctly.. Thanks for reporting it. We do not test Object-Z that much, so any help is appreciated here :)

I have fixed this bug now. You need to update CZT Eclipse - you can either download the latest version again, or use Help > Check for Updates in CZT Eclipse.

Let us know how it goes!

• Daijie Zhang
2013-11-22

Dear,

Thanks for your help, I will update CZT Eclipse.

Best,
Daijie Zhang

• Leo Freitas
2013-11-21

Hi,

Firstly, Daijie these names were adjusted to be more meaningful to users and
be uniform across the implementation.

Secondly, why do you need use before declaration? It should work fine. Have you
tried the command line tool? It should work fine there. Remember that the CZT Eclipse
for Object-Z is barely developed. Would you like to be involved extending it?

Best,
Leo

On 21 Nov 2013, at 07:01, Daijie Zhang zhangdaijie@users.sf.net<mailto:zhangdaijie@users.sf.net> wrote:

Dear ,

I am glad to receive you reply . Before I write the last mail , I have tried the property PROP_TYPECHECK_RECURSIVE_TYPES , but it is valid . I also compare the difference between the old version and new version , I found the old version is different , it is the property PROP_TYPECHECK_USE_BEFORE_DECL ,it is valid.

Why is it? Could you tell me ?

There are two pictures about the difference.

Kind regards
Daijie Zhang

Why the Object-Z specification is invalid?https://sourceforge.net/p/czt/discussion/295268/thread/e8c556d5/?limit=25#0d5d

Sent from sourceforge.nethttp://sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-11-21

Dear:

Thanks for you reply . But I am sorry to say that I don't know how to use the the command line tool . So I want to ask , Where I can load the tool and study the use of this tool , or whether you can say more thing about the tool?

Best,
Daijie Zhang

Last edit: Daijie Zhang 2013-11-21

• Leo Freitas
2013-11-21

Hi,

It’s straightforward:

assuming czt.jar is in some directory, if go to a terminal / cmd-prompt window and type

java -jar czt.jar —help
java -jar czt.jar ozedtypecheck -help

You get all information you need to use the tools.

Best
Leo

On 21 Nov 2013, at 13:30, Daijie Zhang zhangdaijie@users.sf.net<mailto:zhangdaijie@users.sf.net> wrote:

Dear:

Thanks for you reply . But I am sorry to say that I don't know how use the the command line tool . So I want to ask , Where I can load the tool or whether you can say more thing about the tool?

Best,
Daijie Zhang

Why the Object-Z specification is invalid?https://sourceforge.net/p/czt/discussion/295268/thread/e8c556d5/?limit=25#0d5d/30f6/ae86

Sent from sourceforge.nethttp://sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-11-22

Dear,

Thanks for your help, if I can't solve mp problem ,I will learn it.

Best,
Daijie Zhang

• Daijie Zhang
2013-11-22

Dear,

I have try the method that you told me after load the czt_1_5_0_bin.jar .But there is an error "Unable to access jarfile czt.jar". Why is it ? Could you tell me ?

Best,
Daijie Zhang

• Leo Freitas
2013-11-22

Dajie,

You need to get the latest version of CZT. Or else build it from sources,
which was what I assumed you would do given you said you had interest
in implementing Eclipse Object-Z?

Leo

On 22 Nov 2013, at 09:00, Daijie Zhang zhangdaijie@users.sf.net wrote:

Dear,

I have try the method that you told me after load the czt_1_5_0_bin.jar .But there is an error "Unable to access jarfile czt.jar". Why is it ? Could you tell me ?

Best,
Daijie Zhang

Why the Object-Z specification is invalid?

Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Hi Daijie,

If you really want to use czt.jar, pick up the latest version from Sourceforge. Version 1.5.0 is very old :) though, sadly, it is still the last "official" release. Current updates are available as nightly builds.

But I would first suggest using CZT Eclipse, as I mentioned earlier. I have fixed the bug you reported, so try using updating CZT Eclipse and see if your problem has gone away.

• Daijie Zhang
2013-11-22

Dear,

First,I have solved the last problem by getting the latest version of CZT. But I found a new problem .

You can see the two pictures. In the latest version, when I use the operation of "Init" ,I found I must put it in the final , otherwise, there will be an error , such as Fig1 and Fig2. It is right in the old version whether front and final. In this example , the order of ".\Init" has no influence to the specification . But sometimes , I must let the ".\Init" before other operations . So I don't know whether it is the problem of tool or my own problem. I hope you can help me .

There are the pictures and the specification.

Best,
Daijie Zhang

Last edit: Daijie Zhang 2013-11-22
Attachments

• Leo Freitas
2013-11-22

Daijie,

Out of interest, what led you to use Object-Z?

I don’t know OZ much, but the best thing to do is to look at the ObjectZ grammar in the parser
as it is what is acceptable. Another (easier) source are examples within the type checker and

Leo

On 22 Nov 2013, at 12:54, Daijie Zhang zhangdaijie@users.sf.net wrote:

Dear,

First,I have solved the last problem by getting the latest version of CZT. But I found a new problem .

You can see the two pictures. In the latest version, when I use the operation of "Init" ,I found I must put it in the final , otherwise, there will be an error , such as Fig1 and Fig2. It is right in the old version. In this example , the order of ".\Init" has no influence to the specification . But sometimes , I must let the ".\Init" before other operations . So I don't know whether it is the problem of tool or my own problem.

There are the pictures and the specification.

Best,
Daijie Zhang

Why the Object-Z specification is invalid?

Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-11-25

Dear,

Do you see my problem?

• Hi,

Sorry - I don't know Object-Z either, so I am not sure if that is a problem, how it should actually be and how to solve it at the moment. Maybe other CZT developers will find this thread who are better placed to answer.

• Daijie Zhang
2013-11-26

Dear,

Thanks, you have helped me a lot .Hope that other developers can help to me.

Best,
Daijie

• Daijie Zhang
2013-11-22

Dear,

Thanks, I think I would more likely to use the Eclipse Object-Z . thanks again.

Best,
Daijie Zhang

• Daijie Zhang
2013-12-04

Hi,

I am sorry to trouble you again . When I use the Z/EVES in the CZT , I click the button "Show Theorems" ,But it said " The Z/EVES prover is not connected " . Why ? Could you tell me how to solve the problems.

Best

• Leo Freitas
2013-12-04

Z/EVES is a separate tool that you need access, but it is no longer
distributed, so you would need to find someone who has it and can share it.

Also, it does not handle Object-Z

Best,
Leo

On 4 Dec 2013, at 14:05, Daijie Zhang zhangdaijie@users.sf.net wrote:

Hi,

I am sorry to trouble you again . When I use the Z/EVES in the CZT , I click the button "Show Theorems" ,But it said " The Z/EVES prover is not connected " . Why ? Could you tell me how to solve the problems.

Best

Why the Object-Z specification is invalid?

Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-12-05

Dear,

Thanks very much. Do you mean I must install the Z/EVES ? And Where can I find how to use the Z/EVES in CZT ? Could you tell me more ?

Best,
Daijie

• Leo Freitas
2013-12-05

Hi

In The message I say ZEVES is an external tool no longer distributed :-).
So, if you don’t have it, it’s hard to find it. Although some sites put it up online.

What are you trying to do? What is your project / interest in CZT and Z/EVES?

Leo

On 5 Dec 2013, at 02:30, Daijie Zhang zhangdaijie@users.sf.net wrote:

Dear,

Thanks very much. Do you mean I must install the Z/EVES ? And Where can I find how to use the Z/EVES in CZT ? Could you tell me more ?

Best,
Daijie

Why the Object-Z specification is invalid?

Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-12-05

Dear,

Thanks very much .I am try to prove the validity of the code.

Best,
Daijie

Last edit: Daijie Zhang 2013-12-05

• Daijie Zhang
2013-12-05

Dear,

Thanks very much .

Best,
Daijie

• Daijie Zhang
2013-12-09

Dear,

Now , I am trying to verify my specification by proving the theorems which the CZT Automatically generate in the "verification" .I used to think that if I want to verify it , I must connect z/eves. But my teacher said, CZT should have its own validation rules .So I have to trouble you again .

Whether does the CZT has its own validation rules ? And where can I study the rules and process of proof. Are there examples?

Hope you can help me again .Looking forward to your reply .

Best,
Daijie

Last edit: Daijie Zhang 2013-12-09

• Leo Freitas
2013-12-09

Daijie,

This way it will be easier to answer some of your questions below.

Best,
Leo

On 8 Dec 2013, at 21:15, Daijie Zhang zhangdaijie@users.sf.net wrote:

Dear,

Now , I am trying to verify my specification by proving the theorems which the CZT Automatically generate in the "verification" .I used to think that if I want to verify it , I must connect z/eves. But my teacher said, CZT should have its own validation rules .So I have to trouble you again .

Whether does the CZT has its own validation rules ? And where can I study the rules and process of proof.

Hope you can help me again .Looking forward to your reply .

Best,
Daijie

Why the Object-Z specification is invalid?

Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Hi Daijie,

Can it be that your teacher was talking about the Rules package of CZT? I think it was an attempt to provide transformation/theorem proving rules for CZT - I am not too sure about its current state. As you can see, there is not much info about it - just the Javadoc, I guess. I am not very familiar with this CZT development.

The Verification view in CZT Eclipse could be considered standalone, i.e. it generates the proof obligations that could eventually be proved in different manner. The current support in CZT Eclipse is for Z/EVES theorem prover only (which you need to have available), the Rules package is not supported in CZT for Eclipse - you will need to use the command line tools for that (I think).

• Daijie Zhang
2013-12-12

Dear，

Thanks very much .I think I would like to use Z/EVES in CZT eclipse。

As I wrote in the reply to Leo , I had encountered a problems when tried to connect to the Z/EVES.

The question is like this .I have load the Z/EVES 2.1 ,(z-eves-pc-windows-acl-2.1.exe,) . And I try to connect to Z/eves follow the method in “help—help contents—czt user guide—Getting started—Z/EVES proofs”(my computer is win-7,32 bit) and it’s name is “New_configuration”. But every time progress to 57% , it will pop up a message box of “connect to Z/EVES sever, retry ?”. When I choose “retry” , it will keep on popping up the message box . But when I choose “Run – External Tools -- New_configuration” , it pop up the message box of “Only a single Z/eves prover can be running at any time – stop the running prover before launching a new one “

It has troubled me for a long time , I tried to modify the port , but it also is wrong .

I doubt it is problem of version .Maybe my Z/EVES version is too old . If it is , Could you give me a new version ?(I have looking for a long time , but didn’t find it ) . If it isn’t , Could you give me some advice ?

There is a picture of my configurations.

Best,
Daijie

Attachments
• Hi - sorry for a very late reply.

I think you are doing everything ok with the configuration. However, I think you need to install Z/EVES first. The z-eves-pc-windows-acl-2.1.exe file is an installer - extract it and try installing Z/EVES on your machine using SETUP.exe. After installing you will need to indicate <ZEVES install dir>/system/z-eves-pc-windows-lispworks.exe as the executable in the configuration.

Let me know how it goes!

• Daijie Zhang
2013-12-23

Dear,

I am also sorry to reply late. Thanks very much. Now I know where I went wrong. But I still cant connection successful. I think this maybe my own error . Does the port have requirement?

Finally, thanks for always help me .

Best ,
Daijie

• Lomesh Meshram
2014-05-16

But SETUP.exe file not executing. Also SETUP.exe file is too old year 1997.
What is the problem?

• Lomesh Meshram
2014-05-16

Hi,
I'm unable to find the executable and working directory while launching
Z/Eves. How did u get this two?

• Daijie Zhang
2013-12-09

Dear，

I'm very sorry didn't make it clear.

My teacher let me to learn about the knowledge of formal verification through the verification of a simple kernel code. This is my thought .First I want to translate the C code into Z or Object-Z form, then I can prove the correctness of Z or Object-Z specification to judge the correctness of the original code. If the specification has Redundant and inconsistent error , I can say the code also has the sample error .And ,I think maybe I can prove the correctness of specification by proving the theorems automatically generate in the " Z verification".

Before, I have been learning about Z and OZ. Now has begun to enter the verification phase.If I want to finish the verification ,I must known the verification rules of the tool that my use.For example there are five proof rules(formule) in the Z/EVES, “ Reduction ，Case， Quantifiers , Normal Forms ,and Equality ".

So what I want to ask is , Whether does the CZT has its own validation rules(formule) ? And where can I study the rules and process of proof? Are there examples?

Do you think my idea about the work is correct ?

Best,
Daijie

There are a picture of the theorems that I want to prove .

Attachments

• Leo Freitas
2013-12-11

Hi

Okay, I understand it better now. You have a tall order in front of you. And I don't yet understand your rationale of choice for z or oz.

Theorem proving is a tricky / difficult subject, but it's a great one too.

I don't yet follow
What you mean by "rules" or what is it you are trying to prove. Could you state the theorems formally? If not, could you state what you would like to prove in English?

Best
Leo

On 9 Dec 2013, at 09:36, "Daijie Zhang" zhangdaijie@users.sf.net<mailto:zhangdaijie@users.sf.net> wrote:

Dear，

I'm very sorry didn't make it clear.

My teacher let me to learn about the knowledge of formal verification through the verification of a simple kernel code. This is my thought .First I want to translate the C code into Z or Object-Z form, then I can prove the correctness of Z or Object-Z specification to judge the correctness of the original code. If the specification has Redundant and inconsistent error , I can say the code also has the sample error .And ,I think maybe I can prove the correctness of specification by proving the theorems automatically generate in the " Z verification".

Before, I have been learning about Z and OZ. Now has begun to enter the verification phase.If I want to finish the verification ,I must known the verification rules of the tool that my use.For example there are five proof rules(formule) in the Z/EVES, “ Reduction ，Case， Quantifiers , Normal Forms ,and Equality ".

So what I want to ask is , Whether does the CZT has its own validation rules(formule) ? And where can I study the rules and process of proof? Are there examples?

Do you think my idea about the work is correct ?

Best,
Daijie

There are a picture of the theorems that I want to prove .

Attachment: verification.jpg (110.2 kB; image/jpeg)

Why the Object-Z specification is invalid?https://sourceforge.net/p/czt/discussion/295268/thread/e8c556d5/?limit=50#b492

Sent from sourceforge.nethttp://sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-12-11

Dear，

Sorry, my English ability is not very good.

Simply speaking, I want to know how CZT to carry out the theorem proving. Whether there is a user manual for theorem proving in CZT.

For example , there is a specification of “bbook” (I have sent to you) . When I open the specification in CZT , I do the following operation, “Window” –“Show View”—“Z verification” . then in the ““verification” ,I can see the verification condition .They are “schema” and ” theorems” . “Window” –“Show View”—“Z Info” , I can see the content of those “schema” and ” theorems” . I think if I want to prove the bbook specification is right , I need to prove the theorems in the “Z verification” . What do you think?

Now, Could you understand my question? If you think my method about Formal verification is not good ,could you give me some advice ?

There is the specification of bbook.

Best,
Daijie

Attachments

• Leo Freitas
2013-12-11

Hi,

CZT does not have verification support. It has however support to link
with verification tools like Z/Eves.

You will need to learn Z/Eves through its manuals, which has nothing to do with CZT.
But be aware that learning theorem proving is quite time consuming / hard. Make sure
that's what you need to do.

Leo

On 11 Dec 2013, at 03:13, Daijie Zhang zhangdaijie@users.sf.net wrote:

Dear，

Sorry, my English ability is not very good.

Simply speaking, I want to know how CZT to carry out the theorem proving. Whether there is a user manual for theorem proving in CZT.

For example , there is a specification of “bbook” (I have sent to you) . When I open the specification in CZT , I do the following operation, “Window” –“Show View”—“Z verification” . then in the ““verification” ,I can see the verification condition .They are “schema” and ” theorems” . “Window” –“Show View”—“Z Info” , I can see the content of those “schema” and ” theorems” . I think if I want to prove the bbook specification is right , I need to prove the theorems in the “Z verification” . What do you think?

Now, Could you understand my question? If you think my method about Formal verification is not good ,could you give me some advice ?

There is the specification of bbook.

Best,
Daijie

Attachment: bbook.zed (3.3 kB; application/octet-stream)

Why the Object-Z specification is invalid?

Sent from sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/

To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/

• Daijie Zhang
2013-12-12

Dear，

Thanks very much , now I have known. Actually, it is quite time consuming / hard to learn theorem proving . But my teacher let me learn the formal verification , In addition to it, is there any other way?
before , I tried to connect to the Z/EVES, but I had encountered a problems .

I have load the Z/EVES 2.1 ,(z-eves-pc-windows-acl-2.1.exe,) . And I try to connect to Z/eves follow the method in “help—help contents—czt user guide—Getting started—Z/EVES proofs”(my computer is win-7,32 bit) and it’s name is “New_configuration”. But every time progress to 57% , it will pop up a message box of “connect to Z/EVES sever, retry ?”. When I choose “retry” , it will keep on popping up the message box . But when I choose “Run – External Tools -- New_configuration” , it pop up the message box of “Only a single Z/eves prover can be running at any time – stop the running prover before launching a new one “

I can’t solve the problems by myself, it have He has troubled me for a long time , in fact , last week , before my teacher let me looking for theorem proving method of CZT itself , I have tried to connect to Z/EVES . I tried to modify the port , but it also is wrong .

Is it because my Z/EVES version is too old ? If it is , Could you give me a new version ?(I have looking for a long time , but didn’t find it ) . If it isn’t , Could you tell me where is my fault ?

There is a picture of my configurations.