czt-devel — For programmers using the CZT code

Re: [CZT-Devel] Fixes to build standalone CZT for JDK11 and Maven 3.8.1

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

Thanks to Anthony Hall who followed my steps to build CZT on a Windows 7 /
JDK 11 platform (versus my Windows 10 / JDK SE 11.0.1) which exposed two
problems:
- an addition is needed to the toplevel code/pom.xml to specify a later
(default) version of plexus-archiver.
- my changes to gnast work when the path name contains spaces, like
"C:/home/some
stuff/CZT/", but break when there is no space, like "C:/home/some_stuff/CZT/".
A further change to the file
code\dev\gnast\src\main\java\net\sourceforge\czt\gnast\project.java fixes
this.

Fixes for both of these problems are included in this zip file at
https://drive.google.com/file/d/19x2cnIHbajH1vEAk2JZztlEqVW03dNd9/view?usp=sharing
which replaces that in step 2 of my 11 July post.
This zip file includes all the changes and bug fixes to CZT since my 11
July post to date.

With thanks,
julian



On Sun, 11 Jul 2021 at 10:00, Julian Rose <jro...@gm...> wrote:

>
> The instructions at http://czt.sourceforge.net/dev/setup.html describe
> how to download and build the CZT standalone. But the CZT sources retrieved
> by 'git clone git://git.code.sf.net/p/czt/code' do not successfully build
> with JDK11. The fixes given here enable you to build the standalone CZT
> using JDK11 and the latest Maven 3.8.1.
>
> HowTo:
> 1/ If you don't have the sources, follow the above instructions to 'git
> clone git://git.code.sf.net/p/czt/code'.
> 2/ Replace the files by those in the zip file at '
> https://drive.google.com/file/d/1NMFsEIM03Q4JvDweuWHotzEVURFLo-T-/view?usp=sharing
> '.
> 3/ Follow the above instructions to build in the top level ./code
> directory.
>    For example
>       'cd ./code/'
>       'mvn -X -l logfile clean install'.  (That's minus-ell to name the
> logfile output.)
>    The build does take some time, around 20-30 minutes on my modest laptop.
>    3.1/ The resulting czt.jar will be located in ./code/lib/
>    3.2/ If the build fails then you can view 'logfile' in ./code/ using a
> text editor. Go to the end and scroll upwards to find the [ERROR] reason.
> If some goal failed to execute but there doesn't seem to be a compilation
> error then you may have suffered an Internet brownout (Maven downloads
> files into ~/.m2/repository during the build) and you can just retry the
> build once more.
>
> Size:
> The downloadable czt.jar at czt.sourceforge.net is 6148KB in size (as per
> my Windows file system). Whereas the JDK11-buildable file size is 7400KB.
> The differences are attributable to inclusion of JAXB libraries in the new
> jar (javax/ and com/sun/ packages).
>
> Summary of changes:
> The changes are the minimum required to various Maven configuration files
> (pom.xml) and to Gnast sources. There are no changes to Java code
> (excepting Gnast). All the changes are commented with 'jhr' to make them
> obvious.
>
> The changes to pom files are a/ to do with goal-setting, and b/ bringing
> in JAXB as a dependancy. (JAXB was bundled with JDK8 but has since been
> un-bundled. The CZT source code could be updated to use the newer 'jakarta'
> api.)
>
> The change to Gnast works well but is a workaround. Some behaviour in
> Velocity (which gnast basically wraps up), or perhaps in some maven plugin
> used by Velocity, has changed such that resource files in the
> templateDirectory are not processed as they must previously have been. (A
> fix to Velocity / plug-in might be investigated as an alternative solution.)
>
> The following 'git status' output shows which files are modified:
>
>   On branch master
>   Your branch is up to date with 'origin/master'.
>
>   Changes not staged for commit:
>     (use "git add <file>..." to update what will be committed)
>     (use "git restore <file>..." to discard changes in working directory)
> modified:   corejava/corejava-circus/pom.xml
> modified:   corejava/corejava-circusconf/pom.xml
> modified:   corejava/corejava-circuspatt/pom.xml
> modified:   corejava/corejava-circustime/pom.xml
> modified:   corejava/corejava-oz/pom.xml
> modified:   corejava/corejava-z/pom.xml
> modified:   corejava/corejava-zeves/pom.xml
> modified:   corejava/corejava-zpatt/pom.xml
> modified:   corejava/pom.xml
> modified:   dev/gnast/src/main/java/net/sourceforge/czt/gnast/Apgen.java
> modified:   dev/gnast/src/main/java/net/sourceforge/czt/gnast/Gnast.java
> modified:   dev/gnast/src/main/java/net/sourceforge/czt/gnast/Project.java
> modified:   parser/parser-circus/pom.xml
> modified:   parser/parser-circusconf/pom.xml
> modified:   parser/parser-circustime/pom.xml
> modified:   parser/parser-oz/pom.xml
> modified:   parser/parser-ozpatt/pom.xml
> modified:   parser/parser-z/pom.xml
> modified:   parser/parser-zeves/pom.xml
> modified:   parser/parser-zpatt/pom.xml
> modified:   parser/pom.xml
> modified:   pom.xml
>
> The changes have been used to build on a Windows 10 laptop on which cygwin
> is installed, so maybe some path separator errors are present in my
> changes. Further tests would be useful:
> 1. Build on a Windows laptop that does not have cygwin installed
> 2. Build on a *nix (Linux) host
> 3. Try building with the latest JDK16
>
> julian rose
>
>

Re: [CZT-Devel] livelock error in typechecker-z dependency graph function and an initial solution

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

I was able to find a better solution than my initial one, in the revised
source files attached:
src\code\typechecker\typechecker-z\src\main\java\net\sourceforge\czt\typecheck\z\Checker.java
src\code\typechecker\typechecker-z\src\main\java\net\sourceforge\czt\typecheck\z\util\DependencyGraph.java.

This better solution detects when a cyclic dependency is added and resolves
it, which results in a pass. Whereas the initial solution detects a cyclic
dependency after the event and throws an exception, resulting in output
errors.

Please see outputs from both czt.jar and (ZWordTools) cztinterface.jar with
the better solution applied.

(Since I only have a very small number of test cases, the initial solution
is left intact to catch livelock resulting from other inputs. So you will
still need the modified TypeChecker.java, ErrorMessage.java and
ErrorMessage_en.properties files attached to my previous post. But, the
UNEXPECTED_CYCLIC_DEPENDENCY_IN_LIST exception can be deleted if this
better solution proves acceptable.)

With thanks,
julian

[CZT-Devel] livelock error in typechecker-z dependency graph function and an initial solution

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

There is a bug (or even a design fault) in the CZT typechecker-z software
which can result in livelock in the dependency graph function, so that the
user experiences a frozen tool.

Please see a description of the problem (including an offending
specification) and an initial solution in the attached 'CZT-bug
livelock.docx'.
*@Mark*: Can you please read section 1 of the description and comment (or
email me) if you have any critique on my analysis of sections.

Please see the modified source files attached as per the description
document. (All these source files belong under
...\CZT\src\code\typechecker\typechecker-z\... and not one of the other
sub-typecheckers, which do not have a reorder function.)
Please see outputs from both czt.jar and (ZWordTools) cztinterface.jar with
the initial solution applied.
Lastly the 'CZT-bug livelog.zed8' generated from the description is
attached for those without ZWordTools.

(It is possible the bug report I made on 01 August "IndexOutOfBoundsException
in typechecker-z and a solution" is also symptomatic of the same design
fault - if indeed there is one - I might be able to find a better solution
than these two.)

With thanks,
julian

(*@Admin*: sorry I know this post is larger than the usual 100K limit.)

