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

[CZT-Users] CZT 0.5

[Petra M. <pet...@ya...>]

Hi CZT-er,

CZT version 0.5 has been released.
As usual, source releases can be downloaded from sourceforge
http://sourceforge.net/project/showfiles.php?group_id=86250
binary releases from my web-site
http://www.cs.waikato.ac.nz/~petra/

The zip version of the source release is still missing.  The file was
somehow broken and it is not possible to delete it from the sourceforge
incoming release directory so I can't upload a new one.  But it gets
deleted within 24 hours so I will try to add this file tomorrow.  Sorry
for the inconvenience.

Petra

[CZT-Users] Re: Help with getting started

[Petra M. <pe...@cs...>]

Hi Stephen,

Stephen wrote:
> Thanks. The sty files worked for building the ps files via latex. What I
> don't see from the manual is what do I do when I only have a latex file.
> That is I want to test the object-z specification I have in my latex
> file and I am new to czt. I tried to run oztypecheck against pirate.tex

This is the right way to go.

> and got an NullPointerException:

And this is obviously a bug in the CZT typechecker.
I tested pirate.tex with the current CVS version of the typechecker and
it seems to work so I guess the bug has already been fixed.

> How do I download the cvs version? When I tried to
> download czt via cvs I could not locate the correct module to use.

The correct module is just ".", the root directory.


I am currently working on the jEdit plugin and it now supports Object Z
parsing and typechecking.  If you want, I can send you the jar files for
that and you could test it for me.  :-)

Alternatively, if you still have problems with building CZT from the CVS
sources, I can also send you the jar files for the current version.

Petra

[CZT-Users] Re: Help with getting started

[Stephen T. <to...@au...>]

Thanks. The sty files worked for building the ps files via latex. What I
don't see from the manual is what do I do when I only have a latex file.
That is I want to test the object-z specification I have in my latex
file and I am new to czt. I tried to run oztypecheck against pirate.tex
and got an NullPointerException:

storri@base ~/src/czt_0_4_src/zml/examples/oz $ ~/src/czt_0_4_bin/bin/oztypecheck pirate.tex
Exception in thread "main" java.lang.NullPointerException
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.checkCompatibility(UnificationEnv.java:315)
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.weakUnifyVarClassType(UnificationEnv.java:177)
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.unifyVarClassType(UnificationEnv.java:134)
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.unify(UnificationEnv.java:90)
        at net.sourceforge.czt.typecheck.z.util.UnificationEnv.unifyProdType(UnificationEnv.java:257)
        at net.sourceforge.czt.typecheck.z.util.UnificationEnv.unify(UnificationEnv.java:178)
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.unify(UnificationEnv.java:99)
        at net.sourceforge.czt.typecheck.z.util.UnificationEnv.unifyVariableType(UnificationEnv.java:224)
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.unifyVariableType(UnificationEnv.java:120)
        at net.sourceforge.czt.typecheck.z.util.UnificationEnv.unify(UnificationEnv.java:166)
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.unify(UnificationEnv.java:99)
        at net.sourceforge.czt.typecheck.z.util.UnificationEnv.unifyPowerType(UnificationEnv.java:243)
        at net.sourceforge.czt.typecheck.z.util.UnificationEnv.unify(UnificationEnv.java:175)
        at net.sourceforge.czt.typecheck.oz.util.UnificationEnv.unify(UnificationEnv.java:99)
        at net.sourceforge.czt.typecheck.z.Checker.unify(Checker.java:263)
        at net.sourceforge.czt.typecheck.z.ExprChecker.visitApplExpr(ExprChecker.java:1005)
        at net.sourceforge.czt.typecheck.z.ExprChecker.visitApplExpr(ExprChecker.java:43)
        at net.sourceforge.czt.z.impl.ApplExprImpl.accept(ApplExprImpl.java:107)
        at net.sourceforge.czt.typecheck.oz.ExprChecker.visitTerm(ExprChecker.java:66)
        at net.sourceforge.czt.typecheck.oz.ExprChecker.visitTerm(ExprChecker.java:44)
        at net.sourceforge.czt.base.impl.TermImpl.accept(TermImpl.java:37)
        at net.sourceforge.czt.base.impl.TermAImpl.accept(TermAImpl.java:66)
        at net.sourceforge.czt.z.impl.ExprImpl.accept(ExprImpl.java:86)
        at net.sourceforge.czt.z.impl.Expr2Impl.accept(Expr2Impl.java:112)
        at net.sourceforge.czt.z.impl.ApplExprImpl.accept(ApplExprImpl.java:109)
        at net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:144)
        at net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:42)
        at net.sourceforge.czt.z.impl.MemPredImpl.accept(MemPredImpl.java:133)
        at net.sourceforge.czt.typecheck.oz.PredChecker.visitMemPred(PredChecker.java:79)
        at net.sourceforge.czt.typecheck.oz.PredChecker.visitMemPred(PredChecker.java:45)
        at net.sourceforge.czt.z.impl.MemPredImpl.accept(MemPredImpl.java:133)
        at net.sourceforge.czt.typecheck.z.PredChecker.visitAndPred(PredChecker.java:126)
        at net.sourceforge.czt.typecheck.z.PredChecker.visitAndPred(PredChecker.java:42)
        at net.sourceforge.czt.z.impl.AndPredImpl.accept(AndPredImpl.java:107)
        at net.sourceforge.czt.typecheck.oz.PredChecker.visitAndPred(PredChecker.java:127)
        at net.sourceforge.czt.typecheck.oz.PredChecker.visitAndPred(PredChecker.java:45)
        at net.sourceforge.czt.z.impl.AndPredImpl.accept(AndPredImpl.java:107)
        at net.sourceforge.czt.typecheck.z.PredChecker.visitAndPred(PredChecker.java:126)
        at net.sourceforge.czt.typecheck.z.PredChecker.visitAndPred(PredChecker.java:42)
        at net.sourceforge.czt.z.impl.AndPredImpl.accept(AndPredImpl.java:107)
        at net.sourceforge.czt.typecheck.oz.PredChecker.visitAndPred(PredChecker.java:127)
        at net.sourceforge.czt.typecheck.oz.PredChecker.visitAndPred(PredChecker.java:45)
        at net.sourceforge.czt.z.impl.AndPredImpl.accept(AndPredImpl.java:107)
        at net.sourceforge.czt.typecheck.oz.ParaChecker.visitInitialState(ParaChecker.java:285)
        at net.sourceforge.czt.typecheck.oz.ParaChecker.visitInitialState(ParaChecker.java:40)
        at net.sourceforge.czt.oz.impl.InitialStateImpl.accept(InitialStateImpl.java:122)
        at net.sourceforge.czt.typecheck.oz.ParaChecker.visitClassPara(ParaChecker.java:158)
        at net.sourceforge.czt.typecheck.oz.ParaChecker.visitClassPara(ParaChecker.java:40)
        at net.sourceforge.czt.oz.impl.ClassParaImpl.accept(ClassParaImpl.java:200)
        at net.sourceforge.czt.typecheck.z.SpecChecker.visitZSect(SpecChecker.java:117)
        at net.sourceforge.czt.z.impl.ZSectImpl.accept(ZSectImpl.java:133)
        at net.sourceforge.czt.typecheck.oz.SpecChecker.visitTerm(SpecChecker.java:61)
        at net.sourceforge.czt.base.impl.TermImpl.accept(TermImpl.java:37)
        at net.sourceforge.czt.base.impl.TermAImpl.accept(TermAImpl.java:66)
        at net.sourceforge.czt.z.impl.SectImpl.accept(SectImpl.java:86)
        at net.sourceforge.czt.z.impl.ZSectImpl.accept(ZSectImpl.java:135)
        at net.sourceforge.czt.typecheck.z.SpecChecker.visitSpec(SpecChecker.java:55)
        at net.sourceforge.czt.z.impl.SpecImpl.accept(SpecImpl.java:159)
        at net.sourceforge.czt.typecheck.oz.SpecChecker.visitTerm(SpecChecker.java:61)
        at net.sourceforge.czt.base.impl.TermImpl.accept(TermImpl.java:37)
        at net.sourceforge.czt.base.impl.TermAImpl.accept(TermAImpl.java:66)
        at net.sourceforge.czt.z.impl.SpecImpl.accept(SpecImpl.java:161)
        at net.sourceforge.czt.typecheck.z.TypeChecker.visitTerm(TypeChecker.java:171)
        at net.sourceforge.czt.typecheck.oz.TypeCheckUtils.lTypecheck(TypeCheckUtils.java:121)
        at net.sourceforge.czt.typecheck.oz.TypeCheckUtils.lTypecheck(TypeCheckUtils.java:104)
        at net.sourceforge.czt.typecheck.z.TypeCheckUtils.run(TypeCheckUtils.java:252)
        at net.sourceforge.czt.typecheck.oz.TypeCheckUtils.main(TypeCheckUtils.java:175)

