czt-devel — For programmers using the CZT code

Re: [CZT-Devel] installing CZT

[Urmas R. <ur...@ho...>]

Hello,


I have one more question at the moment if its possible.

Is there any tutorial how to animate the specification using CZT?
For example i have simple specification like 

┌AddAB
      a?, b?, c!: ℕ   
     | 
       c! = a?+b?   
└



I would like to get output 3 if i provide inputs 1 and 2.

is it possible to animate the specification using command line?
Is it possible to store outputs in output file and read inputs from input file?
Can this operations be defined in specification or i have to provide inputs as parameters?

Urmas.

From: ur...@ho...
To: czt...@li...
Date: Tue, 11 Oct 2011 10:51:28 +0200
Subject: [CZT-Devel] installing CZT








Hello,

I had recently downloaded the last fixes, and now the installation comes through.
[INFO] Reactor Summary:
[INFO] 
[INFO] Community Z Tools ................................. SUCCESS [1.479s]
[INFO] CZT Util .......................................... SUCCESS [5.354s]
[INFO] CZT Jaxb .......................................... SUCCESS [17.602s]
[INFO] CZT ZML ........................................... SUCCESS [2.448s]
[INFO] CZT GnAST ......................................... SUCCESS [2.387s]
[INFO] CZT GnAST Maven Plugin ............................ SUCCESS [2.791s]
[INFO] CZT Corejava ...................................... SUCCESS [3:22.958s]
[INFO] CZT SpecReader .................................... SUCCESS [4.513s]
[INFO] CZT Session ....................................... SUCCESS [3.272s]
[INFO] CZT Java Cup ...................................... SUCCESS [4.908s]
[INFO] CZT Parser Source ................................. SUCCESS [1.528s]
[INFO] CZT Cup Maven Plugin .............................. SUCCESS [1.329s]
[INFO] CZT Parser ........................................ SUCCESS [1:29.434s]
[INFO] CZT Z Pattern Parser .............................. SUCCESS [20.646s]
[INFO] CZT Typechecker ................................... SUCCESS [25.878s]
[INFO] CZT Rules ......................................... SUCCESS [29.582s]
[INFO] CZT ZLive ......................................... SUCCESS [22.648s]
[INFO] CZT Gaffe ......................................... SUCCESS [11.563s]
[INFO] CZT Gaffe2 ........................................ SUCCESS [4.354s]
[INFO] CZT jEdit plugins ................................. SUCCESS [0.332s]
[INFO] CZT ZLive jEdit Plugin ............................ SUCCESS [1.365s]
[INFO] CZT Object Z Parser ............................... SUCCESS [27.113s]
[INFO] CZT Object-Z Typechecker .......................... SUCCESS [19.771s]
[INFO] CZT Z/Eves (proofs) Parser ........................ SUCCESS [1:30.195s]
[INFO] CZT Z/Eves (proofs) Typechecker ................... SUCCESS [44.580s]
[INFO] CZT Z VCG ......................................... SUCCESS [21.737s]
[INFO] CZT ZSideKick jEdit Plugin ........................ SUCCESS [6.955s]
[INFO] CZT Z Palette jEdit Plugin ........................ SUCCESS [1.407s]
[INFO] CZT Z/Eves Integration ............................ SUCCESS [44.098s]
[INFO] CZT Z/Eves jEdit Plugin ........................... SUCCESS [2.165s]
[INFO] CZT Circus Parser ................................. SUCCESS [1:02.805s]
[INFO] CZT Object Z Pattern Parser ....................... SUCCESS [32.151s]
[INFO] CZT Circus Typechecker ............................ SUCCESS [16.917s]
[INFO] CZT User Interface ................................ SUCCESS [30.234s]
[INFO] CZT Z to B translator ............................. SUCCESS [9.747s]
[INFO] ------------------------------------------------------------------------
[INFO] BUILD SUCCESS
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 14:27.724s
[INFO] Finished at: Tue Oct 11 11:44:46 EEST 2011
[INFO] Final Memory: 47M/769M
[INFO] ------------------------------------------------------------------------

So i have jar files generated in lib folder, will try to attach them with c++ command line.

If somebody has any corresponding experience how to execute CZT from c++ then please let me know to make things simpler.

Thank You,
Urmas.
 		 	   		  

------------------------------------------------------------------------------
All the data continuously generated in your IT infrastructure contains a
definitive record of customers, application performance, security
threats, fraudulent activity and more. Splunk takes this data and makes
sense of it. Business sense. IT sense. Common sense.
http://p.sf.net/sfu/splunk-d2d-oct
_______________________________________________
CZT-Devel mailing list
CZT...@li...
https://lists.sourceforge.net/lists/listinfo/czt-devel 		 	   		  

[CZT-Devel] installing CZT

[Urmas R. <ur...@ho...>]

Hello,

I had recently downloaded the last fixes, and now the installation comes through.
[INFO] Reactor Summary:
[INFO] 
[INFO] Community Z Tools ................................. SUCCESS [1.479s]
[INFO] CZT Util .......................................... SUCCESS [5.354s]
[INFO] CZT Jaxb .......................................... SUCCESS [17.602s]
[INFO] CZT ZML ........................................... SUCCESS [2.448s]
[INFO] CZT GnAST ......................................... SUCCESS [2.387s]
[INFO] CZT GnAST Maven Plugin ............................ SUCCESS [2.791s]
[INFO] CZT Corejava ...................................... SUCCESS [3:22.958s]
[INFO] CZT SpecReader .................................... SUCCESS [4.513s]
[INFO] CZT Session ....................................... SUCCESS [3.272s]
[INFO] CZT Java Cup ...................................... SUCCESS [4.908s]
[INFO] CZT Parser Source ................................. SUCCESS [1.528s]
[INFO] CZT Cup Maven Plugin .............................. SUCCESS [1.329s]
[INFO] CZT Parser ........................................ SUCCESS [1:29.434s]
[INFO] CZT Z Pattern Parser .............................. SUCCESS [20.646s]
[INFO] CZT Typechecker ................................... SUCCESS [25.878s]
[INFO] CZT Rules ......................................... SUCCESS [29.582s]
[INFO] CZT ZLive ......................................... SUCCESS [22.648s]
[INFO] CZT Gaffe ......................................... SUCCESS [11.563s]
[INFO] CZT Gaffe2 ........................................ SUCCESS [4.354s]
[INFO] CZT jEdit plugins ................................. SUCCESS [0.332s]
[INFO] CZT ZLive jEdit Plugin ............................ SUCCESS [1.365s]
[INFO] CZT Object Z Parser ............................... SUCCESS [27.113s]
[INFO] CZT Object-Z Typechecker .......................... SUCCESS [19.771s]
[INFO] CZT Z/Eves (proofs) Parser ........................ SUCCESS [1:30.195s]
[INFO] CZT Z/Eves (proofs) Typechecker ................... SUCCESS [44.580s]
[INFO] CZT Z VCG ......................................... SUCCESS [21.737s]
[INFO] CZT ZSideKick jEdit Plugin ........................ SUCCESS [6.955s]
[INFO] CZT Z Palette jEdit Plugin ........................ SUCCESS [1.407s]
[INFO] CZT Z/Eves Integration ............................ SUCCESS [44.098s]
[INFO] CZT Z/Eves jEdit Plugin ........................... SUCCESS [2.165s]
[INFO] CZT Circus Parser ................................. SUCCESS [1:02.805s]
[INFO] CZT Object Z Pattern Parser ....................... SUCCESS [32.151s]
[INFO] CZT Circus Typechecker ............................ SUCCESS [16.917s]
[INFO] CZT User Interface ................................ SUCCESS [30.234s]
[INFO] CZT Z to B translator ............................. SUCCESS [9.747s]
[INFO] ------------------------------------------------------------------------
[INFO] BUILD SUCCESS
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 14:27.724s
[INFO] Finished at: Tue Oct 11 11:44:46 EEST 2011
[INFO] Final Memory: 47M/769M
[INFO] ------------------------------------------------------------------------

