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