[CZT-Devel] IndexOutOfBoundsException in typechecker-z and a solution

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

There is a bug in the CZT typechecker-z software which can result in an
IndexOutOfBoundsException when using the "-d" cmdline option (use before
definition). The error output requests an email be sent to czt-devel.

corejava-z\target\generated-sources\gnast\net\sourceforge\czt\z\impl\ZParaListImpl.java:246
throws-up an ArrayIndexOutOfBoundsException, the cause of which is
code\typechecker\typechecker-z\src\main\java\net\sourceforge\czt\typecheck\z\Checker.java:881
in the function reorderParaList (dependancy graph paragraph reordering).

Please find attached a solution in Checker.java:reorderParaList, summarised
in the attached file diff-checker-java, which guards against the index out
of bounds from happening. (The four other CZT implementations of
Checker.java (circus, circusconf, zeves, oz) do not include a
reorderParaList function.)

Please see proof of fix attached, which shows test output from the before
and after change to both ZWT (ZWordTools) and CZT jar files with and
without "-d" cmdline option. The minimal zed8 input test file is also
attached. My builds are made using JDK11 and Maven 3.8.1.

With thanks,
julian

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

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

 Hei Anthony,

I have now built ZWordTools cztinterface.jar using Maven 3.8.1 and JDK11,
and successfully tested it.

I built ...\zwordtools-code\cztinterface with 'mvn -X -l logfile
-Dmaven.test.skip=true clean install', as the tests fail to build for me.
(For example, some of your "expect" (zee) files have paths hard-coded like
/Users/Anthony/... and this is not going to work for me. The cztinterface
tests might be generalised.) I made small changes
to...\zwordtools-code\cztinterface\pom.xml and
...\zwordtools-code\cztinterface\src\main\java\net\sourceforge\zwordtools\cztinterface\CZTCheck.java,
commented with jhr, as attached.

The resulting ...\zwordtools-code\Code\cztinterface.jar size is 2,800KB,
compared to your download jar file size of 1,453KB. This larger size is
attributable to the inclusion of com/sun and javax packages in the new jar.
(These packages are inherited through dependencies and inclusion of
typechecker-z by Maven from
...\.m2\repository\net\sourceforge\czt\typechecker-z resulting from my
JDK11 czt build).

Finally, I replaced cztinterface.jar in
C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\ and
successfully used ZWT on my test input. (I did another test, replacing
PredChecker.class in your download cztinterface.jar which also tested
successfully.)

With thanks,
julian

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

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

Hello again,

Please find a fix for this problem attached in the file PredChecker.java.
More precisely this is the PredChecker.java found in
.\code\typechecker\typechecker-z\src\main\java\net\sourceforge\czt\typecheck\z\.
My solution is a try..catch block around the cast.

I have tested this fix by building a new czt.jar and executing that with my
original test input.
Please see attached 'proof of fix.txt' which shows executions using both
the release czt.jar (results in crash) and separately my own build (results
in useful output).
I have also re-attached my original test input - the content has errors
which the tool should report.

@Anthony: While I have downloaded the source files, I'm not sure how to
build zwordtools.
But you would need to include the new PredChecker.class file in
cztinterface.jar
I think you said you can't build czt currently (maybe my post to czt-devel
last week helps with that), so I can send you the PredChecker.class file if
you want to test it and can complete a build of zwt from there.

There is a different unguarded cast in the typechecker-oz\PredChecker.java,
and that should be tested.
I think the typechecker-circus and typechecker-zeves versions of
PredChecker.java do not have this problem.

With thanks,
julian

[CZT-Devel] Fixes to build standalone CZT for JDK11 and Maven 3.8.1

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

The instructions at http://czt.sourceforge.net/dev/setup.html describe how
to download and build the CZT standalone. But the CZT sources retrieved by
'git clone git://git.code.sf.net/p/czt/code' do not successfully build with
JDK11. The fixes given here enable you to build the standalone CZT using
JDK11 and the latest Maven 3.8.1.

HowTo:
1/ If you don't have the sources, follow the above instructions to 'git
clone git://git.code.sf.net/p/czt/code'.
2/ Replace the files by those in the zip file at '
https://drive.google.com/file/d/1NMFsEIM03Q4JvDweuWHotzEVURFLo-T-/view?usp=sharing
'.
3/ Follow the above instructions to build in the top level ./code directory.
   For example
      'cd ./code/'
      'mvn -X -l logfile clean install'.  (That's minus-ell to name the
logfile output.)
   The build does take some time, around 20-30 minutes on my modest laptop.
   3.1/ The resulting czt.jar will be located in ./code/lib/
   3.2/ If the build fails then you can view 'logfile' in ./code/ using a
text editor. Go to the end and scroll upwards to find the [ERROR] reason.
If some goal failed to execute but there doesn't seem to be a compilation
error then you may have suffered an Internet brownout (Maven downloads
files into ~/.m2/repository during the build) and you can just retry the
build once more.

Size:
The downloadable czt.jar at czt.sourceforge.net is 6148KB in size (as per
my Windows file system). Whereas the JDK11-buildable file size is 7400KB.
The differences are attributable to inclusion of JAXB libraries in the new
jar (javax/ and com/sun/ packages).

Summary of changes:
The changes are the minimum required to various Maven configuration files
(pom.xml) and to Gnast sources. There are no changes to Java code
(excepting Gnast). All the changes are commented with 'jhr' to make them
obvious.

The changes to pom files are a/ to do with goal-setting, and b/ bringing in
JAXB as a dependancy. (JAXB was bundled with JDK8 but has since been
un-bundled. The CZT source code could be updated to use the newer 'jakarta'
api.)

The change to Gnast works well but is a workaround. Some behaviour in
Velocity (which gnast basically wraps up), or perhaps in some maven plugin
used by Velocity, has changed such that resource files in the
templateDirectory are not processed as they must previously have been. (A
fix to Velocity / plug-in might be investigated as an alternative solution.)

The following 'git status' output shows which files are modified:

  On branch master
  Your branch is up to date with 'origin/master'.

  Changes not staged for commit:
    (use "git add <file>..." to update what will be committed)
    (use "git restore <file>..." to discard changes in working directory)
modified:   corejava/corejava-circus/pom.xml
modified:   corejava/corejava-circusconf/pom.xml
modified:   corejava/corejava-circuspatt/pom.xml
modified:   corejava/corejava-circustime/pom.xml
modified:   corejava/corejava-oz/pom.xml
modified:   corejava/corejava-z/pom.xml
modified:   corejava/corejava-zeves/pom.xml
modified:   corejava/corejava-zpatt/pom.xml
modified:   corejava/pom.xml
modified:   dev/gnast/src/main/java/net/sourceforge/czt/gnast/Apgen.java
modified:   dev/gnast/src/main/java/net/sourceforge/czt/gnast/Gnast.java
modified:   dev/gnast/src/main/java/net/sourceforge/czt/gnast/Project.java
modified:   parser/parser-circus/pom.xml
modified:   parser/parser-circusconf/pom.xml
modified:   parser/parser-circustime/pom.xml
modified:   parser/parser-oz/pom.xml
modified:   parser/parser-ozpatt/pom.xml
modified:   parser/parser-z/pom.xml
modified:   parser/parser-zeves/pom.xml
modified:   parser/parser-zpatt/pom.xml
modified:   parser/pom.xml
modified:   pom.xml

The changes have been used to build on a Windows 10 laptop on which cygwin
is installed, so maybe some path separator errors are present in my
changes. Further tests would be useful:
1. Build on a Windows laptop that does not have cygwin installed
2. Build on a *nix (Linux) host
3. Try building with the latest JDK16

julian rose

Re: [CZT-Devel] ZWordTools fails to proceed with this input

[<an...@an...>]

Dear Julian

 