So i have jar files generated in lib folder, will try to attach them with c++ command line.

If somebody has any corresponding experience how to execute CZT from c++ then please let me know to make things simpler.

Thank You,
Urmas.
 		 	   		  

Re: [CZT-Devel] CZT Tool Install and execute from c++

[Leo F. <leo...@ne...>]

Urmas,

Petra's problem was at parser-zeves, yet yours is at typechecker-zeves.
So, they are not related (e.g., and if you get to typechecker-zeves you have
already passed parser-zeves).

Petra's problem is indeed an error, and has just been fixed. Yours, I am still unsure whether
it's something for us or for you to do (e.g., problems with your Maven).

The "-Dmaven.test.skip=true" isn't relevant, I think. It just switches testing off - which is bad in your case.
Could you execute

"mvn -e clean install >> issues.txt"

and send me the output + issues.txt please?

Best,
Leo

On 10 Oct 2011, at 13:26, Urmas Repinski wrote:

Hello, Petra, Leo.

I have an error during installation process.
Some files are missed or cannot be downloaded.

Could not find artifact net.sourceforge.czt:parser-zeves:jar:tests:1.6-SNAPSHOT

Tests are absent in the SVN i think. for CZT Z/Eves (proofs) Typechecker.

By the way, execution of this tests can be switched off using -Dmaven.test.skip=true  option:
mvn -Dmaven.test.skip=true clean install -rf :typechecker-zeves

But they still should be downloaded otherwise the installation error appears.

Hope this helped,
Urmas.