What is wrong here? How do I download the cvs version? When I tried to
download czt via cvs I could not locate the correct module to use.

Stephen

On Thu, 2006-02-09 at 20:08 +1300, Petra Malik wrote:
> Hi Stephen,
> 
> Stephen wrote:
> > I copied ltcadiz.sty and oz.sty to the ~/src/czt_0_4_src/zml/examples/oz
> > directory. When I attempted to build the file via latex I got errors.
> > See attached pirate.log for the reason: ! LaTeX Error: \begin{state} on
> > input line 11 ended by \end{genschema}.
> 
> That seems to be a problem with the ltcadiz style; unfortunately we
> don't have a czt style yet - feel free to write one.  :-)
> 
> I modified the ltcadiz style (it now needs ap.sty as well, which is
> attached) so that pirate is now working for me.  Lots more work is
> probably needed to get the other examples working and to get a nice czt
> style but I don't have the time to do that.
> 
> Hope it helps to get at least one example through latex.  Note that you
> can still use the czt typechecker to typecheck your specification - even
> when you get latex errors.
> 
> Petra
-- 
PhD. Candidate
Auburn University
Department of Computer Science and Software Engineering
107 Dunstan Hall
Auburn, AL 36849-5347  U.S.A.
(334) 844-4330 (O)
to...@au...

Re: [CZT-Users] Re: Help with getting started

[Stephen T. <to...@au...>]

On Mon, 2006-01-30 at 12:29 +1300, Petra Malik wrote:
> Hi Stephen,
> 
> nice to see that we've got a user that dares to ask questions on this
> mailing list.  :-)

My mission to quote Star Trek is "To boldy go where no one has gone
before".

Thanks for the the help.

Stephen
-- 
PhD. Candidate
Auburn University
Department of Computer Science and Software Engineering
107 Dunstan Hall
Auburn, AL 36849-5347  U.S.A.
(334) 844-4330 (O)
to...@au...

[CZT-Users] Re: Help with getting started

[Petra M. <pe...@cs...>]

Hi Stephen,

nice to see that we've got a user that dares to ask questions on this
mailing list.  :-)

Stephen Torri wrote:
> [...] Well I got a few errors that I don't understand:
> 
> storri@base ~/src/czt_0_4_bin/bin $ ./zedtypecheck ~/Documents/StephenTorri/comp7730/project/project.tex
> Jan 27, 2006 12:33:42 AM class net.sourceforge.czt.parser.z.Latex2Unicode
> SEVERE: Unknown latex command \tfun

In short, you are using a latex command that is not defined in the Z
Standard.

Here is a bit more explanation:  There are several Z dialects and
different Z latex commands for those dialects; CZT is an implementation
of the Z Standard and currently only supports the latex commands defined
there.  You can download the Standard for free from the ISO/IEC web-page.

I guess "\tfun" is a total function and is written "\fun" in Standard Z.

> SEVERE: Unknown latex command \times

Use "\cross" instead.

> SEVERE: Unknown latex command \rightarrow

Do you mean "\implies"?

> "/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 20 column 1: Syntax error at symbol RELATION

You probably want to use "\relation".

> "/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 30 column 1: Syntax error at symbol PARENTS

You probably want to use "\parents".

> "/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 97 column 13: Expression expected; found predicate

I have no idea; I would need to have a look at the source latex file to
understand.

Hope that helps,
Petra

[CZT-Users] Help with getting started

[Stephen T. <to...@au...>]

