Why the Object-Z specification is invalid?

Help
2013-11-05
2014-05-21
  • Daijie Zhang
    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
    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
      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
        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
        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
        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
    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
    • Hi,

      Can you attach your specification file to test ourselves?

       
      • Daijie Zhang
        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
            Daijie Zhang
            2013-11-22

            Dear,

            Thanks for your help, I will update CZT Eclipse.

            Best,
            Daijie Zhang

             
    • Leo Freitas
      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
        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?

        Looking forward you reply .

        Best,
        Daijie Zhang

         
        Last edit: Daijie Zhang 2013-11-21
        • Leo Freitas
          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?

          Looking forward you reply .

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

                  Looking forward to your reply.

                  There are the pictures and the specification.

                  Best,
                  Daijie Zhang

                   
                  Last edit: Daijie Zhang 2013-11-22
                  Attachments
                  • Leo Freitas
                    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
                    parser projects (if you download the sources).

                    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.

                    Looking forward to your reply.

                    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
                  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
                      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
                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
    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
      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
        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
          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
            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
            Daijie Zhang
            2013-12-05

            Dear,

            Thanks very much .

            Best,
            Daijie

             
          • Daijie Zhang
            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
              Leo Freitas
              2013-12-09

              Daijie,

              Could you please tell us more about what you are doing and what are your goals?
              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
                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.

                Looking forward to your reply.

                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
                    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
                    Lomesh Meshram
                    2014-05-16

                    I downloaded the z-eves-pc-windows-acl-2.1.exe file in windows 7
                    But SETUP.exe file not executing. Also SETUP.exe file is too old year 1997.
                    What is the problem?

                     
                • Lomesh Meshram
                  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
    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
      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
    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
      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
        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.

        Looking forward to your reply.

        Best,
        Daijie

         
        Attachments