> Date: Tue, 11 Oct 2011 00:02:50 +1300
> From: Pet...@ec...<mailto:Pet...@ec...>
> To: czt...@li...<mailto:czt...@li...>
> Subject: Re: [CZT-Devel] CZT Tool Install and execute from c++
>
> Hi there,
>
> I get the same error:
> [INFO] CZT Z/Eves (proofs) Parser ........................ FAILURE
>
> due to a test failing:
> Tests run: 41, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 29.787
> sec <<< FAILURE!
> Running net.sourceforge.czt.print.zeves.ZmlPrintTest
> Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
>
> Results :
>
> Failed tests:
> null(net.sourceforge.czt.parser.util.CztManagedTest$TestNormal)
> Tests run: 79, Failures: 1, Errors: 0, Skipped: 0
>
> BTW, it is hard to find useful output due to the huge amount of debug
> output like:
> =================================================================
> Direct UNICODE printing of
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8
>
> ============================ TOSTRING ============================
> toString successful for zeveslabels
>
> ==================================================================
> SM UNICODE printing of
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8
>
> ============================ LATEX ============================
> created file
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.tex
>
> ============================ XML ============================
> created file
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.zml
> ==================================================================
>
> Is there a way to switch that off?
>
> Cheers,
> Petra
>
> On 10/10/11 23:20, Leo Freitas wrote:
> > Hi Urmas,
> >
> > I am sorry to hear about this. When committing, I always run CZT clean/install to ensure this doesn't happen.
> > I just rebuilt it here successfully, and double-checked all is in place (e.g., no missing commits). Could you send
> > us the maven detailed info? I think if you run "mvn -e clean install" it gives that.
> >
> > If you reached that far, there might be something wrong on our end. I will double check (e.g., on a fresh machine).
> > By the way, I asked a colleague to download / install in a machine without CZT and it went through successfully.
> > Could you please try again and let me know if you still get the problem?
> >
> > ----
> >
> > About your specification animation, could you explain it a little bit further, please? I mean, there is the ZLive animator,
> > which would enable you to "execute" Z specifications that are concrete enough (and with contained enough types).
> >
> > How is that to be linked with C++? I mean, what' s the role of the Z specification for you? Is it to define the C++ code
> > functional correctness? Or is for the C memory model / run-time exceptions? What is it you are trying to achieve?
> >
> > Best,
> > Leo
> >
> > On 10 Oct 2011, at 10:41, Urmas Repinski wrote:
> >
> > Hello,
> >
> > I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++.
> >
> > First of all i want to install CZT on my PC.
> >
> > I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached
> >
> > [INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s]
> > [INFO] CZT Z VCG ......................................... SKIPPED
> > [INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED
> > [INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED
> > [INFO] CZT Z/Eves Integration ............................ SKIPPED
> > ....
> >
> >
> > So maybe i have to use any other mirror to download archives that are required during installation?
> > I had tried all mirrors that are in MAVEN website -
> >
> > http://maven.apache.org/guides/mini/guide-mirror-settings.html
> >
> > But this does not solve the problem, the installation does not finish.
> >
> > And one more problem, can i after the installation animate simple Z specifications from c++ code?
> >
> > If yes then please somebody replay me how can i do that?
> >
> > Thank you very much,
> > Urmas Repinski.
> > <ATT00001..txt><ATT00002..txt>
> >
> >
> > ------------------------------------------------------------------------------
> > All the data continuously generated in your IT infrastructure contains a
> > definitive record of customers, application performance, security
> > threats, fraudulent activity and more. Splunk takes this data and makes
> > sense of it. Business sense. IT sense. Common sense.
> > http://p.sf.net/sfu/splunk-d2dcopy1
> > _______________________________________________
> > CZT-Devel mailing list
> > CZT...@li...<mailto:CZT...@li...>
> > https://lists.sourceforge.net/lists/listinfo/czt-devel
>
>
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure contains a
> definitive record of customers, application performance, security
> threats, fraudulent activity and more. Splunk takes this data and makes
> sense of it. Business sense. IT sense. Common sense.
> http://p.sf.net/sfu/splunk-d2dcopy1
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...<mailto:CZT...@li...>
> https://lists.sourceforge.net/lists/listinfo/czt-devel
<ATT00001..txt><ATT00002..txt>

Re: [CZT-Devel] CZT Tool Install and execute from c++

[Leo F. <leo...@ne...>]

Hi Petra,

That's very helpful, thank you. It doesn't happen with my build, but I think I figured out why it does on yours.
The way to check if we are talking about the same problem is to clean and build, and it shouldn't happen.
Notice that the need for the clean-install maybe needed for other reasons, like out-of-memory when handling
too many (large) tests as a result of the extra tests created on the fly.

Cutting a long story short, the reason for this is because of a combination of factors: ZEves proof keywords use in declarations;
special names only allowed by the prover; CZT markup translations (e.g., Latex->Unicode->Latex); Latex markup directive handling, etc.

The source of the problem is when translating from tex-zed8, then back from zed8->tex. The issue is with ZEves use of "proof" keywords 
in "special" declared names (E.g., names only the prover can declare - containing $). They can be used in expressions/predicates, though. 
The issue is that the Unicode2Latex doesn't add necessary hardspaces for this(ese) kind of names. That is, in Latex

(R \cup S) ~applies\$to~ x

(as in appTo.tex) leads to this in Unicode when converted from Latex

( R ∪ S ) applies$to x 

which then leads to this when converted back to Latex (from Unicode)

(R \cup S) applies\$to x

because applies$to is an infix function (operator template), then no hard spaces is added. 
The overall solution I added was to force this special case at the Unicode2Latex markup printer, 
such that these case gets handled properly. 

Also, notice that the problem only happens if you use the zed8->tex printer for this peculiar operator template.... 
ZEves makes a poor naming convention here, I should say. All should be okay now.

Thanks for spotting this.
Leo

On 10 Oct 2011, at 12:55, Petra Dietrich wrote:

> Hi Leo,
> 
> That's better; I can now see the error messages.
> See below what maven prints and attached the detailed report for
> ProofScriptParsingTest.
> 
> Cheers,
> Petra
> 
> Running net.sourceforge.czt.parser.zeves.ProofScriptParsingTest
> Number of tests for Z/Eves proofs parsing: 121
> 
> Encountered exception during reparsing
> net.sourceforge.czt.session.CommandException
> 
> Unexpected exception
> 	File     :
> file:/home/petra/czt/parser-zeves/target/test-classes/tests/zeves/instantiateTest.tex.zml
> 	Exception: net.sourceforge.czt.session.CommandException: Key
> (instantiateTest.tex,interface net.sourceforge.czt.z.ast.Spec) not
> computed by net.sourceforge.czt.parser.zeves.ParseUtils@2bccb2
> 	Cause    : null
> Encountered exception during reparsing
> net.sourceforge.czt.session.CommandException
> 
> ... and lots of similar ones.
> <net.sourceforge.czt.parser.zeves.ProofScriptParsingTest.txt><ATT00001..txt><ATT00002..txt>

Re: [CZT-Devel] CZT Tool Install and execute from c++

[Urmas R. <ur...@ho...>]

Hello, Petra, Leo.

I have an error during installation process.
Some files are missed or cannot be downloaded. 

Could not find artifact net.sourceforge.czt:parser-zeves:jar:tests:1.6-SNAPSHOT 

Tests are absent in the SVN i think. for CZT Z/Eves (proofs) Typechecker.

By the way, execution of this tests can be switched off using -Dmaven.test.skip=true  option:
mvn -Dmaven.test.skip=true clean install -rf :typechecker-zeves

But they still should be downloaded otherwise the installation error appears.

Hope this helped,
Urmas.






> Date: Tue, 11 Oct 2011 00:02:50 +1300
> From: Pet...@ec...
> To: czt...@li...
> Subject: Re: [CZT-Devel] CZT Tool Install and execute from c++
> 
> Hi there,
> 
> I get the same error:
> [INFO] CZT Z/Eves (proofs) Parser ........................ FAILURE
> 
> due to a test failing:
> Tests run: 41, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 29.787
> sec <<< FAILURE!
> Running net.sourceforge.czt.print.zeves.ZmlPrintTest
> Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
> 
> Results :
> 
> Failed tests:
>   null(net.sourceforge.czt.parser.util.CztManagedTest$TestNormal)
> Tests run: 79, Failures: 1, Errors: 0, Skipped: 0
> 
> BTW, it is hard to find useful output due to the huge amount of debug
> output like:
> =================================================================
> Direct UNICODE printing of
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8
> 
> ============================ TOSTRING ============================
>   toString successful for zeveslabels
> 
> ==================================================================
> SM UNICODE printing of
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8
> 
> ============================ LATEX    ============================
>   created file
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.tex
> 
> ============================ XML      ============================
>   created file
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.zml
> ==================================================================
> 
> Is there a way to switch that off?
> 
> Cheers,
> Petra
> 
> On 10/10/11 23:20, Leo Freitas wrote:
> > Hi Urmas,
> > 
> > I am sorry to hear about this. When committing, I always run CZT clean/install to ensure this doesn't happen.
> > I just rebuilt it here successfully, and double-checked all is in place (e.g., no missing commits). Could you send
> > us the maven detailed info? I think if you run  "mvn -e clean install" it gives that.
> > 
> > If you reached that far, there might be something wrong on our end. I will double check (e.g., on a fresh machine).
> > By the way, I asked a colleague to download / install in a machine without CZT and it went through successfully.
> > Could you please try again and let me know if you still get the problem?
> > 
> > ----
> > 
> > About your specification animation, could you explain it a little bit further, please? I mean, there is the ZLive animator,
> > which would enable you to "execute" Z specifications that are concrete enough (and with contained enough types).
> > 
> > How is that to be linked with C++? I mean, what' s the role of the Z specification for you? Is it to define the C++ code
> > functional correctness? Or is for the C memory model / run-time exceptions? What is it you are trying to achieve?
> > 
> > Best,
> > Leo
> > 
> > On  10 Oct 2011, at 10:41, Urmas Repinski wrote:
> > 
> > Hello,
> > 
> > I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++.
> > 
> > First of all i want to install CZT on my PC.
> > 
> > I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached
> > 
> > [INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s]
> > [INFO] CZT Z VCG ......................................... SKIPPED
> > [INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED
> > [INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED
> > [INFO] CZT Z/Eves Integration ............................ SKIPPED
> > ....
> > 
> > 
> > So maybe i have to use any other mirror to download archives that are required during installation?
> > I had tried all mirrors that are in MAVEN website -
> > 
> > http://maven.apache.org/guides/mini/guide-mirror-settings.html
> > 
> > But this does not solve the problem, the installation does not finish.
> > 
> > And one more problem, can i after the installation animate simple Z specifications from c++ code?
> > 
> > If yes then please somebody replay me how can i do that?
> > 
> > Thank you very much,
> > Urmas Repinski.
> > <ATT00001..txt><ATT00002..txt>
> > 
> > 
> > ------------------------------------------------------------------------------
> > All the data continuously generated in your IT infrastructure contains a
> > definitive record of customers, application performance, security
> > threats, fraudulent activity and more. Splunk takes this data and makes
> > sense of it. Business sense. IT sense. Common sense.
> > http://p.sf.net/sfu/splunk-d2dcopy1
> > _______________________________________________
> > CZT-Devel mailing list
> > CZT...@li...
> > https://lists.sourceforge.net/lists/listinfo/czt-devel
> 
> 
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure contains a
> definitive record of customers, application performance, security
> threats, fraudulent activity and more. Splunk takes this data and makes
> sense of it. Business sense. IT sense. Common sense.
> http://p.sf.net/sfu/splunk-d2dcopy1
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
 		 	   		  

Re: [CZT-Devel] CZT Tool Install and execute from c++

[Petra D. <Pet...@ec...>]

Hi Leo,

That's better; I can now see the error messages.
See below what maven prints and attached the detailed report for
ProofScriptParsingTest.

Cheers,
Petra

Running net.sourceforge.czt.parser.zeves.ProofScriptParsingTest
Number of tests for Z/Eves proofs parsing: 121

Encountered exception during reparsing
net.sourceforge.czt.session.CommandException

Unexpected exception
	File     :
file:/home/petra/czt/parser-zeves/target/test-classes/tests/zeves/instantiateTest.tex.zml
	Exception: net.sourceforge.czt.session.CommandException: Key
(instantiateTest.tex,interface net.sourceforge.czt.z.ast.Spec) not
computed by net.sourceforge.czt.parser.zeves.ParseUtils@2bccb2
	Cause    : null
Encountered exception during reparsing
net.sourceforge.czt.session.CommandException

... and lots of similar ones.

Re: [CZT-Devel] CZT Tool Install and execute from c++

[Leo F. <leo...@ne...>]

Hi Petra,

About the failure, from the numbers below I see it happened on ProofScriptParsingTest
could you send me the name of the file on which it failed please?

It's interesting the other user's failure was on typechecker and not the parser. Hum...
 
---

About the debug log, yes, it's large.... They were added to enable easy pinpointing of tricky 
lexing errors when handling certain ZEves productions that are not quite within ISOz, and 
the fact we wanted all formats at the same level of stability, given there were various issues
with extension for Unicode and XML printers (see SVN logs).

The ZEves CZT parser is now stable, I will disable the debug flags. Thanks for pointing it out.
The output is now quite silent:

Running net.sourceforge.czt.parser.zeves.ScanningTest
Tests run: 37, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 4.862 sec
Running net.sourceforge.czt.parser.zeves.OnTheFlyParsingTest
Tests run: 1, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
Running net.sourceforge.czt.print.zeves.ZmlPrintTest
Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.003 sec
Running net.sourceforge.czt.parser.zeves.ProofScriptParsingTest
Number of tests for Z/Eves proofs parsing: 41
Tests run: 41, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 9.121 sec

Results :
Tests run: 79, Failures: 0, Errors: 0, Skipped: 0

---

Best,
Leo


On 10 Oct 2011, at 12:02, Petra Dietrich wrote:

> Hi there,
> 
> I get the same error:
> [INFO] CZT Z/Eves (proofs) Parser ........................ FAILURE
> 
> due to a test failing:
> Tests run: 41, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 29.787
> sec <<< FAILURE!
> Running net.sourceforge.czt.print.zeves.ZmlPrintTest
> Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec
> 
> Results :
> 
> Failed tests:
>  null(net.sourceforge.czt.parser.util.CztManagedTest$TestNormal)
> Tests run: 79, Failures: 1, Errors: 0, Skipped: 0
> 
> BTW, it is hard to find useful output due to the huge amount of debug
> output like:
> =================================================================
> Direct UNICODE printing of
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8
> 
> ============================ TOSTRING ============================
>  toString successful for zeveslabels
> 
> ==================================================================
> SM UNICODE printing of
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8
> 
> ============================ LATEX    ============================
>  created file
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.tex
> 
> ============================ XML      ============================
>  created file
> /home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.zml
> ==================================================================
> 
> Is there a way to switch that off?
> 
> Cheers,
> Petra
> 
> On 10/10/11 23:20, Leo Freitas wrote:
>> Hi Urmas,
>> 
>> I am sorry to hear about this. When committing, I always run CZT clean/install to ensure this doesn't happen.
>> I just rebuilt it here successfully, and double-checked all is in place (e.g., no missing commits). Could you send
>> us the maven detailed info? I think if you run  "mvn -e clean install" it gives that.
>> 
>> If you reached that far, there might be something wrong on our end. I will double check (e.g., on a fresh machine).
>> By the way, I asked a colleague to download / install in a machine without CZT and it went through successfully.
>> Could you please try again and let me know if you still get the problem?
>> 
>> ----
>> 
>> About your specification animation, could you explain it a little bit further, please? I mean, there is the ZLive animator,
>> which would enable you to "execute" Z specifications that are concrete enough (and with contained enough types).
>> 
>> How is that to be linked with C++? I mean, what' s the role of the Z specification for you? Is it to define the C++ code
>> functional correctness? Or is for the C memory model / run-time exceptions? What is it you are trying to achieve?
>> 
>> Best,
>> Leo
>> 
>> On  10 Oct 2011, at 10:41, Urmas Repinski wrote:
>> 
>> Hello,
>> 
>> I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++.
>> 
>> First of all i want to install CZT on my PC.
>> 
>> I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached
>> 
>> [INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s]
>> [INFO] CZT Z VCG ......................................... SKIPPED
>> [INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED
>> [INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED
>> [INFO] CZT Z/Eves Integration ............................ SKIPPED
>> ....
>> 
>> 
>> So maybe i have to use any other mirror to download archives that are required during installation?
>> I had tried all mirrors that are in MAVEN website -
>> 
>> http://maven.apache.org/guides/mini/guide-mirror-settings.html
>> 
>> But this does not solve the problem, the installation does not finish.
>> 
>> And one more problem, can i after the installation animate simple Z specifications from c++ code?
>> 
>> If yes then please somebody replay me how can i do that?
>> 
>> Thank you very much,
>> Urmas Repinski.
>> <ATT00001..txt><ATT00002..txt>
>> 
>> 
>> ------------------------------------------------------------------------------
>> All the data continuously generated in your IT infrastructure contains a
>> definitive record of customers, application performance, security
>> threats, fraudulent activity and more. Splunk takes this data and makes
>> sense of it. Business sense. IT sense. Common sense.
>> http://p.sf.net/sfu/splunk-d2dcopy1
>> _______________________________________________
>> CZT-Devel mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-devel
> 
> 
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure contains a
> definitive record of customers, application performance, security
> threats, fraudulent activity and more. Splunk takes this data and makes
> sense of it. Business sense. IT sense. Common sense.
> http://p.sf.net/sfu/splunk-d2dcopy1
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] CZT Tool Install and execute from c++

[Petra D. <Pet...@ec...>]

Hi there,

I get the same error:
[INFO] CZT Z/Eves (proofs) Parser ........................ FAILURE

due to a test failing:
Tests run: 41, Failures: 1, Errors: 0, Skipped: 0, Time elapsed: 29.787
sec <<< FAILURE!
Running net.sourceforge.czt.print.zeves.ZmlPrintTest
Tests run: 0, Failures: 0, Errors: 0, Skipped: 0, Time elapsed: 0.002 sec

Results :

Failed tests:
  null(net.sourceforge.czt.parser.util.CztManagedTest$TestNormal)
Tests run: 79, Failures: 1, Errors: 0, Skipped: 0

BTW, it is hard to find useful output due to the huge amount of debug
output like:
=================================================================
Direct UNICODE printing of
/home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8

============================ TOSTRING ============================
  toString successful for zeveslabels

==================================================================
SM UNICODE printing of
/home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8

============================ LATEX    ============================
  created file
/home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.tex

============================ XML      ============================
  created file
/home/petra/czt/parser-zeves/target/test-classes/tests/zeves/zeveslabels.zed8.zml
==================================================================

Is there a way to switch that off?

Cheers,
Petra

On 10/10/11 23:20, Leo Freitas wrote:
> Hi Urmas,
> 
> I am sorry to hear about this. When committing, I always run CZT clean/install to ensure this doesn't happen.
> I just rebuilt it here successfully, and double-checked all is in place (e.g., no missing commits). Could you send
> us the maven detailed info? I think if you run  "mvn -e clean install" it gives that.
> 
> If you reached that far, there might be something wrong on our end. I will double check (e.g., on a fresh machine).
> By the way, I asked a colleague to download / install in a machine without CZT and it went through successfully.
> Could you please try again and let me know if you still get the problem?
> 
> ----
> 
> About your specification animation, could you explain it a little bit further, please? I mean, there is the ZLive animator,
> which would enable you to "execute" Z specifications that are concrete enough (and with contained enough types).
> 
> How is that to be linked with C++? I mean, what' s the role of the Z specification for you? Is it to define the C++ code
> functional correctness? Or is for the C memory model / run-time exceptions? What is it you are trying to achieve?
> 
> Best,
> Leo
> 
> On  10 Oct 2011, at 10:41, Urmas Repinski wrote:
> 
> Hello,
> 
> I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++.
> 
> First of all i want to install CZT on my PC.
> 
> I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached
> 
> [INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s]
> [INFO] CZT Z VCG ......................................... SKIPPED
> [INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED
> [INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED
> [INFO] CZT Z/Eves Integration ............................ SKIPPED
> ....
> 
> 
> So maybe i have to use any other mirror to download archives that are required during installation?
> I had tried all mirrors that are in MAVEN website -
> 
> http://maven.apache.org/guides/mini/guide-mirror-settings.html
> 
> But this does not solve the problem, the installation does not finish.
> 
> And one more problem, can i after the installation animate simple Z specifications from c++ code?
> 
> If yes then please somebody replay me how can i do that?
> 
> Thank you very much,
> Urmas Repinski.
> <ATT00001..txt><ATT00002..txt>
> 
> 
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure contains a
> definitive record of customers, application performance, security
> threats, fraudulent activity and more. Splunk takes this data and makes
> sense of it. Business sense. IT sense. Common sense.
> http://p.sf.net/sfu/splunk-d2dcopy1
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] CZT Tool Install and execute from c++

[Leo F. <leo...@ne...>]

Hi Urmas,

I am sorry to hear about this. When committing, I always run CZT clean/install to ensure this doesn't happen.
I just rebuilt it here successfully, and double-checked all is in place (e.g., no missing commits). Could you send
us the maven detailed info? I think if you run  "mvn -e clean install" it gives that.

If you reached that far, there might be something wrong on our end. I will double check (e.g., on a fresh machine).
By the way, I asked a colleague to download / install in a machine without CZT and it went through successfully.
Could you please try again and let me know if you still get the problem?

----

About your specification animation, could you explain it a little bit further, please? I mean, there is the ZLive animator,
which would enable you to "execute" Z specifications that are concrete enough (and with contained enough types).

How is that to be linked with C++? I mean, what' s the role of the Z specification for you? Is it to define the C++ code
functional correctness? Or is for the C memory model / run-time exceptions? What is it you are trying to achieve?

Best,
Leo

On  10 Oct 2011, at 10:41, Urmas Repinski wrote:

Hello,

I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++.

First of all i want to install CZT on my PC.

I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached

[INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s]
[INFO] CZT Z VCG ......................................... SKIPPED
[INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED
[INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED
[INFO] CZT Z/Eves Integration ............................ SKIPPED
....


So maybe i have to use any other mirror to download archives that are required during installation?
I had tried all mirrors that are in MAVEN website -

http://maven.apache.org/guides/mini/guide-mirror-settings.html

But this does not solve the problem, the installation does not finish.

And one more problem, can i after the installation animate simple Z specifications from c++ code?

If yes then please somebody replay me how can i do that?

Thank you very much,
Urmas Repinski.
<ATT00001..txt><ATT00002..txt>

[CZT-Devel] CZT Tool Install and execute from c++

[Urmas R. <ur...@ho...>]

Hello,



I would like to use CZT Tools for my work, the tool is useful i want to animate Z specifications using in c++.



First of all i want to install CZT on my PC.



I had downloadad version from SVN, installed MAVEN, executed mvn clean install, but the install process fails then it is reached



[INFO] CZT Z/Eves (proofs) Typechecker ................... FAILURE [0.334s]

[INFO] CZT Z VCG ......................................... SKIPPED

[INFO] CZT ZSideKick jEdit Plugin ........................ SKIPPED

[INFO] CZT Z Palette jEdit Plugin ........................ SKIPPED

[INFO] CZT Z/Eves Integration ............................ SKIPPED

....





So maybe i have to use any other mirror to download archives that are required during installation?

I had tried all mirrors that are in MAVEN website - 



http://maven.apache.org/guides/mini/guide-mirror-settings.html



But this does not solve the problem, the installation does not finish.



And one more problem, can i after the installation animate simple Z specifications from c++ code?



If yes then please somebody replay me how can i do that?



Thank you very much,

Urmas Repinski. 		 	   		  

Re: [CZT-Devel] explicit generics again

[Tim M. <tm...@un...>]

Hi Leo,

That is definitely a violation of the standard, which allows only 
refnames. However, the parser is written as follows:

         inner_term:it LSQUARE expressionList:el RSQUARE:rsquare
         {:
            RESULT = factory_.createRefExpr(name(it), el, Boolean.FALSE, 
Boolean.TRUE);
            addLocAnn(RESULT, getLocation(it, rsquare));
         :}

This means that the grammar will allow the following:

    (A \cup B)[C] = A \cup B

The CZT parser will report an error that a refname is expected for the 
generic instantiation when it calls name(it), and tries to cast the 
expression to a name. However, if this is for one of the dialects, you 
can easily add a new type of term to that dialect's schema, and then 
change the code body to create one of these terms.

Tim

On 22/09/11 18:39, Leo Freitas wrote:
> Hi Tim,
>
> I am confused about the role of the "explicit" parameter in RefExpr. My understanding is that it is true when the user suplies the generics, and false otherwise.
> That is because after type checking the ZExprList will contain (possibly non-maximal) generics which the user don't want explicitly given on the terms.
>
> Is that right? Assuming it is, what about proofs / conjectures involving non-maximal generics?  Ex:
>
> \begin{theorem}{lNonMaxCup}[X]
>       \vdash? \forall C: \power~X @ \forall A, B: \power~C @ (\_ \cup \_)[C] (A,B) =A \cup B
> \end{theorem}
>
> \begin{theorem}{catGen}[X]
>       \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ (\_\cat\_)[A] (s, t) = s \cat t
> \end{theorem}
>
> In ZEves, these theorems could be written as
>
> \begin{theorem}{lNonMaxCup}[X]
>       \vdash? \forall C: \power~X @ \forall A, B: \power~C @ A \cup[C] B = A \cup B
> \end{theorem}
>
> \begin{theorem}{catGen}[X]
>       \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ s \cat[A] t = s \cat t
> \end{theorem}
>
> When the expressions are large, it's rather ugly to need to write the whole thing with mixfix false :-(....
>
> So the question is, is there a way to have explicit generics mixfix=true appl expr or ref expr?
> That is crucial, otherwise, translating legacy proofs or indeed doing new proofs (e.g., ZEves
> throws back at you nonmaximal or maximal generics in places)..... :-( .... any ideas?
>
> Best,
> Leo

[CZT-Devel] explicit generics again

[Leo F. <leo...@ne...>]

Hi Tim,

I am confused about the role of the "explicit" parameter in RefExpr. My understanding is that it is true when the user suplies the generics, and false otherwise.
That is because after type checking the ZExprList will contain (possibly non-maximal) generics which the user don't want explicitly given on the terms.

Is that right? Assuming it is, what about proofs / conjectures involving non-maximal generics?  Ex:

\begin{theorem}{lNonMaxCup}[X]
     \vdash? \forall C: \power~X @ \forall A, B: \power~C @ (\_ \cup \_)[C] (A,B) =A \cup B
\end{theorem}

\begin{theorem}{catGen}[X]
     \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ (\_\cat\_)[A] (s, t) = s \cat t
\end{theorem}

In ZEves, these theorems could be written as

\begin{theorem}{lNonMaxCup}[X]
     \vdash? \forall C: \power~X @ \forall A, B: \power~C @ A \cup[C] B = A \cup B
\end{theorem}

\begin{theorem}{catGen}[X]
     \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ s \cat[A] t = s \cat t
\end{theorem}

When the expressions are large, it's rather ugly to need to write the whole thing with mixfix false :-(....

So the question is, is there a way to have explicit generics mixfix=true appl expr or ref expr?
That is crucial, otherwise, translating legacy proofs or indeed doing new proofs (e.g., ZEves
throws back at you nonmaximal or maximal generics in places)..... :-( .... any ideas?

Best,
Leo

Re: [CZT-Devel] posfix ApplExpr puzzlement

[Leo F. <leo...@ne...>]

Hi Tim,

Thank you for this. At first, I didn't expect it to be a type error: it passed through both CZT, ZEves, and fuzz.
And working out the types as you did is sensible, yes. I think my confusion came because of the (abstracted)
example that I tried to create:

\begin{gendef}[X,Y]
   w : Y \fun X
\end{gendef}

\begin{theorem}{postfixGen3}[X,Y]
    \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y]
\end{theorem}

This one works. But this one doesn't

\begin{theorem}{postfixGen2}[X,Y]
    \vdash? \forall z: X \fun Y; w: Y \fun X @ z = w (\_~\inv)[X,Y]
\end{theorem}

And the reason I guess is because Y is fixed in the second for what
in the first case it varies (e.g., first Y generic is not the same as second).

Z is a lovely language for describing abstract thinking concisely. 
My goodness it's complicated to build tools for!

Thanks,
Leo

On 22 Sep 2011, at 02:48, Tim Miller wrote:

> On 21/09/11 19:05, Leo Freitas wrote:
>> c) PUZZLE
>> 
>> \begin{gendef}[X,Y]
>>    w : Y \fun X
>> \end{gendef}
>> 
>> \begin{theorem}{postfixGen3}[X,Y]
>>     \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y]
>> \end{theorem}
>> 
>> ApplExpr(LHS="w", RHS="_\inv[X,Y]", MF=false)
>> 
>> (e.g., mistakenly we forgot to put \inv on the LHS, yet no error is raised!)
>> 
>> Shouldn't we have an error here either when applying w to inv or when comparing it to z?
>> 
> Do you mean a type error? I don't think so. If we consider the types, we 
> have (substituting in unique generic parameters to avoid confusion):
> 
>  \_ \inv: P (P(A x B) x P(B x A))   % (A x B) \fun (B x A)
>  w : P(C x D)
>  z : P(E x F)
> 
> The expression w (\_~\inv)[E,F] is a function application. The type of 
> (\_ \inv)[E,F] is P (P(E x F) x P(F x E))) from the explicit 
> instantiation.  Therefore, the type of the refexpr "w" is inferred as 
> P(P(E x F) x P(F x E) x Var), where C is instantiated by P(P(E x F) x 
> P(F x E)) and D is not instantiated (yet), so is given a variable type 
> Var. The equality z = w(\_\inv)[E,F] allows us to infer that Var = F, so 
> the type of w is fully instantiated.
> 
> Confused? :)
> 
> Tim
> 
> ------------------------------------------------------------------------------
> All the data continuously generated in your IT infrastructure contains a
> definitive record of customers, application performance, security
> threats, fraudulent activity and more. Splunk takes this data and makes
> sense of it. Business sense. IT sense. Common sense.
> http://p.sf.net/sfu/splunk-d2dcopy1
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] posfix ApplExpr puzzlement

[Tim M. <tm...@un...>]

On 21/09/11 19:05, Leo Freitas wrote:
> c) PUZZLE
>
> \begin{gendef}[X,Y]
>     w : Y \fun X
> \end{gendef}
>
> \begin{theorem}{postfixGen3}[X,Y]
>      \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y]
> \end{theorem}
>
> ApplExpr(LHS="w", RHS="_\inv[X,Y]", MF=false)
>
> (e.g., mistakenly we forgot to put \inv on the LHS, yet no error is raised!)
>
> Shouldn't we have an error here either when applying w to inv or when comparing it to z?
>
Do you mean a type error? I don't think so. If we consider the types, we 
have (substituting in unique generic parameters to avoid confusion):

  \_ \inv: P (P(A x B) x P(B x A))   % (A x B) \fun (B x A)
  w : P(C x D)
  z : P(E x F)

The expression w (\_~\inv)[E,F] is a function application. The type of 
(\_ \inv)[E,F] is P (P(E x F) x P(F x E))) from the explicit 
instantiation.  Therefore, the type of the refexpr "w" is inferred as 
P(P(E x F) x P(F x E) x Var), where C is instantiated by P(P(E x F) x 
P(F x E)) and D is not instantiated (yet), so is given a variable type 
Var. The equality z = w(\_\inv)[E,F] allows us to infer that Var = F, so 
the type of w is fully instantiated.

Confused? :)