I’m sorry, but this is again a fault in CZT, not in the Word tools themselves. I’m copying this to the czt developers, and if they fix it and let me know I will try and update the Z Word tools to incorporate the fix.

 

Are you using features of standard Z that are not in Spivey Z? If not, you might find it quicker and more reliable to use fuzz as the typechecker. As you said previously, it does not look as if CZT is being maintained.

 

Regards

 

Anthony

 

From: Julian Rose [mailto:jro...@gm...] 
Sent: 02 August 2020 14:50
To: Anthony Hall
Cc: Julian Rose
Subject: ZWordTools fails to proceed with this input

 

Hei Anthony,

 

ZWordTools typecheck (czt) livelocks on the attached input file.

The file contains a text summary of the problem, which cause is just a typo.

No fault is reported so I haven't raised a bug report.

The .zte and .ztr files are empty. The .zed8 is populated correctly (with typo).

 

With thanks,

julian

 

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

[<an...@an...>]

Thanks Mark

 

Can you please let me know when this is fixed, and what’s been changed, so I can try to update the ZWT snapshot?

 

All the best

 

Anthony

 

From: Mark Utting [mailto:bm....@gm...] 
Sent: 02 June 2020 05:50
To: Julian Rose
Cc: Anthony Hall; czt-devel
Subject: Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

 

Julian

 

Done:  https://sourceforge.net/p/czt/bugs/130/ 

 

Thanks for reporting this.

Mark 

 

On Tue, 2 Jun 2020 at 14:23, Julian Rose <jro...@gm...> wrote:

Hei Prof. Mark Utting,

 

Thanks for your reply. 

As you say the tool should handle invalid input gracefully. 

I am not a member Sourceforge CZT so do not have permission to create a ticket. Could you add it please?

 

 

(The content of the Z doesn't matter - although see my reply to Anthony Hall - and was reduced simply to reproduce the error.

The Boolean type I use in the reply to Anthony is defined as a set of schemas:

False == [ | false ]

True == [ | true ]

Boolean == { False, True }

which I borrowed from Ian Toyn.)

 

(The cut-and-paste works because the characters are Unicode. 

You might like this web site for displayable characters <https://www.codetable.net/groups>  which you can use in Word and in HTML and others.)

 

With thanks,

julian

 

 

 

 

 

On Tue, 2 Jun 2020 at 08:51, Mark Utting <bm....@gm...> wrote:

Anthony and Julian

 

The error message is clearer with Java 8 (than with later Java versions which use modules):

 

java.lang.ClassCastException: net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to net.sourceforge.czt.z.ast.ProdType
        at net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:173)
        at net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:39)

 

I think this is actually caused by a type error in the input specification.

 

r  _ : seq X

 

