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