Tim

[CZT-Devel] posfix ApplExpr puzzlement

[Leo F. <leo...@ne...>]

Hi,

I got puzzled by postfix ApplExpr types. The Std says (after syntactic transformations) there are two cases: mixfix and !mixfix.

a) mixfix true: okay, as expected

\begin{theorem}{postfixGen}[X,Y]
   \vdash? \forall q : X \fun Y; f : Y \fun X @ q = f\inv
\end{theorem}

Here, in (f\inv) we have an ApplExpr(LHS="_ \inv", RHS="f", MF=true)

(e.g., syntactic transformation puts \inv in the LHS of ApplExpr)

b) mixfix false: okay, as expected

\begin{theorem}{postfixGen2}[X,Y]
    \vdash? \forall g: X \fun Y; h: Y \fun X @ h = (\_~\inv)[X,Y] g
\end{theorem}

ApplExpr(LHS="_ \inv[X,Y]", RHS="g", MF=true)

(e.g., one MUST explicitly put the postfix on the LHS)

c) PUZZLE

\begin{gendef}[X,Y]
   w : Y \fun X
\end{gendef}

\begin{theorem}{postfixGen3}[X,Y]
    \vdash? \forall z: X \fun Y @ z = w (\_~\inv)[X,Y]
\end{theorem}