∀ s : seq X  ⦁

          r s ⇔ ( ∃ i : 1..#s ⦁ ¬s⟨i⟩ )

(That's pretty neat, that a copy-paste from the Word doc translates to HTML in this email!)

 

Firstly, Z does not have a boolean type, so it is not clear what the predicate inside the exists means.

Secondly, the type of 'r' probably needs to be '\power (\seq X)'.

(See 'disjoint' in the ISO standard Z library for an example of a prefix relation).

 

That said, the CZT typechecker should give a nice type checking error message, not throw a cast exception!

So Julian, please feel free to report this as a typechecker bug on the Sourceforge repository.

 

Cheers

Mark

 

 

 

On Mon, 1 Jun 2020 at 19:45, <an...@an...> wrote:

Dear Mark

 

The Z Word Tools certainly work OK with Word 2007, so that isn’t the problem.  I’m trying to look into this myself but my Java configuration seems to be broken at the moment. The generated file temp.zedB looks to me as if it’s  a correct translation of the Word Document. Can you please tell me whether it goes through CZT correctly? If so, then the problem must be with the subset snapshot of CZT that ZWT uses and I will have to fix that – which I fear may take me some time! If not, does it give the error that Julian is seeing, or something different?

 

All the best

 

Anthony

(Z Word Tools developer)

 

From: Mark Utting [mailto:bm....@gm...] 
Sent: 01 June 2020 01:21
To: czt-devel
Subject: Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

 

Julian

 

I'm not very familiar with ZWTools architecture, but this looks like some kind of version or configuration problem.

 

I suggest you try with a more recent version of Word, that is more likely to have been tested with ZWTools.

Such as Word 2013.

 

Cheers

Mark

 

 

On Mon, 1 Jun 2020 at 10:12, <czt...@li...> wrote:

Send CZT-Devel mailing list submissions to
        czt...@li...

To subscribe or unsubscribe via the World Wide Web, visit
        https://lists.sourceforge.net/lists/listinfo/czt-devel
or, via email, send a message with subject or body 'help' to
        czt...@li...

You can reach the person managing the list at
        czt...@li...

When replying, please edit your Subject line so it is more specific
than "Re: Contents of CZT-Devel digest..."


Today's Topics:

   1. bug report: net.sourceforge.czt.typecheck.z.PredChecker
      (Julian Rose)


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

Message: 1
Date: Fri, 29 May 2020 10:20:58 +0800
From: Julian Rose <jro...@gm...>
To: czt...@li...
Cc: Julian Rose <jro...@gm...>
Subject: [CZT-Devel] bug report:
        net.sourceforge.czt.typecheck.z.PredChecker
Message-ID:
        <CAH...@ma... <mailto:CAHUeuCEFFeGF5L-z%2B98Zbg%2BS...@ma...> >
Content-Type: text/plain; charset="utf-8"

Hei,

Summary.....: A general Throwable exception has happened - class
net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
net.sourceforge.czt.z.ast.ProdType
(net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
Exception...: java.lang.ClassCastException
Cause.......: none

I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
configured for CZT type-checking with option ?Allow use before
declaration?.

The ZWordTools-generated temp.bat file contains (java -jar
"C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
-d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
Please see attached files.
Including a minimal temp.docx to reproduce the error.
The temp.ztr file is empty.

With thanks,
julian
-------------- next part --------------
An HTML attachment was scrubbed...
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.zed8
Type: application/octet-stream
Size: 129 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.zte
Type: application/octet-stream
Size: 3827 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.docx
Type: application/vnd.openxmlformats-officedocument.wordprocessingml.document
Size: 45196 bytes
Desc: not available

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



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

Subject: Digest Footer

_______________________________________________
CZT-Devel mailing list
CZT...@li...
https://lists.sourceforge.net/lists/listinfo/czt-devel


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

End of CZT-Devel Digest, Vol 64, Issue 1
****************************************

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

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

Julian

Done:  https://sourceforge.net/p/czt/bugs/130/

Thanks for reporting this.
Mark

On Tue, 2 Jun 2020 at 14:23, Julian Rose <jro...@gm...> wrote:

> Hei Prof. Mark Utting,
>
> Thanks for your reply.
> As you say the tool should handle invalid input gracefully.
> I am not a member Sourceforge CZT so do not have permission to create a
> ticket. Could you add it please?
>
>
> (The content of the Z doesn't matter - although see my reply to Anthony
> Hall - and was reduced simply to reproduce the error.
> The Boolean type I use in the reply to Anthony is defined as
> * a set of schemas:*
> *False *== [ | *false *]
> *True *== [ | *true *]
> *Boolean *== { *False*, *True *}
> which I borrowed from Ian Toyn.)
>
> (The cut-and-paste works because the characters are Unicode.
> You might like this web site for displayable characters
> <https://www.codetable.net/groups> which you can use in Word and in HTML
> and others.)
>
> With thanks,
> julian
>
>
>
>
>
> On Tue, 2 Jun 2020 at 08:51, Mark Utting <bm....@gm...> wrote:
>
>> Anthony and Julian
>>
>> The error message is clearer with Java 8 (than with later Java versions
>> which use modules):
>>
>> java.lang.ClassCastException:
>> net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to
>> net.sourceforge.czt.z.ast.ProdType
>>         at
>> net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:173)
>>         at
>> net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:39)
>>
>> I think this is actually caused by a type error in the input
>> specification.
>>
>> *r*  _ : *seq X*
>>
>>
>>
>> ∀ *s *: *seq X * ⦁
>>
>>           *r* *s *⇔ ( ∃ *i *: 1..#*s *⦁ ¬*s*⟨*i*⟩ )
>> (That's pretty neat, that a copy-paste from the Word doc translates to
>> HTML in this email!)
>>
>> Firstly, Z does not have a boolean type, so it is not clear what the
>> predicate inside the exists means.
>> Secondly, the type of 'r' probably needs to be '\power (\seq X)'.
>> (See 'disjoint' in the ISO standard Z library for an example of a prefix
>> relation).
>>
>> That said, the CZT typechecker should give a nice type checking error
>> message, not throw a cast exception!
>> So Julian, please feel free to report this as a typechecker bug on the
>> Sourceforge repository.
>>
>> Cheers
>> Mark
>>
>>
>>
>> On Mon, 1 Jun 2020 at 19:45, <an...@an...> wrote:
>>
>>> Dear Mark
>>>
>>>
>>>
>>> The Z Word Tools certainly work OK with Word 2007, so that isn’t the
>>> problem.  I’m trying to look into this myself but my Java configuration
>>> seems to be broken at the moment. The generated file temp.zedB looks to me
>>> as if it’s  a correct translation of the Word Document. Can you please tell
>>> me whether it goes through CZT correctly? If so, then the problem must be
>>> with the subset snapshot of CZT that ZWT uses and I will have to fix that –
>>> which I fear may take me some time! If not, does it give the error that
>>> Julian is seeing, or something different?
>>>
>>>
>>>
>>> All the best
>>>
>>>
>>>
>>> Anthony
>>>
>>> (Z Word Tools developer)
>>>
>>>
>>>
>>> *From:* Mark Utting [mailto:bm....@gm...]
>>> *Sent:* 01 June 2020 01:21
>>> *To:* czt-devel
>>> *Subject:* Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1
>>>
>>>
>>>
>>> Julian
>>>
>>>
>>>
>>> I'm not very familiar with ZWTools architecture, but this looks like
>>> some kind of version or configuration problem.
>>>
>>>
>>>
>>> I suggest you try with a more recent version of Word, that is more
>>> likely to have been tested with ZWTools.
>>>
>>> Such as Word 2013.
>>>
>>>
>>>
>>> Cheers
>>>
>>> Mark
>>>
>>>
>>>
>>>
>>>
>>> On Mon, 1 Jun 2020 at 10:12, <czt...@li...>
>>> wrote:
>>>
>>> Send CZT-Devel mailing list submissions to
>>>         czt...@li...
>>>
>>> To subscribe or unsubscribe via the World Wide Web, visit
>>>         https://lists.sourceforge.net/lists/listinfo/czt-devel
>>> or, via email, send a message with subject or body 'help' to
>>>         czt...@li...
>>>
>>> You can reach the person managing the list at
>>>         czt...@li...
>>>
>>> When replying, please edit your Subject line so it is more specific
>>> than "Re: Contents of CZT-Devel digest..."
>>>
>>>
>>> Today's Topics:
>>>
>>>    1. bug report: net.sourceforge.czt.typecheck.z.PredChecker
>>>       (Julian Rose)
>>>
>>>
>>> ----------------------------------------------------------------------
>>>
>>> Message: 1
>>> Date: Fri, 29 May 2020 10:20:58 +0800
>>> From: Julian Rose <jro...@gm...>
>>> To: czt...@li...
>>> Cc: Julian Rose <jro...@gm...>
>>> Subject: [CZT-Devel] bug report:
>>>         net.sourceforge.czt.typecheck.z.PredChecker
>>> Message-ID:
>>>         <
>>> CAH...@ma...>
>>> Content-Type: text/plain; charset="utf-8"
>>>
>>> Hei,
>>>
>>> Summary.....: A general Throwable exception has happened - class
>>> net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to
>>> class
>>> net.sourceforge.czt.z.ast.ProdType
>>> (net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
>>> net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
>>> Exception...: java.lang.ClassCastException
>>> Cause.......: none
>>>
>>> I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
>>> configured for CZT type-checking with option ?Allow use before
>>> declaration?.
>>>
>>> The ZWordTools-generated temp.bat file contains (java -jar
>>>
>>> "C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
>>> -d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
>>> Please see attached files.
>>> Including a minimal temp.docx to reproduce the error.
>>> The temp.ztr file is empty.
>>>
>>> With thanks,
>>> julian
>>> -------------- next part --------------
>>> An HTML attachment was scrubbed...
>>> -------------- next part --------------
>>> A non-text attachment was scrubbed...
>>> Name: temp.zed8
>>> Type: application/octet-stream
>>> Size: 129 bytes
>>> Desc: not available
>>> -------------- next part --------------
>>> A non-text attachment was scrubbed...
>>> Name: temp.zte
>>> Type: application/octet-stream
>>> Size: 3827 bytes
>>> Desc: not available
>>> -------------- next part --------------
>>> A non-text attachment was scrubbed...
>>> Name: temp.docx
>>> Type:
>>> application/vnd.openxmlformats-officedocument.wordprocessingml.document
>>> Size: 45196 bytes
>>> Desc: not available
>>>
>>> ------------------------------
>>>
>>>
>>>
>>> ------------------------------
>>>
>>> Subject: Digest Footer
>>>
>>> _______________________________________________
>>> CZT-Devel mailing list
>>> CZT...@li...
>>> https://lists.sourceforge.net/lists/listinfo/czt-devel
>>>
>>>
>>> ------------------------------
>>>
>>> End of CZT-Devel Digest, Vol 64, Issue 1
>>> ****************************************
>>>
>>>

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

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

Hei Prof. Mark Utting,

Thanks for your reply.
As you say the tool should handle invalid input gracefully.
I am not a member Sourceforge CZT so do not have permission to create a
ticket. Could you add it please?


(The content of the Z doesn't matter - although see my reply to Anthony
Hall - and was reduced simply to reproduce the error.
The Boolean type I use in the reply to Anthony is defined as
* a set of schemas:*
*False *== [ | *false *]
*True *== [ | *true *]
*Boolean *== { *False*, *True *}
which I borrowed from Ian Toyn.)

(The cut-and-paste works because the characters are Unicode.
You might like this web site for displayable characters
<https://www.codetable.net/groups> which you can use in Word and in HTML
and others.)

With thanks,
julian





On Tue, 2 Jun 2020 at 08:51, Mark Utting <bm....@gm...> wrote:

> Anthony and Julian
>
> The error message is clearer with Java 8 (than with later Java versions
> which use modules):
>
> java.lang.ClassCastException:
> net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to
> net.sourceforge.czt.z.ast.ProdType
>         at
> net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:173)
>         at
> net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:39)
>
> I think this is actually caused by a type error in the input specification.
>
> *r*  _ : *seq X*
>
>
>
> ∀ *s *: *seq X * ⦁
>
>           *r* *s *⇔ ( ∃ *i *: 1..#*s *⦁ ¬*s*⟨*i*⟩ )
> (That's pretty neat, that a copy-paste from the Word doc translates to
> HTML in this email!)
>
> Firstly, Z does not have a boolean type, so it is not clear what the
> predicate inside the exists means.
> Secondly, the type of 'r' probably needs to be '\power (\seq X)'.
> (See 'disjoint' in the ISO standard Z library for an example of a prefix
> relation).
>
> That said, the CZT typechecker should give a nice type checking error
> message, not throw a cast exception!
> So Julian, please feel free to report this as a typechecker bug on the
> Sourceforge repository.
>
> Cheers
> Mark
>
>
>
> On Mon, 1 Jun 2020 at 19:45, <an...@an...> wrote:
>
>> Dear Mark
>>
>>
>>
>> The Z Word Tools certainly work OK with Word 2007, so that isn’t the
>> problem.  I’m trying to look into this myself but my Java configuration
>> seems to be broken at the moment. The generated file temp.zedB looks to me
>> as if it’s  a correct translation of the Word Document. Can you please tell
>> me whether it goes through CZT correctly? If so, then the problem must be
>> with the subset snapshot of CZT that ZWT uses and I will have to fix that –
>> which I fear may take me some time! If not, does it give the error that
>> Julian is seeing, or something different?
>>
>>
>>
>> All the best
>>
>>
>>
>> Anthony
>>
>> (Z Word Tools developer)
>>
>>
>>
>> *From:* Mark Utting [mailto:bm....@gm...]
>> *Sent:* 01 June 2020 01:21
>> *To:* czt-devel
>> *Subject:* Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1
>>
>>
>>
>> Julian
>>
>>
>>
>> I'm not very familiar with ZWTools architecture, but this looks like some
>> kind of version or configuration problem.
>>
>>
>>
>> I suggest you try with a more recent version of Word, that is more likely
>> to have been tested with ZWTools.
>>
>> Such as Word 2013.
>>
>>
>>
>> Cheers
>>
>> Mark
>>
>>
>>
>>
>>
>> On Mon, 1 Jun 2020 at 10:12, <czt...@li...>
>> wrote:
>>
>> Send CZT-Devel mailing list submissions to
>>         czt...@li...
>>
>> To subscribe or unsubscribe via the World Wide Web, visit
>>         https://lists.sourceforge.net/lists/listinfo/czt-devel
>> or, via email, send a message with subject or body 'help' to
>>         czt...@li...
>>
>> You can reach the person managing the list at
>>         czt...@li...
>>
>> When replying, please edit your Subject line so it is more specific
>> than "Re: Contents of CZT-Devel digest..."
>>
>>
>> Today's Topics:
>>
>>    1. bug report: net.sourceforge.czt.typecheck.z.PredChecker
>>       (Julian Rose)
>>
>>
>> ----------------------------------------------------------------------
>>
>> Message: 1
>> Date: Fri, 29 May 2020 10:20:58 +0800
>> From: Julian Rose <jro...@gm...>
>> To: czt...@li...
>> Cc: Julian Rose <jro...@gm...>
>> Subject: [CZT-Devel] bug report:
>>         net.sourceforge.czt.typecheck.z.PredChecker
>> Message-ID:
>>         <
>> CAH...@ma...>
>> Content-Type: text/plain; charset="utf-8"
>>
>> Hei,
>>
>> Summary.....: A general Throwable exception has happened - class
>> net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
>> net.sourceforge.czt.z.ast.ProdType
>> (net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
>> net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
>> Exception...: java.lang.ClassCastException
>> Cause.......: none
>>
>> I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
>> configured for CZT type-checking with option ?Allow use before
>> declaration?.
>>
>> The ZWordTools-generated temp.bat file contains (java -jar
>>
>> "C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
>> -d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
>> Please see attached files.
>> Including a minimal temp.docx to reproduce the error.
>> The temp.ztr file is empty.
>>
>> With thanks,
>> julian
>> -------------- next part --------------
>> An HTML attachment was scrubbed...
>> -------------- next part --------------
>> A non-text attachment was scrubbed...
>> Name: temp.zed8
>> Type: application/octet-stream
>> Size: 129 bytes
>> Desc: not available
>> -------------- next part --------------
>> A non-text attachment was scrubbed...
>> Name: temp.zte
>> Type: application/octet-stream
>> Size: 3827 bytes
>> Desc: not available
>> -------------- next part --------------
>> A non-text attachment was scrubbed...
>> Name: temp.docx
>> Type:
>> application/vnd.openxmlformats-officedocument.wordprocessingml.document
>> Size: 45196 bytes
>> Desc: not available
>>
>> ------------------------------
>>
>>
>>
>> ------------------------------
>>
>> Subject: Digest Footer
>>
>> _______________________________________________
>> CZT-Devel mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-devel
>>
>>
>> ------------------------------
>>
>> End of CZT-Devel Digest, Vol 64, Issue 1
>> ****************************************
>>
>>

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

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

Anthony and Julian

The error message is clearer with Java 8 (than with later Java versions
which use modules):

java.lang.ClassCastException:
net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to
net.sourceforge.czt.z.ast.ProdType
        at
net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:173)
        at
net.sourceforge.czt.typecheck.z.PredChecker.visitMemPred(PredChecker.java:39)

I think this is actually caused by a type error in the input specification.

*r*  _ : *seq X*



∀ *s *: *seq X * ⦁

          *r* *s *⇔ ( ∃ *i *: 1..#*s *⦁ ¬*s*⟨*i*⟩ )
(That's pretty neat, that a copy-paste from the Word doc translates to HTML
in this email!)

Firstly, Z does not have a boolean type, so it is not clear what the
predicate inside the exists means.
Secondly, the type of 'r' probably needs to be '\power (\seq X)'.
(See 'disjoint' in the ISO standard Z library for an example of a prefix
relation).

That said, the CZT typechecker should give a nice type checking error
message, not throw a cast exception!
So Julian, please feel free to report this as a typechecker bug on the
Sourceforge repository.

Cheers
Mark



On Mon, 1 Jun 2020 at 19:45, <an...@an...> wrote:

> Dear Mark
>
>
>
> The Z Word Tools certainly work OK with Word 2007, so that isn’t the
> problem.  I’m trying to look into this myself but my Java configuration
> seems to be broken at the moment. The generated file temp.zedB looks to me
> as if it’s  a correct translation of the Word Document. Can you please tell
> me whether it goes through CZT correctly? If so, then the problem must be
> with the subset snapshot of CZT that ZWT uses and I will have to fix that –
> which I fear may take me some time! If not, does it give the error that
> Julian is seeing, or something different?
>
>
>
> All the best
>
>
>
> Anthony
>
> (Z Word Tools developer)
>
>
>
> *From:* Mark Utting [mailto:bm....@gm...]
> *Sent:* 01 June 2020 01:21
> *To:* czt-devel
> *Subject:* Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1
>
>
>
> Julian
>
>
>
> I'm not very familiar with ZWTools architecture, but this looks like some
> kind of version or configuration problem.
>
>
>
> I suggest you try with a more recent version of Word, that is more likely
> to have been tested with ZWTools.
>
> Such as Word 2013.
>
>
>
> Cheers
>
> Mark
>
>
>
>
>
> On Mon, 1 Jun 2020 at 10:12, <czt...@li...>
> wrote:
>
> Send CZT-Devel mailing list submissions to
>         czt...@li...
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://lists.sourceforge.net/lists/listinfo/czt-devel
> or, via email, send a message with subject or body 'help' to
>         czt...@li...
>
> You can reach the person managing the list at
>         czt...@li...
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of CZT-Devel digest..."
>
>
> Today's Topics:
>
>    1. bug report: net.sourceforge.czt.typecheck.z.PredChecker
>       (Julian Rose)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Fri, 29 May 2020 10:20:58 +0800
> From: Julian Rose <jro...@gm...>
> To: czt...@li...
> Cc: Julian Rose <jro...@gm...>
> Subject: [CZT-Devel] bug report:
>         net.sourceforge.czt.typecheck.z.PredChecker
> Message-ID:
>         <
> CAH...@ma...>
> Content-Type: text/plain; charset="utf-8"
>
> Hei,
>
> Summary.....: A general Throwable exception has happened - class
> net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
> net.sourceforge.czt.z.ast.ProdType
> (net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
> net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
> Exception...: java.lang.ClassCastException
> Cause.......: none
>
> I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
> configured for CZT type-checking with option ?Allow use before
> declaration?.
>
> The ZWordTools-generated temp.bat file contains (java -jar
>
> "C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
> -d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
> Please see attached files.
> Including a minimal temp.docx to reproduce the error.
> The temp.ztr file is empty.
>
> With thanks,
> julian
> -------------- next part --------------
> An HTML attachment was scrubbed...
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: temp.zed8
> Type: application/octet-stream
> Size: 129 bytes
> Desc: not available
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: temp.zte
> Type: application/octet-stream
> Size: 3827 bytes
> Desc: not available
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: temp.docx
> Type:
> application/vnd.openxmlformats-officedocument.wordprocessingml.document
> Size: 45196 bytes
> Desc: not available
>
> ------------------------------
>
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>
>
> ------------------------------
>
> End of CZT-Devel Digest, Vol 64, Issue 1
> ****************************************
>
>

Re: [CZT-Devel] bug report: net.sourceforge.czt.typecheck.z.PredChecker

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

Hei Anthony Hall,

Thanks for your response.
I posted the bug report because the tool indicated a fault to be reported.

As you point out the source I gave is incorrect Z - it is intended as a
simplified schema that just yields the fault.
FYI the correct schema is:

function (↑◻  _)
└
╷═[X]
↑◻  _ : seq X → Boolean
 |
∀ s : seq X  ⦁
  ∃ ⊥ : X  ⦁
    ↑◻  s ⇔ ¬( ∃ i : 1..#s ⦁ s( i )= ⊥ )
└


Thank you for maintaining the ZWordTools which is very valuable.
Sadly the Eclipse CZT tools don't work with the latest release of Java - I
posted on czt-users a couple of months back - at least on my laptop.
But I don't think the CZT environment is actively supported anymore.

With thanks,
julian




On Mon, 1 Jun 2020 at 23:53, <an...@an...> wrote:

> Dear Julian
>
>
>
> This seems to be a bug in the subset of CZT that is used in Z Word Tools.
> That is a very old snapshot of some  of the CZT code, and I’m trying to
> find out whether the bug is still present in the current version. If not,
> then I will update the Z Word Tools to incorporate the correct version. If
> so, I will need to wait for  the CZT project to fix the problem before
> updating the tools.
>
>
>
> In the meantime, I think the bug is provoked by an error in your Z. I
> think perhaps you intended to declare r as ℙ (*seq X*) . If you do that,
> the typechecker works correctly (and identifies a subsequent problem with
> the application s <i>: that’s incorrect because s is a function from n to
> X, and you ae applying it to a sequence containing  just the number I as
> its first member).
>
>
>
> I hope that helps, and I’ll get back to you when I have more information
> about the typechecker bug.
>
>
>
> Regards
>
>
>
> Anthony
>
>
>
> *From:* Julian Rose [mailto:jro...@gm...]
> *Sent:* 29 May 2020 03:21
> *To:* czt...@li...
> *Cc:* Julian Rose
> *Subject:* [CZT-Devel] bug report:
> net.sourceforge.czt.typecheck.z.PredChecker
>
>
>
> Hei,
>
>
>
> Summary.....: A general Throwable exception has happened - class
> net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
> net.sourceforge.czt.z.ast.ProdType
> (net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
> net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
> Exception...: java.lang.ClassCastException
> Cause.......: none
>
>
>
> I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
> configured for CZT type-checking with option “Allow use before
> declaration”.
>
>
>
> The ZWordTools-generated temp.bat file contains (java -jar
> "C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
> -d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
>
> Please see attached files.
>
> Including a minimal temp.docx to reproduce the error.
>
> The temp.ztr file is empty.
>
>
>
> With thanks,
>
> julian
>
>
>

Re: [CZT-Devel] bug report: net.sourceforge.czt.typecheck.z.PredChecker

[<an...@an...>]

Dear Julian

 

This seems to be a bug in the subset of CZT that is used in Z Word Tools. That is a very old snapshot of some  of the CZT code, and I’m trying to find out whether the bug is still present in the current version. If not, then I will update the Z Word Tools to incorporate the correct version. If so, I will need to wait for  the CZT project to fix the problem before updating the tools.

 

In the meantime, I think the bug is provoked by an error in your Z. I think perhaps you intended to declare r as ℙ (seq X) . If you do that, the typechecker works correctly (and identifies a subsequent problem with the application s <i>: that’s incorrect because s is a function from n to X, and you ae applying it to a sequence containing  just the number I as its first member).

 

I hope that helps, and I’ll get back to you when I have more information about the typechecker bug.

 

Regards

 

Anthony

 

From: Julian Rose [mailto:jro...@gm...] 
Sent: 29 May 2020 03:21
To: czt...@li...
Cc: Julian Rose
Subject: [CZT-Devel] bug report: net.sourceforge.czt.typecheck.z.PredChecker

 

Hei,

 

Summary.....: A general Throwable exception has happened - class net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class net.sourceforge.czt.z.ast.ProdType (net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
Exception...: java.lang.ClassCastException
Cause.......: none

 

I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1 configured for CZT type-checking with option “Allow use before declaration”. 

 

The ZWordTools-generated temp.bat file contains (java -jar "C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar" -d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")

Please see attached files.

Including a minimal temp.docx to reproduce the error.

The temp.ztr file is empty.

 

With thanks,

julian

 

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

[B_londeix <b_l...@te...>]

Hello All,

 

I do not know why I received this email, I am not part of this current problem.

But I am pleased to see that Z and its support tool Z Word is being used.

 

I have been using it a few years ago and was happy with it. I will have the occasion of using it again in a few months (Windows 10, Microsoft 365 Word). Could you let me know of the new version? Download? And new user guide?

 

Thanks,

 

Best regards,

 

Bernard Londeix

Telmaco Ltd

COSMIC IAC France

 

49B Myddleton Road

London  N22 8LZ

PCa: 9C3XJV4M+GX

M: +44 7768 588 419 (WhatsApp)

E:  b_l...@te...

W: https://telmaco.com

 

From: an...@an... <an...@an...> 
Sent: 01 June 2020 10:45
To: bm....@gm...; 'czt-devel' <czt...@li...>
Cc: jro...@gm...
Subject: Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

 

Dear Mark

 

The Z Word Tools certainly work OK with Word 2007, so that isn’t the problem.  I’m trying to look into this myself but my Java configuration seems to be broken at the moment. The generated file temp.zedB looks to me as if it’s  a correct translation of the Word Document. Can you please tell me whether it goes through CZT correctly? If so, then the problem must be with the subset snapshot of CZT that ZWT uses and I will have to fix that – which I fear may take me some time! If not, does it give the error that Julian is seeing, or something different?

 

All the best

 

Anthony

(Z Word Tools developer)

 

From: Mark Utting [mailto:bm....@gm...] 
Sent: 01 June 2020 01:21
To: czt-devel
Subject: Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

 

Julian

 

I'm not very familiar with ZWTools architecture, but this looks like some kind of version or configuration problem.

 

I suggest you try with a more recent version of Word, that is more likely to have been tested with ZWTools.

Such as Word 2013.

 

Cheers

Mark

 

 

On Mon, 1 Jun 2020 at 10:12, <czt...@li... <mailto:czt...@li...> > wrote:

Send CZT-Devel mailing list submissions to
        czt...@li... <mailto:czt...@li...> 

To subscribe or unsubscribe via the World Wide Web, visit
        https://lists.sourceforge.net/lists/listinfo/czt-devel
or, via email, send a message with subject or body 'help' to
        czt...@li... <mailto:czt...@li...> 

You can reach the person managing the list at
        czt...@li... <mailto:czt...@li...> 

When replying, please edit your Subject line so it is more specific
than "Re: Contents of CZT-Devel digest..."


Today's Topics:

   1. bug report: net.sourceforge.czt.typecheck.z.PredChecker
      (Julian Rose)


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

Message: 1
Date: Fri, 29 May 2020 10:20:58 +0800
From: Julian Rose <jro...@gm... <mailto:jro...@gm...> >
To: czt...@li... <mailto:czt...@li...> 
Cc: Julian Rose <jro...@gm... <mailto:jro...@gm...> >
Subject: [CZT-Devel] bug report:
        net.sourceforge.czt.typecheck.z.PredChecker
Message-ID:
        <CAH...@ma... <mailto:CAHUeuCEFFeGF5L-z%2B98Zbg%2BS...@ma...> >
Content-Type: text/plain; charset="utf-8"

Hei,

Summary.....: A general Throwable exception has happened - class
net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
net.sourceforge.czt.z.ast.ProdType
(net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
Exception...: java.lang.ClassCastException
Cause.......: none

I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
configured for CZT type-checking with option ?Allow use before
declaration?.

The ZWordTools-generated temp.bat file contains (java -jar
"C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
-d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
Please see attached files.
Including a minimal temp.docx to reproduce the error.
The temp.ztr file is empty.

With thanks,
julian
-------------- next part --------------
An HTML attachment was scrubbed...
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.zed8
Type: application/octet-stream
Size: 129 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.zte
Type: application/octet-stream
Size: 3827 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.docx
Type: application/vnd.openxmlformats-officedocument.wordprocessingml.document
Size: 45196 bytes
Desc: not available

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



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

Subject: Digest Footer

_______________________________________________
CZT-Devel mailing list
CZT...@li... <mailto:CZT...@li...> 
https://lists.sourceforge.net/lists/listinfo/czt-devel


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

End of CZT-Devel Digest, Vol 64, Issue 1
****************************************

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

[<an...@an...>]

Dear Mark

 

The Z Word Tools certainly work OK with Word 2007, so that isn’t the problem.  I’m trying to look into this myself but my Java configuration seems to be broken at the moment. The generated file temp.zedB looks to me as if it’s  a correct translation of the Word Document. Can you please tell me whether it goes through CZT correctly? If so, then the problem must be with the subset snapshot of CZT that ZWT uses and I will have to fix that – which I fear may take me some time! If not, does it give the error that Julian is seeing, or something different?

 

All the best

 

Anthony

(Z Word Tools developer)

 

From: Mark Utting [mailto:bm....@gm...] 
Sent: 01 June 2020 01:21
To: czt-devel
Subject: Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

 

Julian

 

I'm not very familiar with ZWTools architecture, but this looks like some kind of version or configuration problem.

 

I suggest you try with a more recent version of Word, that is more likely to have been tested with ZWTools.

Such as Word 2013.

 

Cheers

Mark

 

 

On Mon, 1 Jun 2020 at 10:12, <czt...@li...> wrote:

Send CZT-Devel mailing list submissions to
        czt...@li...

To subscribe or unsubscribe via the World Wide Web, visit
        https://lists.sourceforge.net/lists/listinfo/czt-devel
or, via email, send a message with subject or body 'help' to
        czt...@li...

You can reach the person managing the list at
        czt...@li...

When replying, please edit your Subject line so it is more specific
than "Re: Contents of CZT-Devel digest..."


Today's Topics:

   1. bug report: net.sourceforge.czt.typecheck.z.PredChecker
      (Julian Rose)


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

Message: 1
Date: Fri, 29 May 2020 10:20:58 +0800
From: Julian Rose <jro...@gm...>
To: czt...@li...
Cc: Julian Rose <jro...@gm...>
Subject: [CZT-Devel] bug report:
        net.sourceforge.czt.typecheck.z.PredChecker
Message-ID:
        <CAH...@ma... <mailto:CAHUeuCEFFeGF5L-z%2B98Zbg%2BS...@ma...> >
Content-Type: text/plain; charset="utf-8"

Hei,

Summary.....: A general Throwable exception has happened - class
net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
net.sourceforge.czt.z.ast.ProdType
(net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
Exception...: java.lang.ClassCastException
Cause.......: none

I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
configured for CZT type-checking with option ?Allow use before
declaration?.

The ZWordTools-generated temp.bat file contains (java -jar
"C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
-d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
Please see attached files.
Including a minimal temp.docx to reproduce the error.
The temp.ztr file is empty.

With thanks,
julian
-------------- next part --------------
An HTML attachment was scrubbed...
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.zed8
Type: application/octet-stream
Size: 129 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.zte
Type: application/octet-stream
Size: 3827 bytes
Desc: not available
-------------- next part --------------
A non-text attachment was scrubbed...
Name: temp.docx
Type: application/vnd.openxmlformats-officedocument.wordprocessingml.document
Size: 45196 bytes
Desc: not available

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



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

Subject: Digest Footer

_______________________________________________
CZT-Devel mailing list
CZT...@li...
https://lists.sourceforge.net/lists/listinfo/czt-devel


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

End of CZT-Devel Digest, Vol 64, Issue 1
****************************************

Re: [CZT-Devel] CZT-Devel Digest, Vol 64, Issue 1

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

Julian

I'm not very familiar with ZWTools architecture, but this looks like some
kind of version or configuration problem.

I suggest you try with a more recent version of Word, that is more likely
to have been tested with ZWTools.
Such as Word 2013.

Cheers
Mark


On Mon, 1 Jun 2020 at 10:12, <czt...@li...>
wrote:

> Send CZT-Devel mailing list submissions to
>         czt...@li...
>
> To subscribe or unsubscribe via the World Wide Web, visit
>         https://lists.sourceforge.net/lists/listinfo/czt-devel
> or, via email, send a message with subject or body 'help' to
>         czt...@li...
>
> You can reach the person managing the list at
>         czt...@li...
>
> When replying, please edit your Subject line so it is more specific
> than "Re: Contents of CZT-Devel digest..."
>
>
> Today's Topics:
>
>    1. bug report: net.sourceforge.czt.typecheck.z.PredChecker
>       (Julian Rose)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Fri, 29 May 2020 10:20:58 +0800
> From: Julian Rose <jro...@gm...>
> To: czt...@li...
> Cc: Julian Rose <jro...@gm...>
> Subject: [CZT-Devel] bug report:
>         net.sourceforge.czt.typecheck.z.PredChecker
> Message-ID:
>         <
> CAH...@ma...>
> Content-Type: text/plain; charset="utf-8"
>
> Hei,
>
> Summary.....: A general Throwable exception has happened - class
> net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
> net.sourceforge.czt.z.ast.ProdType
> (net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
> net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
> Exception...: java.lang.ClassCastException
> Cause.......: none
>
> I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
> configured for CZT type-checking with option ?Allow use before
> declaration?.
>
> The ZWordTools-generated temp.bat file contains (java -jar
>
> "C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
> -d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
> Please see attached files.
> Including a minimal temp.docx to reproduce the error.
> The temp.ztr file is empty.
>
> With thanks,
> julian
> -------------- next part --------------
> An HTML attachment was scrubbed...
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: temp.zed8
> Type: application/octet-stream
> Size: 129 bytes
> Desc: not available
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: temp.zte
> Type: application/octet-stream
> Size: 3827 bytes
> Desc: not available
> -------------- next part --------------
> A non-text attachment was scrubbed...
> Name: temp.docx
> Type:
> application/vnd.openxmlformats-officedocument.wordprocessingml.document
> Size: 45196 bytes
> Desc: not available
>
> ------------------------------
>
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>
>
> ------------------------------
>
> End of CZT-Devel Digest, Vol 64, Issue 1
> ****************************************
>

[CZT-Devel] bug report: net.sourceforge.czt.typecheck.z.PredChecker

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

Hei,

Summary.....: A general Throwable exception has happened - class
net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class
net.sourceforge.czt.z.ast.ProdType
(net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and
net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
Exception...: java.lang.ClassCastException
Cause.......: none

I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1
configured for CZT type-checking with option “Allow use before
declaration”.

The ZWordTools-generated temp.bat file contains (java -jar
"C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar"
-d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")
Please see attached files.
Including a minimal temp.docx to reproduce the error.
The temp.ztr file is empty.

With thanks,
julian

[CZT-Devel] CZT project questions

[Javier B. <jav...@gm...>]

Hi, my name is Javier and a month ago I started working on a project that
uses CZT libraries. In order to have the source code I tried installing it
following the instructions in
http://czt.sourceforge.net/dev/setup.html
but I had a few troubles (not setted dependencies, test failures, etc.)

What I need to know if I'm in the right place to ask about these type of
issues?

If not, please tell me where I have to post.


Thanks in advance.
Javier Bonet.

[CZT-Devel] CZT and others

[Lyle <web...@co...>]

Hi,

I'm studying Software Engineering Mathematics and Z, and I'm finding CZT 
very helpful. Unfortunately it seems like this project has slowed down 
in recent years?

I'm looking at different options for Z animation. I've been playing with 
zLive which works great in many instances, but is not implemented in 
others. I've read about other tools for animation here:

http://www.cs.waikato.ac.nz/~marku/formalmethods.html

but it appears that the links to them are now all broken and I can't 
find any downloads when using google.

Does anyone know where I can find things like PiZA, Possum, etc?


Lyle

[CZT-Devel] CZT Development

[David M. <dav...@wo...>]

Hello, 

I just tried out v1.6 of the CZ toolkit today and its a great little piece of kit! 

Many thanks to all contributors!

Are there any plans for version 2.0 - the code sources don’t seem to have been worked on recently - well not since August 2015.

Are there any plugins which integrate with Ecore models, in particular would it be possible to convert a specification in  Z to ECore(plusOCL) and from that generate code?

If not then I’d be tempted to have a crack at it.

Regards

David Milward

[CZT-Devel] To Develop a Z Analysis Tool

[Cristian V. S. <vid...@ms...>]

Hey Dear.

Since I've already proposed Object-Z extensions for Aspect-Oriented AO Z 
models, I need to work on an AO Z analysis tool; thus, I'd like to know 
tools for doing it as part of CZT. For my background, I can work on 
programming; but, maybe there are other approaches for it.

If I can appreciate a simple Z analysis example, I'd get the necessary 
knowledge to develop an AO Z tool.

I wait for your comments ASAP.

Sincerely,

Cristian Vidal Silva.

Re: [CZT-Devel] Stable versions of cup plugin on maven

[Andrius V. <and...@ne...>]

Dear Roland,

I have re-run the CZT build and indicated to build all /dev tools with Java
7 compatibility. Does the -SNAPSHOT version work for you now?

Andrius

On Thu, 13 Aug 2015 at 11:30 Andrius Velykis <
and...@ne...> wrote:

> Oops - that must be me who did the changes (I am trying to fix the builds
> and thus using Java 8 as I don't have the resources to test on older
> systems..). I did not realise someone was using the cup-maven-plugin. I
> will try to figure something out and possibly release the development
> tools. Is it just the cup-maven-plugin you are using? And which Java
> version are you depending on? Java 7 has reached the end of life..
>
> On a side note, I have noticed recently that CUP got new development:
> http://www2.cs.tum.edu/projects/cup/, there is now 0.11b version.. Our
> fork was on 0.11a - we possibly have to look to upgrade to the newer
> version. So there is more work here as well.
>
> Regarding "releasing" - it has been long, sorry. We will see what could be
> done about this.
>
> Best regards,
> Andrius
>
>
>
> On Thu, 13 Aug 2015 at 11:02 Roland Ziegler <rol...@it...>
> wrote:
>
>> Dear All
>>
>> On the page http://sourceforge.net/projects/czt/files/maven/ is the
>> information, that the CZT libraries will be accessible on Maven Central
>> after a "release".
>>
>> Up to now I can still access only the snapshot release. Since a change
>> in the cup-maven-plugin last night the plugin needs JDK 8 to build,
>> which is a problem with my server configuration.
>>
>> Is there any way to access stable versions over a maven repository? Or
>> can you tell me when the release versions will be available over maven?
>>
>> Kind regards
>> Roland
>>
>> --
>> Roland Ziegler                                http://www.itds.ch
>> Entwicklung                                   IT & Design Solutions GmbH
>> Tel: 031 781 40 21                                        Skype: itds.ch
>>
>> Besuchen Sie unsere neue Webcam: http://www.itds.ch/de/webcam?m
>>
>>
>>
>> ------------------------------------------------------------------------------
>> _______________________________________________
>> CZT-Devel mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-devel
>>
>

Re: [CZT-Devel] Stable versions of cup plugin on maven

[Andrius V. <and...@ne...>]

Oops - that must be me who did the changes (I am trying to fix the builds
and thus using Java 8 as I don't have the resources to test on older
systems..). I did not realise someone was using the cup-maven-plugin. I
will try to figure something out and possibly release the development
tools. Is it just the cup-maven-plugin you are using? And which Java
version are you depending on? Java 7 has reached the end of life..

On a side note, I have noticed recently that CUP got new development:
http://www2.cs.tum.edu/projects/cup/, there is now 0.11b version.. Our fork
was on 0.11a - we possibly have to look to upgrade to the newer version. So
there is more work here as well.

Regarding "releasing" - it has been long, sorry. We will see what could be
done about this.

Best regards,
Andrius


On Thu, 13 Aug 2015 at 11:02 Roland Ziegler <rol...@it...> wrote:

> Dear All
>
> On the page http://sourceforge.net/projects/czt/files/maven/ is the
> information, that the CZT libraries will be accessible on Maven Central
> after a "release".
>
> Up to now I can still access only the snapshot release. Since a change
> in the cup-maven-plugin last night the plugin needs JDK 8 to build,
> which is a problem with my server configuration.
>
> Is there any way to access stable versions over a maven repository? Or
> can you tell me when the release versions will be available over maven?
>
> Kind regards
> Roland
>
> --
> Roland Ziegler                                http://www.itds.ch
> Entwicklung                                   IT & Design Solutions GmbH
> Tel: 031 781 40 21                                        Skype: itds.ch
>
> Besuchen Sie unsere neue Webcam: http://www.itds.ch/de/webcam?m
>
>
>
> ------------------------------------------------------------------------------
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
>

[CZT-Devel] Stable versions of cup plugin on maven

[Roland Z. <rol...@it...>]

Dear All

On the page http://sourceforge.net/projects/czt/files/maven/ is the 
information, that the CZT libraries will be accessible on Maven Central 
after a "release".

Up to now I can still access only the snapshot release. Since a change 
in the cup-maven-plugin last night the plugin needs JDK 8 to build, 
which is a problem with my server configuration.

Is there any way to access stable versions over a maven repository? Or 
can you tell me when the release versions will be available over maven?

Kind regards
Roland

-- 
Roland Ziegler                                http://www.itds.ch
Entwicklung                                   IT & Design Solutions GmbH
Tel: 031 781 40 21                                        Skype: itds.ch

Besuchen Sie unsere neue Webcam: http://www.itds.ch/de/webcam?m