After slogging through trying to build my own version of czt I
downloaded the binary from Petra's web page. Now I am familiar with Z
after having taken a class on formal methods but by no means an expert.
As a part of the class we had to put together a Z specification. So I
thought I would try to use the zedtypecheck to see how I did. Well I got
a few errors that I don't understand:

storri@base ~/src/czt_0_4_bin/bin $ ./zedtypecheck ~/Documents/StephenTorri/comp7730/project/project.tex
Jan 27, 2006 12:33:42 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \tfun
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \tfun
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \times
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \times
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \tfun
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \rightarrow
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \rightarrow
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \rightarrow
Jan 27, 2006 12:33:43 AM class net.sourceforge.czt.parser.z.Latex2Unicode
SEVERE: Unknown latex command \rightarrow
"/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 20 column 1: Syntax error at symbol RELATION
"/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 30 column 1: Syntax error at symbol PARENTS
"/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 97 column 13: Expression expected; found predicate
"/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 98 column 13: Expression expected; found predicate
"/home/storri/Documents/StephenTorri/comp7730/project/project.tex" line 99 column 9: Expression expected; found predicate

Would the latex files be helpful? I don't get an error running latex to
build my paper so I don't think I have bad files.

Stephen
-- 
PhD. Candidate
Auburn University
Department of Computer Science and Software Engineering
107 Dunstan Hall
Auburn, AL 36849-5347  U.S.A.
(334) 844-4330 (O)
to...@au...

[CZT-Users] Re: [CZT-Devel] Binary Releases

[Tim M. <T.M...@cs...>]

Hi all,

Just following up to Petra's message: there have been many changes 
and bugfixes made to the parser/typechecker since the November 10 
version, so if you find problems, it would probably be best to 
wait until the next binary version is released (or check out the 
CVS version and compile it if you are brave), and if that problem 
is still occurring, submit a bug report to us :-)

Thanks,
Tim

Petra Malik wrote:
> Hi all,
> 
> I just noticed that I forgot to announce that here:
> On my web-site
> http://www.cs.waikato.ac.nz/~petra/
> are CZT binary releases available.
> The first one is from November, 10, and we are planning
> to provide a new one very soon (hopefully next week).
> 
> We cannot distribute full binary releases on sourceforge
> since JAXB does not have an open source license and only
> open source software is allowed to be distributed via
> sourceforge (if I understand correctly).
> 
> Petra
> 
> 
> -------------------------------------------------------
> SF email is sponsored by - The IT Product Guide
> Read honest & candid reviews on hundreds of IT Products from real users.
> Discover which products truly live up to the hype. Start reading now. 
> http://productguide.itmanagersjournal.com/
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

[CZT-Users] Binary Releases

[Petra M. <pe...@cs...>]

Hi all,

I just noticed that I forgot to announce that here:
On my web-site
http://www.cs.waikato.ac.nz/~petra/
are CZT binary releases available.
The first one is from November, 10, and we are planning
to provide a new one very soon (hopefully next week).

We cannot distribute full binary releases on sourceforge
since JAXB does not have an open source license and only
open source software is allowed to be distributed via
sourceforge (if I understand correctly).

Petra

[CZT-Users] Corejava release 1.1.1

[Petra M. <pe...@cs...>]

Hi,

corejava 1.1.1 has been released. It contains Java source code for
Z annotated syntax trees, reading and writing XML files etc.

This release fixes a few bugs:

  * API Change:
    change all immutable properties to be mutable since immutable properties
    are no longer needed (they were there for historic reasons)
    => all getter methods that return an immutable list in corejava_1_1_0
       now return a (mutable) list (an example is getDeclName() in AxPara)
    => there are a few more setters now (an example is setName(String)
       in ZSect)
    => there are a few more default factory methods in CoreFactory and
       CoreFactoryImpl (an example is createAxPara())
    => some of the constructors of the implementation classes in package
       have changed; now none of the constructors accepts arguments
       (this should not have influence on applications since these
       constructors are not supposed to be used by applications :-)
    => remove class ImmutableList since it is no longer used

  * add namespace information to the DOM output and write each node
    on its own line (indentation is still missing)

  * use the CLASSPATH environment variable when running the examples
    and tests to avoid NoClassDefFoundError when CLASSPATH is set properly
    but jwsdp.home is not set


Hava fun,
Petra