ApplExpr(LHS="w", RHS="_\inv[X,Y]", MF=false)

(e.g., mistakenly we forgot to put \inv on the LHS, yet no error is raised!)

Shouldn't we have an error here either when applying w to inv or when comparing it to z?

======== context 

This came across as a result of translating posfix expressions to CZT ZEvesEclipse , which handles generics slightly different:

CZT    : (_ NAME _)[X,Y] 
ZEves: (_ NAME[X,Y] _)

That means when we have ZEves terms like

A \cup[X] B

we get in trouble and need it to be something like

(\_ \cup \_)[X] (A,B)

which both CZT and ZEves are happy with. Now, when handling postifix I got

f \inv[X,Y]

then at some point mistakenly translated it to

f (\_ \inv)[X,Y]

instead of

(\_ \inv)[X,Y] f

hence the test case (c) above appeared and the puzzle...

======

Could somebody shed any light, pls? 

Best,
Leo

Re: [CZT-Devel] (implicit) operator templates in (Delta) schemas - ???

[Tim M. <tm...@un...>]

Hi Leo,

You wrote:
> \begin{schema}{Op}
>     \Delta~S
> \where
>      (\_ R \_)' = .....
> \end{schema}
>
> the dashed name is clearly undeclared. Yet, in ZEves, the "dashed" name gets declared
> as an Operator. What the standard says about such "implicit" op temp declarations?
>
There dashed name is declared, but it must be referenced as (\_~ {R}' 
\_). The following example parses and typechecks using CZT:

%%Zinword \R R

\begin{zed}
  \relation (\_ \R \_)
\end{zed}

\begin{schema}{S}
      \_ \R \_ : \nat \rel \nat
\end{schema}

\begin{axdef}
    S~'
\where
     (\_~ {\R}' \_) = \{(1,1)\}
\end{axdef}

\begin{axdef}
\where
   1~ {\R}' 1
\end{axdef}

So here, the name {\R}' is not implicitly declared as a operator, but it 
can be used as one because \R is declared as an operator.

According to the standard, the expression (\_ R \_)' should parse as 
schema decoration, so is not accepted by the CZT typechecker.

Cheers,
Tim

[CZT-Devel] (implicit) operator templates in (Delta) schemas - ???

[Leo F. <leo...@ne...>]

Hi,

I've seen in a spec a relation as an infix operator like 

x R y		(e.g.,  \relation..... )

rather than (x,y) \in R. This relation happen to appear as a variable within a schema (odd?)

\begin{schema}{S}
     \_ R \_ : \nat \rel \nat
\end{schema}

Now, when I have 

\begin{schema}{Op}
   \Delta~S
\where
    (\_ R \_)' = .....
\end{schema}

the dashed name is clearly undeclared. Yet, in ZEves, the "dashed" name gets declared
as an Operator. What the standard says about such "implicit" op temp declarations?

Any comments on that? I haven't come across this before and I am not sure
what's the right answer ....

Best,
Leo

[CZT-Devel] Z Std extension - schema tagging

[Leo F. <leo...@ne...>]

Hi,

I am integrating the Z VCG into the CZT Eclipse plugin. Whilst doing that for refinement (and compact version of precondition) proofs,
I came across the need to know what schema is to be considered as the "State" (+ retrieve, init, concrete, etc). 
In other tools, this can be made explicit by the user, yet each time the tool is run. I was thinking about some persistent version using
specific keywords/tags near SchBox AxPara (e.g., "\begin{schema}{S}"). What do you think? 

I've implemented this already within the ZEves Z parser and thought to put it into the Z one (haven't committed either).
The "keywords" are treated by the scanner/parser outside of boxes. An example would be something like

======================================================
\begin{zsection}
   \SECTION zstate\_toolkit \parents standard\_toolkit
\end{zsection}

Synonymns for when only (abstract/concrete) state is present?
%%Zword \zstate zstate
%%Zword \zstinit zstinit

%%Zword \zastate zastate
%%Zword \zastinit zastinit
%%Zword \zcstate zcstate
%%Zword \zcstinit zcstinit
%%Zword \zretrieve zretrieve
======================================================
\begin{zsection}
   \SECTION zstatev1 \parents zstate\_toolkit
\end{zsection}

\zstate
\begin{schema}{S}
   x: \nat
\where
   bar > x
\end{schema}

\zstinit
\begin{schema}{SInit}
   S~'
\where
   x' = 0
\end{schema}

======================================================
\begin{zsection}
   \SECTION zstatev2 \parents zstate\_toolkit
\end{zsection}

\zastate
\begin{schema}{AState}
   x: \power \nat
\where
  x \neq \emptyset
\end{schema}

\zastinit
\begin{schema}{ASInit}
   AState~'
\where
   x' = \{ 0 \}
\end{schema}

\zcstate
\begin{schema}{CState}
  y: \seq \nat
\where
   y \neq \langle \rangle
\end{schema}

\zcstinit
\begin{schema}{CStInit}
   CState~'
\where
  y' = \langle 0 \rangle
\end{schema}

\zretrieve
\begin{schema}{Retr}
   AState \\
   CState
\where
   \ran~y = x
\end{schema}

======================================================

If there are no objections, I will keep it to the Z parser. Only if you import zstate_toolkit as a parent
would it "work". So, like fuzz_toolkit and named theorems, I see this as a CZT Z extension.... 

I've extended the printer and typechecker as well to cope with the new markup and to ensure 
there are no duplication (e.g., duplicated state tags).

Comments  / thoughts?

Best,
Leo

[CZT-Devel] CZT Eclipse update

[Leo F. <leo...@ne...>]

Hi guys,

I've been working on the Z/Eves proofs parsing for a few weeks with a colleague here in Newcastle.
He is an Eclipse wizard, and not only embedded Z/Eves into Eclipse, but also suggested nice improvements
to the CZT Eclipse plugin as well (e.g., log info, errors displayed in more user-friendly way, etc).

All this should be under SVN now. If you are an Eclipse user, pls have a look and send us any feedback :-)

Best,
Leo

Re: [CZT-Devel] generics/erasure "error(?)" in TypeEnv / SectTypeEnv...

[Tim M. <tm...@un...>]

No, I'm not getting this warning. I'm using javac on the command line.

There is a type issue with the way I have declared those two. I'd not 
noticed it before. You should be able to just rename getX in the 
abstract class without issue because that method will never get bound at 
runtime except in the call to super.getX in the subclasses. Actually, a 
nicer solution would be to rename the subclass methods to getNameTypPair 
and getNameTypeSectTriple. The name "getX" is not very informative.

Cheers,
Tim

Leo Freitas wrote:
> Hi Tim,
> 
> Although nothing has changed in the TypeEnv/SectTypeEnv for getX, Java is now telling about an error in the IDE saying
> 
> "
> name clash: method "protected NameTypePair getX(ZName zName, Map<ZName, NameTypePair> map)" in TypeEnv 
> and "protected <X> X getX(ZName zName, Map<ZName, X> map)" in AbstractTypeEnv have the same erasure yet
> neither overrides the other. The same happens for getX in SectTypeEnv.
> "
> 
> yet, it does compile and pass the test run...  It seems like the "<X> in abstractTypeEnv is not getting bound to either
> NameTypePair or NameTypeSectTriple. Perhaps, what's needed is to have a type parameter <X> on AbstractTypeEnv
> (E.g., that's a common solution to this error I just googled for).... 
> 
> Does this happens with you?
> 
> Best,
> Leo
> ------------------------------------------------------------------------------
> All of the data generated in your IT infrastructure is seriously valuable.
> Why? It contains a definitive record of application performance, security 
> threats, fraudulent activity, and more. Splunk takes this data and makes 
> sense of it. IT sense. And common sense.
> http://p.sf.net/sfu/splunk-d2d-c2
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

[CZT-Devel] generics/erasure "error(?)" in TypeEnv / SectTypeEnv...

[Leo F. <leo...@ne...>]

Hi Tim,

Although nothing has changed in the TypeEnv/SectTypeEnv for getX, Java is now telling about an error in the IDE saying

"
name clash: method "protected NameTypePair getX(ZName zName, Map<ZName, NameTypePair> map)" in TypeEnv 
and "protected <X> X getX(ZName zName, Map<ZName, X> map)" in AbstractTypeEnv have the same erasure yet
neither overrides the other. The same happens for getX in SectTypeEnv.
"

yet, it does compile and pass the test run...  It seems like the "<X> in abstractTypeEnv is not getting bound to either
NameTypePair or NameTypeSectTriple. Perhaps, what's needed is to have a type parameter <X> on AbstractTypeEnv
(E.g., that's a common solution to this error I just googled for).... 

Does this happens with you?

Best,
Leo

Re: [CZT-Devel] theorem environment - comments pls?

[Leo F. <leo...@ne...>]

Hi Tim

Thanks for this. It's quite helpful... and the example is a good one in showing how Z concrete syntax can be challenging.

I now understand something that Z/Eves does about various paragraphs on unboxed envs... To have more than one
para, you *must* use "\also" to separate then rather than "\\". Probably, that's why.
I will look into this, and come back to you.

Many thanks,
Leo

On 27 Jun 2011, at 12:14, Tim Miller wrote:

> Anthony Hall wrote:
>> In view of this, though, I suppose it wouldn't be much of an imposition to insist that for conjecture paragraphs you must follow the standard and have them in a paragraph on their own. In which case I imagine it would be perfectly easy to translate
>> \begin{theorem}{name}
>> into
>> ZED name
>> since the next thing must be either [ opening the generic parameters or the vdash?
>> 
> Ah! Actually, I think this was the reason that the theorem environment 
> was introduced. There is a problem with newlines in predicates. Take the 
> following example:
> 
> \begin{zed}
>  \vdash? true\\
>  x == 1
> \end{zed}
> 
> At this point, the parser will treat the newline as a conjunction and 
> try to parse the next line as part of the predicate. To maintain 
> conformance with the Z standard, we couldn't restrict the parser grammar 
> to parse only predicates with no newlines after \vdash, and to maintain 
> backwards compatibility, it was decided to introduce theorem paragraphs 
> as a workaround.
> 
> Off the top of my head, I can't remember why the parser generator 
> doesn't detect this as a shift-reduce conflict, but I did figure it out 
> at the time.
> 
> Oddly, it seems that the parser generator was never modified to restrict 
> other cases; e.g. the following parses fine:
> 
> \begin{zed}
>  [X]\\
>  \vdash? true
> \end{zed}
> 
> Leo, when you are making the changes, I suggest that you restrict 
> conjectures to their own paragraphs so we can avoid this. It could cause 
> confusion for users when some paragraphs parse, but if you switch the 
> order around, they don't. You should be able to just treat conjectures 
> as their own rule. That is, remove it from "unboxedParagraphItem", and 
> add a new production to the "unboxedParagraphList" rule something like:
> 
>    unboxedParagraphList ::= ...
> 	ZED conjectureParagraph END
> 
> Cheers,
> Tim
> 
> ------------------------------------------------------------------------------
> All of the data generated in your IT infrastructure is seriously valuable.
> Why? It contains a definitive record of application performance, security 
> threats, fraudulent activity, and more. Splunk takes this data and makes 
> sense of it. IT sense. And common sense.
> http://p.sf.net/sfu/splunk-d2d-c2
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel

Re: [CZT-Devel] theorem environment - comments pls?

[Tim M. <tm...@un...>]

Anthony Hall wrote:
> In view of this, though, I suppose it wouldn't be much of an imposition to insist that for conjecture paragraphs you must follow the standard and have them in a paragraph on their own. In which case I imagine it would be perfectly easy to translate
> \begin{theorem}{name}
> into
> ZED name
> since the next thing must be either [ opening the generic parameters or the vdash?
>
Ah! Actually, I think this was the reason that the theorem environment 
was introduced. There is a problem with newlines in predicates. Take the 
following example:

\begin{zed}
  \vdash? true\\
  x == 1
\end{zed}

At this point, the parser will treat the newline as a conjunction and 
try to parse the next line as part of the predicate. To maintain 
conformance with the Z standard, we couldn't restrict the parser grammar 
to parse only predicates with no newlines after \vdash, and to maintain 
backwards compatibility, it was decided to introduce theorem paragraphs 
as a workaround.

Off the top of my head, I can't remember why the parser generator 
doesn't detect this as a shift-reduce conflict, but I did figure it out 
at the time.

Oddly, it seems that the parser generator was never modified to restrict 
other cases; e.g. the following parses fine:

\begin{zed}
  [X]\\
  \vdash? true
\end{zed}

Leo, when you are making the changes, I suggest that you restrict 
conjectures to their own paragraphs so we can avoid this. It could cause 
confusion for users when some paragraphs parse, but if you switch the 
order around, they don't. You should be able to just treat conjectures 
as their own rule. That is, remove it from "unboxedParagraphItem", and 
add a new production to the "unboxedParagraphList" rule something like:

    unboxedParagraphList ::= ...
	ZED conjectureParagraph END

Cheers,
Tim

Re: [CZT-Devel] theorem environment - comments pls?

[<rd...@le...>]

Anthony,

> Thanks for the explanation Tim
>
> (and thanks for that feature too - it would make life more difficult if it
> weren't there!)
>
>> The standard does not allow this, but yes, I designed the CZT parser to
>> support it. It will accept any valid Z specification as defined by the
>> standard, plus a few additions such as this for backward compatibility
>
> In view of this, though, I suppose it wouldn't be much of an imposition to
> insist that for conjecture paragraphs you must follow the standard and
> have them in a paragraph on their own. In which case I imagine it would be
> perfectly easy to translate
> \begin{theorem}{name}
> into
> ZED name
> since the next thing must be either [ opening the generic parameters or
> the vdash?
>
> That would work fine with the Z Word Tools: a theorem paragraph would be
> translated like that for CZT and ignored for fuzz. Rob, would that work
> for Proofpower?
>

I am not sure I understand the question. ProofPower-Z will accept a name
before the turnstile as the name of the theorem. It has the generic
parameters on the right of the turnstile, but I don't think that makes any
difference to you?

Regards,

Rob.


> Anthony
>
>> Leo wrote:
>> >> The issue with Theorem is the same, but slightly worse because
>> ConjPara may appear both within "unboxed para list" or as
>> >> "\begin{theorem}" environments (e.g., they both render as ZEDCHAR)...
>> Does this make sense? How to reconcile those?
>> >
>> I think this was the reason for the theorem environments right? To
>> remove this problem? The details are hazy for me though...
>>
>> Cheers,
>> Tim
>>
>
>

Re: [CZT-Devel] theorem environment - comments pls?

[Anthony H. <an...@an...>]

Thanks for the explanation Tim

(and thanks for that feature too - it would make life more difficult if it weren't there!)

> The standard does not allow this, but yes, I designed the CZT parser to 
> support it. It will accept any valid Z specification as defined by the 
> standard, plus a few additions such as this for backward compatibility

In view of this, though, I suppose it wouldn't be much of an imposition to insist that for conjecture paragraphs you must follow the standard and have them in a paragraph on their own. In which case I imagine it would be perfectly easy to translate 
\begin{theorem}{name} 
into
ZED name
since the next thing must be either [ opening the generic parameters or the vdash?

That would work fine with the Z Word Tools: a theorem paragraph would be translated like that for CZT and ignored for fuzz. Rob, would that work for Proofpower?

Anthony

> Leo wrote:
> >> The issue with Theorem is the same, but slightly worse because ConjPara may appear both within "unboxed para list" or as
> >> "\begin{theorem}" environments (e.g., they both render as ZEDCHAR)... Does this make sense? How to reconcile those?
> >
> I think this was the reason for the theorem environments right? To 
> remove this problem? The details are hazy for me though...
> 
> Cheers,
> Tim
>