Menu
▾
▴
czt-users — For end-users of the CZT tools
This list is closed, nobody may subscribe to it.
| 2003 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
(1) |
Nov
|
Dec
|
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| 2004 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
(2) |
| 2006 |
Jan
(3) |
Feb
(2) |
Mar
|
Apr
|
May
|
Jun
|
Jul
(1) |
Aug
(2) |
Sep
(1) |
Oct
|
Nov
(1) |
Dec
(3) |
| 2007 |
Jan
(8) |
Feb
(3) |
Mar
(1) |
Apr
|
May
|
Jun
|
Jul
(4) |
Aug
|
Sep
|
Oct
|
Nov
(11) |
Dec
|
| 2008 |
Jan
|
Feb
|
Mar
(4) |
Apr
(2) |
May
(2) |
Jun
|
Jul
(1) |
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2009 |
Jan
|
Feb
|
Mar
(4) |
Apr
|
May
(1) |
Jun
|
Jul
|
Aug
(2) |
Sep
|
Oct
|
Nov
|
Dec
|
| 2010 |
Jan
|
Feb
(7) |
Mar
(2) |
Apr
|
May
(4) |
Jun
(4) |
Jul
(2) |
Aug
|
Sep
(9) |
Oct
(2) |
Nov
(15) |
Dec
|
| 2011 |
Jan
(6) |
Feb
|
Mar
(1) |
Apr
(2) |
May
|
Jun
|
Jul
(3) |
Aug
(1) |
Sep
|
Oct
(1) |
Nov
|
Dec
|
| 2012 |
Jan
|
Feb
|
Mar
|
Apr
|
May
(3) |
Jun
(2) |
Jul
(5) |
Aug
(1) |
Sep
|
Oct
(1) |
Nov
|
Dec
|
| 2013 |
Jan
|
Feb
|
Mar
(1) |
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2014 |
Jan
|
Feb
|
Mar
|
Apr
(1) |
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2015 |
Jan
|
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
(1) |
Aug
(1) |
Sep
(2) |
Oct
(1) |
Nov
|
Dec
|
| 2016 |
Jan
(3) |
Feb
|
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2020 |
Jan
|
Feb
(2) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2022 |
Jan
|
Feb
(1) |
Mar
(1) |
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
| 2023 |
Jan
|
Feb
(1) |
Mar
|
Apr
|
May
|
Jun
|
Jul
|
Aug
|
Sep
|
Oct
|
Nov
|
Dec
|
|
From: Anthony H. <an...@an...> - 2010-11-03 14:17:04
|
Dear Petra I may have spoken too soon. Maven certainly reported success, but it didn't, as far as I can see, build an overall czt jar file. Should it have done? It did build a czt-1.6-SNAPSHOT-tests.jar, but not a czt-1.6-SNAPSHOT.jar which I expected. Am I doing something wrong here? Thanks again Anthony -----Original Message----- From: Anthony Hall [mailto:an...@an...] Sent: 03 November 2010 09:54 To: 'Petra Malik'; czt...@li... Subject: Re: [CZT-Users] Maven Problem Building from SVN Dear Petra Many thanks. This has indeed fixed the problem. (However, I did get an error at first, when I ran "mvn -Dmaven.test.skip=true clean install" because the Z Rules seemed to require the typechecker tests. When I built without skipping tests, it built OK and didn't actually take much longer, but perhaps there is something slightly wrong somewhere still?) Thanks for your help Anthony -----Original Message----- From: Petra Malik [mailto:Pet...@ec...] Sent: 03 November 2010 04:04 To: czt...@li... Subject: Re: [CZT-Users] Maven Problem Building from SVN Hi Anthony, I could reproduce this problem with the latest maven version (3.0). For some reason, maven now seems to require version numbers for plugins so I've added those (committed as revision 7275). Please do an "svn update", try again, and let us know if it there are still problems. Hope this helps, Petra PS: The very first "mvn clean" (before the czt maven plugins have been built) still seems to fail but "mvn clean install" works fine. I am not sure how to fix that. Maybe it's something to not worry too much about since once the plugins are in the mvn repository, "mvn clean" works fine. ---------------------------------------------------------------------------- -- Achieve Improved Network Security with IP and DNS Reputation. Defend against bad network traffic, including botnets, malware, phishing sites, and compromised hosts - saving your company time, money, and embarrassment. Learn More! http://p.sf.net/sfu/hpdev2dev-nov _______________________________________________ CZT-Users mailing list CZT...@li... https://lists.sourceforge.net/lists/listinfo/czt-users ---------------------------------------------------------------------------- -- Achieve Improved Network Security with IP and DNS Reputation. Defend against bad network traffic, including botnets, malware, phishing sites, and compromised hosts - saving your company time, money, and embarrassment. Learn More! http://p.sf.net/sfu/hpdev2dev-nov _______________________________________________ CZT-Users mailing list CZT...@li... https://lists.sourceforge.net/lists/listinfo/czt-users |
|
From: Anthony H. <an...@an...> - 2010-11-03 10:07:21
|
Dear Petra Many thanks. This has indeed fixed the problem. (However, I did get an error at first, when I ran "mvn -Dmaven.test.skip=true clean install" because the Z Rules seemed to require the typechecker tests. When I built without skipping tests, it built OK and didn't actually take much longer, but perhaps there is something slightly wrong somewhere still?) Thanks for your help Anthony -----Original Message----- From: Petra Malik [mailto:Pet...@ec...] Sent: 03 November 2010 04:04 To: czt...@li... Subject: Re: [CZT-Users] Maven Problem Building from SVN Hi Anthony, I could reproduce this problem with the latest maven version (3.0). For some reason, maven now seems to require version numbers for plugins so I've added those (committed as revision 7275). Please do an "svn update", try again, and let us know if it there are still problems. Hope this helps, Petra PS: The very first "mvn clean" (before the czt maven plugins have been built) still seems to fail but "mvn clean install" works fine. I am not sure how to fix that. Maybe it's something to not worry too much about since once the plugins are in the mvn repository, "mvn clean" works fine. ---------------------------------------------------------------------------- -- Achieve Improved Network Security with IP and DNS Reputation. Defend against bad network traffic, including botnets, malware, phishing sites, and compromised hosts - saving your company time, money, and embarrassment. Learn More! http://p.sf.net/sfu/hpdev2dev-nov _______________________________________________ CZT-Users mailing list CZT...@li... https://lists.sourceforge.net/lists/listinfo/czt-users |
|
From: Petra M. <Pet...@ec...> - 2010-11-03 04:48:22
|
Hi Paulo,
You wrote:
> [...] I was able to retrieve most of the predicate by
> doing some interpretation of how it is generated but for a few
> predicates there were some parts missing.
>
> For instance in the schema:
>
> \begin{schema}{Remind}
> \Xi BirthdayBook \\
> today?: DATE \\
> cards!: \power NAME
> \where
> cards! = \{ n: known | birthday(n) = today? \}
> \end{schema}
To see how this gets translated into an AST, it might help to look at
the corresponding XML. You can use the czt tools to translate a latex
file into XML, or have a look at
zml/src/main/resources/net/sourceforge/czt/zml/examples/z/birthdaybook.xml
(in your CZT directory).
Note that "cards! = \{ n: known | birthday(n) = today? \}" gets
transformed into "cards! \in \{\{ n: known | birthday(n) = today? \}\}",
which is equivalent. That's why the predicate part of the schema is a
membership (MemPred).
> I got the structure:
>
> net.sourceforge.czt.z.impl.MemPredImpl
> net.sourceforge.czt.z.base.impl.ListTermImpl
> net.sourceforge.czt.z.impl.RefExprImpl
> cards!
> net.sourceforge.czt.z.impl.SetExprImpl
> net.sourceforge.czt.z.impl.ZExprListImpl
> net.sourceforge.czt.z.impl.SetCompExprImpl
Here is the corresponding bit of the ZML that shows what's inside this
SetCompExpr:
<SetCompExpr>
<ZSchText>
<ZDeclList>
<VarDecl>
<ZNameList>
<ZName>
<Word>n</Word>
<ZStrokeList/>
</ZName>
</ZNameList>
<RefExpr Mixfix="false" Explicit="false">
<ZName>
<Word>known</Word>
<ZStrokeList/>
</ZName>
<ZExprList/>
</RefExpr>
...
So the SetCompExpr should have a method getSchText() which gives you the
ZSchText. ZSchText in turn should have a method getDeclList() etc.
> I have tried using some print methods from the package such as the
> net.sourceforge.czt.print.z.PrintUtils.printLatex(term, writer, manager)
> but I could only print the whole specification and wasn't able to print
> a predicate from a single schema.
Try providing the section manager that you've used for parsing the
specification as well as the section name the predicate is defined in.
The problem with printing just a predicate is that it might contain user
defined operators, and their operator definition needs to be looked up.
If you need more help with this, maybe provide your source code so we
can have a look at it. You should also tell us which CZT version you
are using.
Hope this helps,
Petra
|
|
From: Petra M. <Pet...@ec...> - 2010-11-03 04:04:29
|
Hi Anthony, I could reproduce this problem with the latest maven version (3.0). For some reason, maven now seems to require version numbers for plugins so I've added those (committed as revision 7275). Please do an "svn update", try again, and let us know if it there are still problems. Hope this helps, Petra PS: The very first "mvn clean" (before the czt maven plugins have been built) still seems to fail but "mvn clean install" works fine. I am not sure how to fix that. Maybe it's something to not worry too much about since once the plugins are in the mvn repository, "mvn clean" works fine. |
|
From: Petra M. <Pet...@ec...> - 2010-11-03 04:03:14
|
Hi Weiguang, You wrote: >> 1) I want to extract the AST structure from my Z specification using >> CZT, and then do some test generation work on the AST. You might want to have a look at Fastest, a test generation tool built on top of CZT. http://en.wikipedia.org/wiki/Fastest It is described in an ICFEM'09 paper by Maximiliano Cristiá and Pablo Rodríguez Monetti titled "Implementing and Applying the Stocks-Carrington Framework for Model-Based Testing". The CZT papers "CZT: A framework for Z tools" and "CZT support for Z extensions" should give you a basic idea how to extend CZT. Also, the API documentation for the AST in particular should be helpful. http://czt.sourceforge.net/corejava/apidocs/index.html is a (probably somewhat out-of-date) on-line version but you can use maven to generate an up-to-date version. This mailing list is the right place to ask any specific questions you've got. >> 2) I have checked out the CZT trunk (revision 7273) and tried to install it. >> >> After passing the “mvn clean” command, I'm getting a failure when run the “mvn install” command: Could you please do an "svn update" and try again? Let us know if there are still problems (including the exact error message and version numbers for Java and maven). Hope this helps, Petra |
|
From: Weiguang W. <bi...@gm...> - 2010-11-02 17:11:13
|
-------------------------------------------------------------------------------
Test set: net.sourceforge.czt.z.jaxb.JaxbXmlWriterReaderTest
-------------------------------------------------------------------------------
Tests run: 1, Failures: 0, Errors: 1, Skipped: 0, Time elapsed: 0.868 sec <<< FAILURE!
testWritingReading(net.sourceforge.czt.z.jaxb.JaxbXmlWriterReaderTest) Time elapsed: 0.864 sec <<< ERROR!
net.sourceforge.czt.base.util.UnmarshalException: javax.xml.bind.UnmarshalException
- with linked exception:
[org.xml.sax.SAXParseException: cvc-complex-type.2.4.d: Invalid content was found starting with element 'AndPred'. No child element '{"http://czt.sourceforge.net/zml":Pred}' is expected at this point.]
at net.sourceforge.czt.base.jaxb.JaxbXmlReader.read(JaxbXmlReader.java:97)
at net.sourceforge.czt.base.util.XmlWriterReaderTest.testWritingReading(XmlWriterReaderTest.java:71)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at junit.framework.TestCase.runTest(TestCase.java:168)
at junit.framework.TestCase.runBare(TestCase.java:134)
at junit.framework.TestResult$1.protect(TestResult.java:110)
at junit.framework.TestResult.runProtected(TestResult.java:128)
at junit.framework.TestResult.run(TestResult.java:113)
at junit.framework.TestCase.run(TestCase.java:124)
at junit.framework.TestSuite.runTest(TestSuite.java:232)
at junit.framework.TestSuite.run(TestSuite.java:227)
at junit.framework.TestSuite.runTest(TestSuite.java:232)
at junit.framework.TestSuite.run(TestSuite.java:227)
at org.junit.internal.runners.JUnit38ClassRunner.run(JUnit38ClassRunner.java:79)
at org.apache.maven.surefire.junit4.JUnit4TestSet.execute(JUnit4TestSet.java:59)
at org.apache.maven.surefire.suite.AbstractDirectoryTestSuite.executeTestSet(AbstractDirectoryTestSuite.java:115)
at org.apache.maven.surefire.suite.AbstractDirectoryTestSuite.execute(AbstractDirectoryTestSuite.java:102)
at org.apache.maven.surefire.Surefire.run(Surefire.java:180)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
at java.lang.reflect.Method.invoke(Method.java:597)
at org.apache.maven.surefire.booter.SurefireBooter.runSuitesInProcess(SurefireBooter.java:350)
at org.apache.maven.surefire.booter.SurefireBooter.main(SurefireBooter.java:1021)
Caused by: javax.xml.bind.UnmarshalException
- with linked exception:
[org.xml.sax.SAXParseException: cvc-complex-type.2.4.d: Invalid content was found starting with element 'AndPred'. No child element '{"http://czt.sourceforge.net/zml":Pred}' is expected at this point.]
at javax.xml.bind.helpers.AbstractUnmarshallerImpl.createUnmarshalException(AbstractUnmarshallerImpl.java:315)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.createUnmarshalException(UnmarshallerImpl.java:503)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.unmarshal0(UnmarshallerImpl.java:204)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.unmarshal(UnmarshallerImpl.java:173)
at javax.xml.bind.helpers.AbstractUnmarshallerImpl.unmarshal(AbstractUnmarshallerImpl.java:137)
at javax.xml.bind.helpers.AbstractUnmarshallerImpl.unmarshal(AbstractUnmarshallerImpl.java:184)
at net.sourceforge.czt.base.jaxb.JaxbXmlReader.read(JaxbXmlReader.java:94)
... 26 more
Caused by: org.xml.sax.SAXParseException: cvc-complex-type.2.4.d: Invalid content was found starting with element 'AndPred'. No child element '{"http://czt.sourceforge.net/zml":Pred}' is expected at this point.
at com.sun.org.apache.xerces.internal.util.ErrorHandlerWrapper.createSAXParseException(ErrorHandlerWrapper.java:195)
at com.sun.org.apache.xerces.internal.util.ErrorHandlerWrapper.error(ErrorHandlerWrapper.java:131)
at com.sun.org.apache.xerces.internal.impl.XMLErrorReporter.reportError(XMLErrorReporter.java:384)
at com.sun.org.apache.xerces.internal.impl.XMLErrorReporter.reportError(XMLErrorReporter.java:318)
at com.sun.org.apache.xerces.internal.impl.xs.XMLSchemaValidator$XSIErrorReporter.reportError(XMLSchemaValidator.java:417)
at com.sun.org.apache.xerces.internal.impl.xs.XMLSchemaValidator.reportSchemaError(XMLSchemaValidator.java:3182)
at com.sun.org.apache.xerces.internal.impl.xs.XMLSchemaValidator.elementLocallyValidComplexType(XMLSchemaValidator.java:3169)
at com.sun.org.apache.xerces.internal.impl.xs.XMLSchemaValidator.elementLocallyValidType(XMLSchemaValidator.java:3105)
at com.sun.org.apache.xerces.internal.impl.xs.XMLSchemaValidator.processElementContent(XMLSchemaValidator.java:3007)
at com.sun.org.apache.xerces.internal.impl.xs.XMLSchemaValidator.handleEndElement(XMLSchemaValidator.java:2150)
at com.sun.org.apache.xerces.internal.impl.xs.XMLSchemaValidator.endElement(XMLSchemaValidator.java:818)
at com.sun.org.apache.xerces.internal.jaxp.validation.ValidatorHandlerImpl.endElement(ValidatorHandlerImpl.java:563)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.ValidatingUnmarshaller.endElement(ValidatingUnmarshaller.java:83)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.SAXConnector.endElement(SAXConnector.java:145)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.endElement(AbstractSAXParser.java:601)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl.scanEndElement(XMLDocumentFragmentScannerImpl.java:1782)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl$FragmentContentDriver.next(XMLDocumentFragmentScannerImpl.java:2938)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentScannerImpl.next(XMLDocumentScannerImpl.java:648)
at com.sun.org.apache.xerces.internal.impl.XMLNSDocumentScannerImpl.next(XMLNSDocumentScannerImpl.java:140)
at com.sun.org.apache.xerces.internal.impl.XMLDocumentFragmentScannerImpl.scanDocument(XMLDocumentFragmentScannerImpl.java:511)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:808)
at com.sun.org.apache.xerces.internal.parsers.XML11Configuration.parse(XML11Configuration.java:737)
at com.sun.org.apache.xerces.internal.parsers.XMLParser.parse(XMLParser.java:119)
at com.sun.org.apache.xerces.internal.parsers.AbstractSAXParser.parse(AbstractSAXParser.java:1205)
at com.sun.org.apache.xerces.internal.jaxp.SAXParserImpl$JAXPSAXParser.parse(SAXParserImpl.java:522)
at com.sun.xml.internal.bind.v2.runtime.unmarshaller.UnmarshallerImpl.unmarshal0(UnmarshallerImpl.java:200)
... 30 more
|
|
From: Paulo K. <pau...@gm...> - 2010-10-24 03:47:08
|
Greetings,
I have been working on a university project that intends to generate source
code from a specification of software in Z notation.
My first goal was to simply print the predicate as it was in the
specification in LaTeX that I get with the method getPred() from a object of
the class net.sourceforge.czt.z.ast.ZSchText after a call to the method
visitTerm(net.sourceforge.czt.util.Visitor visitor,
net.sourceforge.czt.base.ast.Term term of the class
net.sourceforge.czt.base.visitor.VisitorUtils.
After that I have managed to attain some values that i could print from the
class net.sourceforge.czt.z.impl.RefExprImpl using a object Term as base,
containing a single schema, after analyzing the structure of the AST. Using
that object I was able to retrieve most of the predicate by doing some
interpretation of how it is generated but for a few predicates there were
some parts missing.
For instance in the schema:
\begin{schema}{Remind}
\Xi BirthdayBook \\
today?: DATE \\
cards!: \power NAME
\where
cards! = \{ n: known | birthday(n) = today? \}
\end{schema}
I got the structure:
net.sourceforge.czt.z.impl.MemPredImpl
net.sourceforge.czt.z.base.impl.ListTermImpl
net.sourceforge.czt.z.impl.RefExprImpl
cards!
net.sourceforge.czt.z.impl.SetExprImpl
net.sourceforge.czt.z.impl.ZExprListImpl
net.sourceforge.czt.z.impl.SetCompExprImpl
net.sourceforge.czt.z.impl.MemPredImpl
net.sourceforge.czt.base.impl.ListTermImpl
net.sourceforge.czt.z.impl.ApplExprImpl
net.sourceforge.czt.z.impl.RefExprImpl
birthday
net.sourceforge.czt.z.impl.RefExprImpl
n
net.sourceforge.czt.z.impl.SetExprImpl
net.sourceforge.czt.z.impl.ZExprListImpl
net.sourceforge.czt.z.impl.RefExprImpl
today?
true
true
I have used indentation to show the children of each as I have used
recursion to print that structure. As it shows I wasn't able to retrieve the
part "n: known |" of the predicate.
I have tried using some print methods from the package such as the
net.sourceforge.czt.print.z.PrintUtils.printLatex(term, writer, manager) but
I could only print the whole specification and wasn't able to print a
predicate from a single schema.
Any help is really appreciated.
Thanks in advance.
Regards, Paulo.
|
|
From: Ray R. <ray...@gm...> - 2010-09-22 15:25:16
|
The penny has dropped and I've sorted out the section / parents stuff.
All is working. Thanks.
On Wed, Sep 22, 2010 at 12:53 AM, Petra Malik <Pet...@ec...> wrote:
> Ray wrote:
>
>> I have 2 specifications, A.tex and B.tex. There is a sequence of 4-5
>> schemas that both documents share in common so I refactored them into
>> a common tex file C.tex. In the appropriate locations in A.tex and
>> B.tex I've inserted a \input{C} and "include" the common fragments.
>> However running java -jar czt.jar A.tex fails to type check as czt
>> does not appear to be processing the \input latex.
>
> CZT doesn't parse the latex outside Z paragraphs so doesn't know about
> the input command.
> What you can do is to declare named Z sections:
> In C.tex (at the beginning) you'd have something like:
> \begin{zsection}
> \SECTION C \parents standard\_toolkit
> \end{zsection}
>
> and then in A.tex and B.tex you can declare section C as a parent:
> \begin{zsection}
> \SECTION A \parents C
> \end{zsection}
>
> When Z section A is parsed, CZT tries to find parent section C by
> looking for a file C.tex (among other things). You might have to let
> CZT know in which directory to look for file C.tex (and how to do this
> depends on which interface you are using). So try whether just adding Z
> sections works. If it can't find the file, we will have to figure out
> how to set the CZT path for the interface you are using (command
> line/jEdit/Eclipse).
>
> Petra
>
> ------------------------------------------------------------------------------
> Start uncovering the many advantages of virtual appliances
> and start using them to simplify application deployment and
> accelerate your shift to cloud computing.
> http://p.sf.net/sfu/novell-sfdev2dev
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users
>
--
The object of life is not to be on the side of the majority, but to
escape finding oneself in the ranks of the insane. - Marcus Aurelius
|
|
From: Petra M. <Pet...@ec...> - 2010-09-22 04:53:48
|
Ray wrote:
> I have 2 specifications, A.tex and B.tex. There is a sequence of 4-5
> schemas that both documents share in common so I refactored them into
> a common tex file C.tex. In the appropriate locations in A.tex and
> B.tex I've inserted a \input{C} and "include" the common fragments.
> However running java -jar czt.jar A.tex fails to type check as czt
> does not appear to be processing the \input latex.
CZT doesn't parse the latex outside Z paragraphs so doesn't know about
the input command.
What you can do is to declare named Z sections:
In C.tex (at the beginning) you'd have something like:
\begin{zsection}
\SECTION C \parents standard\_toolkit
\end{zsection}
and then in A.tex and B.tex you can declare section C as a parent:
\begin{zsection}
\SECTION A \parents C
\end{zsection}
When Z section A is parsed, CZT tries to find parent section C by
looking for a file C.tex (among other things). You might have to let
CZT know in which directory to look for file C.tex (and how to do this
depends on which interface you are using). So try whether just adding Z
sections works. If it can't find the file, we will have to figure out
how to set the CZT path for the interface you are using (command
line/jEdit/Eclipse).
Petra
|
|
From: Ray R. <ray...@gm...> - 2010-09-21 20:14:35
|
Hello,
Thanks for CZT.
I have 2 specifications, A.tex and B.tex. There is a sequence of 4-5
schemas that both documents share in common so I refactored them into
a common tex file C.tex. In the appropriate locations in A.tex and
B.tex I've inserted a \input{C} and "include" the common fragments.
However running java -jar czt.jar A.tex fails to type check as czt
does not appear to be processing the \input latex.
In other words, it appears that czt is restricted to checking a single
monolithic tex file at this time. Or am I doing something wrong.
Thanks
Ray
--
The object of life is not to be on the side of the majority, but to
escape finding oneself in the ranks of the insane. - Marcus Aurelius
|
|
From: <pet...@ec...> - 2010-09-20 09:09:07
|
There is no definition of AIRPORT'. You want to refer to AIRPORT and then prime its components. In Standard Z you need a space between the name AIRPORT and the ' operator. Hope this helps, Petra ----- Reply message ----- From: "Philippe de Rochambeau" <ph...@fr...> Date: Mon, Sep 20, 2010 18:32 Subject: [CZT-Users] AIRPORT' To: <czt...@li...> Hello, after typing the following code (copied from "Formal Specification in Z" by D Lightfoot) in Eclipse, I got an error message stating that AIRPORT' is undeclared (in Init). Why is that? Many thanks. Philippe ─ section Airline parents standard_toolkit └ ─ [ PLANE ] └ ─ [ GATE ] └ ┌ AIRPORT waiting: ℙ PLANE assignment: GATE ↣ PLANE | waiting ∩ ran assignment = ∅ └ ┌ Init AIRPORT′ | waiting′ = ∅ empty′ = ∅ └ |
|
From: Philippe de R. <ph...@fr...> - 2010-09-20 06:32:42
|
Hello, after typing the following code (copied from "Formal Specification in Z" by D Lightfoot) in Eclipse, I got an error message stating that AIRPORT' is undeclared (in Init). Why is that? Many thanks. Philippe ─ section Airline parents standard_toolkit └ ─ [ PLANE ] └ ─ [ GATE ] └ ┌ AIRPORT waiting: ℙ PLANE assignment: GATE ↣ PLANE | waiting ∩ ran assignment = ∅ └ ┌ Init AIRPORT′ | waiting′ = ∅ empty′ = ∅ └ |
|
From: Petra M. <Pet...@ec...> - 2010-09-19 23:21:16
|
Hi phiroc, You wrote: > In the following section, I define the > 'speaks' relation twice, once in the CountryLanguage schema > and once in the LatinIsNotASpoken schema, because > I couldn't find a way to make it global in Eclipse CZT. Axiomatic definitions are used to define global relations like this. > I tried adding it after [LANGUAGE] basic type, but > to no avail, because CZT assumed that was a comment. I am not quite sure which mark-up you are using. If you are using Unicode, you need special box character to introduce the axiomatic paragraph: ╷ DECLS | PREDS └ > [COUNTRY] > [LANGUAGE] > ... add 'speaks' here? Yes, that's the right place to put it but I still don't know what mark-up you are using. > Furthermore, is there a special character in Z which lets > you create commments? You can write text/comments anywhere outside a Z paragraph but not within a Z paragraph. Petra |
|
From: Petra M. <Pet...@ec...> - 2010-09-19 23:14:47
|
Hi Philippe, You wrote: > is there anyone in this list? Yes. :) > Does the oz compiler in Eclipse work? It should work but might have bugs. I usually use the jEdit plugins or the command line interface so don't know how well it works. If you find a bug, please submit it at sourceforge. http://sourceforge.net/tracker/?group_id=86250 > When I click the + sign next to "Credit Card" class show below, to fold it, > Eclipse folds it right after "limit E {1000, 2000, ...}" which is > obviously not the > class's end. If your specification hasn't parsed properly, I don't expect the folding to work correctly. First make sure that you don't get any errors any more and then try the folding feature again. > Furthermore, Eclipse displays a " syntax error at ZPROJ" next to the > (limit, balance, etc.) visibility list. You don't seem to use the Object-Z syntax expected by CZT. You should have a keyword "class" before the name of your class, that is, change > ┌ CreditCard to ┌ class CreditCard > Visibility list > [...] > Constant schema These are comments, aren't they? I don't think you can have comments like this within an Object-Z class but I am not quite sure. If these are comments, try deleting them to see whether this makes a difference. Have a look at other examples, to learn about the exact syntax. I usually use latex so I am not really familiar with the Unicode mark-up but CZT provides facilities to translate between the mark-ups. Hope this helps, Petra |
|
From: Philippe de R. <ph...@fr...> - 2010-09-19 13:19:14
|
Hello,
is there anyone in this list?
Does the oz compiler in Eclipse work?
When I click the + sign next to "Credit Card" class show below, to fold it,
Eclipse folds it right after "limit E {1000, 2000, ...}" which is obviously not the
class's end.
Furthermore, Eclipse displays a " syntax error at ZPROJ" next to the (limit, balance, etc.) visibility list.
Any help would be much appreciated.
pr
┌ CreditCard
Visibility list
⨡ ( limit, balance, INIT, withdraw, deposit, withdrawAvail )
Constant schema
╷
limit: ℕ
|
limit ∈ { 1000, 2000, 5000 }
└
┌─
balance: ℤ
|
balance + limit >= 0
└
┌ Init
balance = 0
└
┌ widthDraw
Δ ( balance )
amount?: ℕ
|
amount? <= balance + limit
balance' = balance - amount?
└
┌ deposit
Δ ( balance )
amount?: ℕ
|
balance' = balance + amount?
└
┌ widthdrawAvail
Δ ( balance )
amount!: ℕ
|
amount! = balance + limit
balance' = - limit
└
└
|
|
From: <ph...@fr...> - 2010-09-08 10:01:21
|
Hello, In the following section, I define the 'speaks' relation twice, once in the CountryLanguage schema and once in the LatinIsNotASpoken schema, because I couldn't find a way to make it global in Eclipse CZT. I tried adding it after [LANGUAGE] basic type, but to no avail, because CZT assumed that was a comment. -------------- [COUNTRY] [LANGUAGE] ... add 'speaks' here? CountryLanguage speaks: P ( COUNTRY x LANGUAGE) spoken: P ( LANGUAGE x COUNTRY) LatinIsNotASpokenLanguage Latin: LANGUAGE speaks: P ( COUNTRY x LANGUAGE) ... ------------- Is there a way to make relationships global? Furthermore, is there a special character in Z which lets you create commments? Many thanks. pr |
|
From: Tim M. <tm...@un...> - 2010-07-11 22:54:47
|
Hi Pablo, I've had a quick look at this. It seems like a fault in the typechecker. I haven't got the time to look at it at the moment. Could you please submit a bug report at http://sourceforge.net/projects/czt/support? I'll take a closer look when I get the chance. Thanks, Tim Pablo Rodriguez Monetti wrote: > Hi czt'ers, > > I had a problem trying to load an specification with uses before > declarations. In general, this kind of models are supported. For > example, I could correctly load the following specification: > > \begin{zed} > Integers == Positives \lor Negatives \lor Zero > \end{zed} > > \begin{zed} > Positives == [a: \nat | a > 0] \\ > Negatives == [a: \nat | a < 0] \\ > Zero == [a: \nat | a = 0] \\ > \end{zed} > > However, the following one could not be loaded in the given order: > > \begin{gendef}[X] > optional:\power X \fun \power (\power X)\\ > \end{gendef} > > \begin{zed} > FFName == String \{2\}\\ > \end{zed} > > \begin{schema}{FF} > name: FFName\\ > \end{schema} > > \begin{schema}{NI} > hI: optional~HI\\ > \end{schema} > > \begin{schema}{HI} > hF:FF\\ > \end{schema} > > \begin{zed} > STRING == \seq \nat \\ > \end{zed} > > \begin{axdef} > String : \power(\nat) \fun \power(STRING) \\ > \end{axdef} > > reporting the following error: > > "ubf2.tex", line 13: Implicit parameters not determined > Expression: optional > > It's very sensitive to exactly what the declaration sequence is. For > example, if I change the declaration of FFName from String{2} to STRING, > it works fine. If I reorder the specification appropriately, it works > fine too. > > Cheers, > > Pablo > > > > > > On Tue, Jun 1, 2010 at 3:13 PM, Pablo Rodriguez Monetti > <rod...@gm... <mailto:rod...@gm...>> wrote: > > Hi Tim, > > You are right! The problem was that I was mistakenly expecting the > typecheck() method to throw an exception whenever there was an error > (like I did with manager.get() ) and forgot to check the return value :S > > However, a few weeks ago, I cloned and "manually" modify the AST > structure of an AxPara (conjugating its predicate to a given > predicate P, to typecheck P in the context of the variables declared > in the AxPara) and when I wanted to typecheck the resulting AxPara, > calling typecheck() with the AxPara object failed to find errors > while calling the method with the SchExpr associated to the AxPara > was successful (ie. it found errors, if any). That's why I believed > that the typecheck() method failed with some types of terms and was > ok with others. > > Many thanks! > > Pablo > > > > On Mon, May 31, 2010 at 8:19 PM, Tim Miller <tm...@un... > <mailto:tm...@un...>> wrote: > > Hi Pablo, > > Can you post the example that you are trying to typecheck? > > If I use the source code that you pasted into your email, > everything seems to work ok for me. I have the following example: > > \begin{zed} > x == y > \end{zed} > > \begin{zed} > y == 1 > \end{zed} > > \begin{axdef} > \where > x \in y > \end{axdef} > > in which 'y' is used before it is declared, and there is a type > mismatch in the axdef. If I compile and run the following code, > it reports the type mismatch, but not the use before declaration: > > import java.util.List; > > import net.sourceforge.czt.typecheck.z.*; > import net.sourceforge.czt.z.ast.*; > import net.sourceforge.czt.session.*; > > public class Test > { > > public static void main(String [] args) throws Exception > { > String fileName = "usebeforedecl.tex"; > > Source source = new FileSource(fileName); > SectionManager manager = new SectionManager(); > manager.put(new Key(fileName, Source.class), source); > Spec spec = (Spec) manager.get(new Key(fileName, Spec.class)); > List<? extends ErrorAnn> errors = > > TypeCheckUtils.typecheck(spec, manager, true); > > for (ErrorAnn error : errors) { > System.out.println(error); > } > } > } > > > If I set the use before declaration flag to false, it reports both. > > Can you try this and see what you get? > > Thanks, > > Tim > > Pablo Rodriguez Monetti wrote: > > Hi Tim, > > Many thanks for your answer! > > I have tried with the typecheck() method, passing as first > argument an Spec object: > > Source source = new FileSource(fileName); > SectionManager manager = new SectionManager(); > manager.put(new Key(fileName, Source.class), source); > Spec spec = (Spec) manager.get(new Key(fileName, > Spec.class)); > TypeCheckUtils.typecheck(spec, manager, true); > > but it fails to detect type errors. As I could see, this > method works well with Expr and Pred terms, but fails with > Spec and Para terms, among others. > > Previously, I was loading my specifications with a piece of > code similar to this: > > Source source = new FileSource(filename); > manager.put(new Key<Source>(filename, > Source.class), source); > Spec spec = (Spec) manager.get(key); > String sectName = null; > for (Sect sect : spec.getSect()) { > if (sect instanceof ZSect) { > sectName = ((ZSect) sect).getName(); > Key<SectTypeEnvAnn> typekey = > new Key<SectTypeEnvAnn>(sectName, > SectTypeEnvAnn.class); > manager.get(typekey); > } > } > > but it fails to load specs with uses of variables before > their declarations. > > Any suggestion? > > Cheers, > > Pablo > > > > > On Sun, May 30, 2010 at 3:58 AM, Tim Miller > <tm...@un... <mailto:tm...@un...> > <mailto:tm...@un... > <mailto:tm...@un...>>> wrote: > > Hi Pablo, > > The TypeCheckUtils class contains an overloaded static > methods > called "typecheck". The one you want is: > > typecheck(Term term, SectionManager sectInfo, boolean > useBeforeDecl) > > Set useBeforeDecl to "true" if you want to enable the use of > variables before declaration. There are several other > "typecheck" > methods in the same class that also do this, but which > offer several > other properties as well. > > Regards, > Tim > > Pablo Rodriguez Monetti wrote: > > Hi Czt'ers, > > I would like to know if there is any way to load, > through the > CZT API, Z specifications that have uses of variables > before > their declaration. With "load" I mean parse the > specifications > as well as typeckeck them. The desired behaviour > would be like > the the one provided by the -d (dependency analysis) > feature of > fuzz. > > Cheers, > > Pablo Rodríguez Monetti > > > > ------------------------------------------------------------------------ > > > ------------------------------------------------------------------------------ > > > > > ------------------------------------------------------------------------ > > _______________________________________________ > CZT-Users mailing list > CZT...@li... > <mailto:CZT...@li...> > <mailto:CZT...@li... > <mailto:CZT...@li...>> > > https://lists.sourceforge.net/lists/listinfo/czt-users > > > > > > |
|
From: Pablo R. M. <rod...@gm...> - 2010-07-07 15:37:19
|
Hi czt'ers,
I had a problem trying to load an specification with uses before
declarations. In general, this kind of models are supported. For example, I
could correctly load the following specification:
\begin{zed}
Integers == Positives \lor Negatives \lor Zero
\end{zed}
\begin{zed}
Positives == [a: \nat | a > 0] \\
Negatives == [a: \nat | a < 0] \\
Zero == [a: \nat | a = 0] \\
\end{zed}
However, the following one could not be loaded in the given order:
\begin{gendef}[X]
optional:\power X \fun \power (\power X)\\
\end{gendef}
\begin{zed}
FFName == String \{2\}\\
\end{zed}
\begin{schema}{FF}
name: FFName\\
\end{schema}
\begin{schema}{NI}
hI: optional~HI\\
\end{schema}
\begin{schema}{HI}
hF:FF\\
\end{schema}
\begin{zed}
STRING == \seq \nat \\
\end{zed}
\begin{axdef}
String : \power(\nat) \fun \power(STRING) \\
\end{axdef}
reporting the following error:
"ubf2.tex", line 13: Implicit parameters not determined
Expression: optional
It's very sensitive to exactly what the declaration sequence is. For
example, if I change the declaration of FFName from String{2} to STRING, it
works fine. If I reorder the specification appropriately, it works fine too.
Cheers,
Pablo
On Tue, Jun 1, 2010 at 3:13 PM, Pablo Rodriguez Monetti <
rod...@gm...> wrote:
> Hi Tim,
>
> You are right! The problem was that I was mistakenly expecting the
> typecheck() method to throw an exception whenever there was an error (like I
> did with manager.get() ) and forgot to check the return value :S
>
> However, a few weeks ago, I cloned and "manually" modify the AST structure
> of an AxPara (conjugating its predicate to a given predicate P, to typecheck
> P in the context of the variables declared in the AxPara) and when I wanted
> to typecheck the resulting AxPara, calling typecheck() with the AxPara
> object failed to find errors while calling the method with the SchExpr
> associated to the AxPara was successful (ie. it found errors, if any).
> That's why I believed that the typecheck() method failed with some types of
> terms and was ok with others.
>
> Many thanks!
>
> Pablo
>
>
>
> On Mon, May 31, 2010 at 8:19 PM, Tim Miller <tm...@un...>wrote:
>
>> Hi Pablo,
>>
>> Can you post the example that you are trying to typecheck?
>>
>> If I use the source code that you pasted into your email, everything seems
>> to work ok for me. I have the following example:
>>
>> \begin{zed}
>> x == y
>> \end{zed}
>>
>> \begin{zed}
>> y == 1
>> \end{zed}
>>
>> \begin{axdef}
>> \where
>> x \in y
>> \end{axdef}
>>
>> in which 'y' is used before it is declared, and there is a type mismatch
>> in the axdef. If I compile and run the following code, it reports the type
>> mismatch, but not the use before declaration:
>>
>> import java.util.List;
>>
>> import net.sourceforge.czt.typecheck.z.*;
>> import net.sourceforge.czt.z.ast.*;
>> import net.sourceforge.czt.session.*;
>>
>> public class Test
>> {
>>
>> public static void main(String [] args) throws Exception
>> {
>> String fileName = "usebeforedecl.tex";
>>
>> Source source = new FileSource(fileName);
>> SectionManager manager = new SectionManager();
>> manager.put(new Key(fileName, Source.class), source);
>> Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
>> List<? extends ErrorAnn> errors =
>>
>> TypeCheckUtils.typecheck(spec, manager, true);
>>
>> for (ErrorAnn error : errors) {
>> System.out.println(error);
>> }
>> }
>> }
>>
>>
>> If I set the use before declaration flag to false, it reports both.
>>
>> Can you try this and see what you get?
>>
>> Thanks,
>>
>> Tim
>>
>> Pablo Rodriguez Monetti wrote:
>>
>>> Hi Tim,
>>>
>>> Many thanks for your answer!
>>>
>>> I have tried with the typecheck() method, passing as first argument an
>>> Spec object:
>>>
>>> Source source = new FileSource(fileName);
>>> SectionManager manager = new SectionManager();
>>> manager.put(new Key(fileName, Source.class), source);
>>> Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
>>> TypeCheckUtils.typecheck(spec, manager, true);
>>>
>>> but it fails to detect type errors. As I could see, this method works
>>> well with Expr and Pred terms, but fails with Spec and Para terms, among
>>> others.
>>>
>>> Previously, I was loading my specifications with a piece of code similar
>>> to this:
>>>
>>> Source source = new FileSource(filename);
>>> manager.put(new Key<Source>(filename, Source.class), source);
>>> Spec spec = (Spec) manager.get(key);
>>> String sectName = null;
>>> for (Sect sect : spec.getSect()) {
>>> if (sect instanceof ZSect) {
>>> sectName = ((ZSect) sect).getName();
>>> Key<SectTypeEnvAnn> typekey =
>>> new Key<SectTypeEnvAnn>(sectName,
>>> SectTypeEnvAnn.class);
>>> manager.get(typekey);
>>> }
>>> }
>>>
>>> but it fails to load specs with uses of variables before their
>>> declarations.
>>>
>>> Any suggestion?
>>>
>>> Cheers,
>>>
>>> Pablo
>>>
>>>
>>>
>>>
>>> On Sun, May 30, 2010 at 3:58 AM, Tim Miller <tm...@un...<mailto:
>>> tm...@un...>> wrote:
>>>
>>> Hi Pablo,
>>>
>>> The TypeCheckUtils class contains an overloaded static methods
>>> called "typecheck". The one you want is:
>>>
>>> typecheck(Term term, SectionManager sectInfo, boolean useBeforeDecl)
>>>
>>> Set useBeforeDecl to "true" if you want to enable the use of
>>> variables before declaration. There are several other "typecheck"
>>> methods in the same class that also do this, but which offer several
>>> other properties as well.
>>>
>>> Regards,
>>> Tim
>>>
>>> Pablo Rodriguez Monetti wrote:
>>>
>>> Hi Czt'ers,
>>>
>>> I would like to know if there is any way to load, through the
>>> CZT API, Z specifications that have uses of variables before
>>> their declaration. With "load" I mean parse the specifications
>>> as well as typeckeck them. The desired behaviour would be like
>>> the the one provided by the -d (dependency analysis) feature of
>>> fuzz.
>>>
>>> Cheers,
>>>
>>> Pablo Rodríguez Monetti
>>>
>>>
>>>
>>> ------------------------------------------------------------------------
>>>
>>>
>>> ------------------------------------------------------------------------------
>>>
>>>
>>>
>>>
>>> ------------------------------------------------------------------------
>>>
>>> _______________________________________________
>>> CZT-Users mailing list
>>> CZT...@li...
>>> <mailto:CZT...@li...>
>>>
>>> https://lists.sourceforge.net/lists/listinfo/czt-users
>>>
>>>
>>>
>>>
>>
>
|
|
From: Pablo R. M. <rod...@gm...> - 2010-06-15 15:33:20
|
Thanks for your answer, Petra! It was pretty useful.
Cheers,
Pablo
On Thu, Jun 10, 2010 at 6:46 AM, Petra Malik <Pet...@ec...>wrote:
> Hi Pablo,
>
> You wrote:
> > I am having troubles in determining, from the Z Standard, which names
> > are valid (and which are not) for user-defined operators. In Page 28,
> > the Z Standard assures "Each operator template creates additional
> > keyword-like associations between WORDs and operator tokens.". However,
> > not all WORD seems to be accepted. And I could not find more
> > restrictions about this issue in the Z Standard.
>
> There are a few more restrictions on user-defined operators on page 35
> (8.3 User-defined operators). Also relevant to your question is page 25
> (7.2 Formal definition of context-free lexis) and page 26 (7.3
> Additional lexical restrictions, notes and examples) as well as page 84
> (Annex A; A.2 LaTeX mark-up).
>
> > the following are rejected:
>
> > \_ <1 \_: X \rel X
>
> "<1" is lexed as two tokens: the DECORWORD "<" followed by DECORWORD
> "1". If you have a look at page 25, you'll find that "1" is an ALPHASTR
> while "<" is a SYMBOLSTR and if you want to form a word out of those you
> have to put WORDGLUE between the two like in "<_1".
>
>
> > \_ <? \_: \nat \rel \nat \\
>
> "<?" is actually a DECORWORD but since you are using LaTeX mark-up and
> spaces are added around "<" (see page 84 of the Standard) it is lexed as
> two words. To avoid having spaces added when translating from LaTeX to
> Unicode add braces: "{<}?"
>
> > \function 40 \leftassoc (\_ ope \_)
>
> Here you need hard spaces: "\_~ope~\_" or even better use the \varg
> latex command "\varg ope \varg" to avoid having the lexer merge the
> underscore and "ope" to a word. (Note that "_" is defined as WORDGLUE
> on page 21 and then used to glue words on page 25.)
>
> > I suppose that the name cannot start with a letter
>
> It can start with a letter as in the ope example above.
>
> > nor finish with a stroke (case in which it is
> > a DECORDWORD instead of a WORD).
>
> And it can have decorations, too.
>
> > However, I understand that <1 and 1< are valid WORD's.
>
> But they are not; see example above.
>
> > Additionally, which situations, where an operator appear, needs to
> > previously define the corresponding operator template paragraph and
> > which not? The following two paragraphs are accepted without one of
> > these paragraphs:
> >
> > \begin{gendef}[X]
> > \_ <_1 \_: X \rel X
> > \end{gendef}
>
> That's because in one of the toolkits there is an operator template for
> "<" and the mapping to operator tokens is based on the WORD part (see
> page 27).
>
> Hope this helps,
> Petra
>
>
> ------------------------------------------------------------------------------
> ThinkGeek and WIRED's GeekDad team up for the Ultimate
> GeekDad Father's Day Giveaway. ONE MASSIVE PRIZE to the
> lucky parental unit. See the prize list and enter to win:
> http://p.sf.net/sfu/thinkgeek-promo
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users
>
|
|
From: Petra M. <Pet...@ec...> - 2010-06-10 09:46:34
|
Hi Pablo,
You wrote:
> I am having troubles in determining, from the Z Standard, which names
> are valid (and which are not) for user-defined operators. In Page 28,
> the Z Standard assures "Each operator template creates additional
> keyword-like associations between WORDs and operator tokens.". However,
> not all WORD seems to be accepted. And I could not find more
> restrictions about this issue in the Z Standard.
There are a few more restrictions on user-defined operators on page 35
(8.3 User-defined operators). Also relevant to your question is page 25
(7.2 Formal definition of context-free lexis) and page 26 (7.3
Additional lexical restrictions, notes and examples) as well as page 84
(Annex A; A.2 LaTeX mark-up).
> the following are rejected:
> \_ <1 \_: X \rel X
"<1" is lexed as two tokens: the DECORWORD "<" followed by DECORWORD
"1". If you have a look at page 25, you'll find that "1" is an ALPHASTR
while "<" is a SYMBOLSTR and if you want to form a word out of those you
have to put WORDGLUE between the two like in "<_1".
> \_ <? \_: \nat \rel \nat \\
"<?" is actually a DECORWORD but since you are using LaTeX mark-up and
spaces are added around "<" (see page 84 of the Standard) it is lexed as
two words. To avoid having spaces added when translating from LaTeX to
Unicode add braces: "{<}?"
> \function 40 \leftassoc (\_ ope \_)
Here you need hard spaces: "\_~ope~\_" or even better use the \varg
latex command "\varg ope \varg" to avoid having the lexer merge the
underscore and "ope" to a word. (Note that "_" is defined as WORDGLUE
on page 21 and then used to glue words on page 25.)
> I suppose that the name cannot start with a letter
It can start with a letter as in the ope example above.
> nor finish with a stroke (case in which it is
> a DECORDWORD instead of a WORD).
And it can have decorations, too.
> However, I understand that <1 and 1< are valid WORD's.
But they are not; see example above.
> Additionally, which situations, where an operator appear, needs to
> previously define the corresponding operator template paragraph and
> which not? The following two paragraphs are accepted without one of
> these paragraphs:
>
> \begin{gendef}[X]
> \_ <_1 \_: X \rel X
> \end{gendef}
That's because in one of the toolkits there is an operator template for
"<" and the mapping to operator tokens is based on the WORD part (see
page 27).
Hope this helps,
Petra
|
|
From: Pablo R. M. <rod...@gm...> - 2010-06-04 18:16:35
|
Hi czt'ers,
I am having troubles in determining, from the Z Standard, which names are
valid (and which are not) for user-defined operators. In Page 28, the Z
Standard assures "Each operator template creates additional keyword-like
associations between WORDs and operator tokens.". However, not all WORD
seems to be accepted. And I could not find more restrictions about this
issue in the Z Standard.
For example, the following paragraphs are accepted:
1)
\begin{schema}{OperatorUse}
\_ <_1 \_: \nat \rel \nat \\
t,u: \nat
\where
t <_1 u
\end{schema}
2)
\begin{zed}
\function 40 \leftassoc (\_ \ope \_)
\end{zed}
\begin{gendef}[X]
\_ \ope \_: (\nat \cross \nat) \fun \nat
\where
\forall x,y: \nat @ x \ope y = x - y
\end{gendef}
but the following are rejected:
3)
\begin{gendef}[X]
\_ <1 \_: X \rel X
\end{gendef}
4)
\begin{schema}{OperatorUse}
\_ <? \_: \nat \rel \nat \\
t,u: \nat
\where
t <? u
\end{schema}
5)
\begin{zed}
\function 40 \leftassoc (\_ ope \_)
\end{zed}
I suppose that the name cannot start with a letter (case in which it must be
prefixed by a '\') nor finish with a stroke (case in which it is a
DECORDWORD instead of a WORD). However, I understand that <1 and 1< are
valid WORD's. In summary, I would like to determine a complete and more
precise set of rules.
Additionally, which situations, where an operator appear, needs to
previously define the corresponding operator template paragraph and which
not? The following two paragraphs are accepted without one of these
paragraphs:
\begin{gendef}[X]
\_ <_1 \_: X \rel X
\end{gendef}
\begin{schema}{State}
a,b: \nat
\where
a <_1 b
\end{schema}
Thanks in advance,
Pablo Rodriguez Monetti
|
|
From: Pablo R. M. <rod...@gm...> - 2010-06-01 18:13:42
|
Hi Tim,
You are right! The problem was that I was mistakenly expecting the
typecheck() method to throw an exception whenever there was an error (like I
did with manager.get() ) and forgot to check the return value :S
However, a few weeks ago, I cloned and "manually" modify the AST structure
of an AxPara (conjugating its predicate to a given predicate P, to typecheck
P in the context of the variables declared in the AxPara) and when I wanted
to typecheck the resulting AxPara, calling typecheck() with the AxPara
object failed to find errors while calling the method with the SchExpr
associated to the AxPara was successful (ie. it found errors, if any).
That's why I believed that the typecheck() method failed with some types of
terms and was ok with others.
Many thanks!
Pablo
On Mon, May 31, 2010 at 8:19 PM, Tim Miller <tm...@un...> wrote:
> Hi Pablo,
>
> Can you post the example that you are trying to typecheck?
>
> If I use the source code that you pasted into your email, everything seems
> to work ok for me. I have the following example:
>
> \begin{zed}
> x == y
> \end{zed}
>
> \begin{zed}
> y == 1
> \end{zed}
>
> \begin{axdef}
> \where
> x \in y
> \end{axdef}
>
> in which 'y' is used before it is declared, and there is a type mismatch in
> the axdef. If I compile and run the following code, it reports the type
> mismatch, but not the use before declaration:
>
> import java.util.List;
>
> import net.sourceforge.czt.typecheck.z.*;
> import net.sourceforge.czt.z.ast.*;
> import net.sourceforge.czt.session.*;
>
> public class Test
> {
>
> public static void main(String [] args) throws Exception
> {
> String fileName = "usebeforedecl.tex";
>
> Source source = new FileSource(fileName);
> SectionManager manager = new SectionManager();
> manager.put(new Key(fileName, Source.class), source);
> Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
> List<? extends ErrorAnn> errors =
>
> TypeCheckUtils.typecheck(spec, manager, true);
>
> for (ErrorAnn error : errors) {
> System.out.println(error);
> }
> }
> }
>
>
> If I set the use before declaration flag to false, it reports both.
>
> Can you try this and see what you get?
>
> Thanks,
>
> Tim
>
> Pablo Rodriguez Monetti wrote:
>
>> Hi Tim,
>>
>> Many thanks for your answer!
>>
>> I have tried with the typecheck() method, passing as first argument an
>> Spec object:
>>
>> Source source = new FileSource(fileName);
>> SectionManager manager = new SectionManager();
>> manager.put(new Key(fileName, Source.class), source);
>> Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
>> TypeCheckUtils.typecheck(spec, manager, true);
>>
>> but it fails to detect type errors. As I could see, this method works well
>> with Expr and Pred terms, but fails with Spec and Para terms, among others.
>>
>> Previously, I was loading my specifications with a piece of code similar
>> to this:
>>
>> Source source = new FileSource(filename);
>> manager.put(new Key<Source>(filename, Source.class), source);
>> Spec spec = (Spec) manager.get(key);
>> String sectName = null;
>> for (Sect sect : spec.getSect()) {
>> if (sect instanceof ZSect) {
>> sectName = ((ZSect) sect).getName();
>> Key<SectTypeEnvAnn> typekey =
>> new Key<SectTypeEnvAnn>(sectName,
>> SectTypeEnvAnn.class);
>> manager.get(typekey);
>> }
>> }
>>
>> but it fails to load specs with uses of variables before their
>> declarations.
>>
>> Any suggestion?
>>
>> Cheers,
>>
>> Pablo
>>
>>
>>
>>
>> On Sun, May 30, 2010 at 3:58 AM, Tim Miller <tm...@un...<mailto:
>> tm...@un...>> wrote:
>>
>> Hi Pablo,
>>
>> The TypeCheckUtils class contains an overloaded static methods
>> called "typecheck". The one you want is:
>>
>> typecheck(Term term, SectionManager sectInfo, boolean useBeforeDecl)
>>
>> Set useBeforeDecl to "true" if you want to enable the use of
>> variables before declaration. There are several other "typecheck"
>> methods in the same class that also do this, but which offer several
>> other properties as well.
>>
>> Regards,
>> Tim
>>
>> Pablo Rodriguez Monetti wrote:
>>
>> Hi Czt'ers,
>>
>> I would like to know if there is any way to load, through the
>> CZT API, Z specifications that have uses of variables before
>> their declaration. With "load" I mean parse the specifications
>> as well as typeckeck them. The desired behaviour would be like
>> the the one provided by the -d (dependency analysis) feature of
>> fuzz.
>>
>> Cheers,
>>
>> Pablo Rodríguez Monetti
>>
>>
>>
>> ------------------------------------------------------------------------
>>
>>
>> ------------------------------------------------------------------------------
>>
>>
>>
>>
>> ------------------------------------------------------------------------
>>
>> _______________________________________________
>> CZT-Users mailing list
>> CZT...@li...
>> <mailto:CZT...@li...>
>>
>> https://lists.sourceforge.net/lists/listinfo/czt-users
>>
>>
>>
>>
>
|
|
From: Tim M. <tm...@un...> - 2010-05-31 23:19:32
|
Hi Pablo,
Can you post the example that you are trying to typecheck?
If I use the source code that you pasted into your email, everything
seems to work ok for me. I have the following example:
\begin{zed}
x == y
\end{zed}
\begin{zed}
y == 1
\end{zed}
\begin{axdef}
\where
x \in y
\end{axdef}
in which 'y' is used before it is declared, and there is a type mismatch
in the axdef. If I compile and run the following code, it reports the
type mismatch, but not the use before declaration:
import java.util.List;
import net.sourceforge.czt.typecheck.z.*;
import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.session.*;
public class Test
{
public static void main(String [] args) throws Exception
{
String fileName = "usebeforedecl.tex";
Source source = new FileSource(fileName);
SectionManager manager = new SectionManager();
manager.put(new Key(fileName, Source.class), source);
Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
List<? extends ErrorAnn> errors =
TypeCheckUtils.typecheck(spec, manager, true);
for (ErrorAnn error : errors) {
System.out.println(error);
}
}
}
If I set the use before declaration flag to false, it reports both.
Can you try this and see what you get?
Thanks,
Tim
Pablo Rodriguez Monetti wrote:
> Hi Tim,
>
> Many thanks for your answer!
>
> I have tried with the typecheck() method, passing as first argument an
> Spec object:
>
> Source source = new FileSource(fileName);
> SectionManager manager = new SectionManager();
> manager.put(new Key(fileName, Source.class), source);
> Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
> TypeCheckUtils.typecheck(spec, manager, true);
>
> but it fails to detect type errors. As I could see, this method works
> well with Expr and Pred terms, but fails with Spec and Para terms, among
> others.
>
> Previously, I was loading my specifications with a piece of code similar
> to this:
>
> Source source = new FileSource(filename);
> manager.put(new Key<Source>(filename, Source.class), source);
> Spec spec = (Spec) manager.get(key);
> String sectName = null;
> for (Sect sect : spec.getSect()) {
> if (sect instanceof ZSect) {
> sectName = ((ZSect) sect).getName();
> Key<SectTypeEnvAnn> typekey =
> new Key<SectTypeEnvAnn>(sectName,
> SectTypeEnvAnn.class);
> manager.get(typekey);
> }
> }
>
> but it fails to load specs with uses of variables before their declarations.
>
> Any suggestion?
>
> Cheers,
>
> Pablo
>
>
>
>
> On Sun, May 30, 2010 at 3:58 AM, Tim Miller <tm...@un...
> <mailto:tm...@un...>> wrote:
>
> Hi Pablo,
>
> The TypeCheckUtils class contains an overloaded static methods
> called "typecheck". The one you want is:
>
> typecheck(Term term, SectionManager sectInfo, boolean useBeforeDecl)
>
> Set useBeforeDecl to "true" if you want to enable the use of
> variables before declaration. There are several other "typecheck"
> methods in the same class that also do this, but which offer several
> other properties as well.
>
> Regards,
> Tim
>
> Pablo Rodriguez Monetti wrote:
>
> Hi Czt'ers,
>
> I would like to know if there is any way to load, through the
> CZT API, Z specifications that have uses of variables before
> their declaration. With "load" I mean parse the specifications
> as well as typeckeck them. The desired behaviour would be like
> the the one provided by the -d (dependency analysis) feature of
> fuzz.
>
> Cheers,
>
> Pablo Rodríguez Monetti
>
>
> ------------------------------------------------------------------------
>
> ------------------------------------------------------------------------------
>
>
>
> ------------------------------------------------------------------------
>
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> <mailto:CZT...@li...>
> https://lists.sourceforge.net/lists/listinfo/czt-users
>
>
>
|
|
From: Pablo R. M. <rod...@gm...> - 2010-05-31 20:59:52
|
Hi Tim,
Many thanks for your answer!
I have tried with the typecheck() method, passing as first argument an Spec
object:
Source source = new FileSource(fileName);
SectionManager manager = new SectionManager();
manager.put(new Key(fileName, Source.class), source);
Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
TypeCheckUtils.typecheck(spec, manager, true);
but it fails to detect type errors. As I could see, this method works well
with Expr and Pred terms, but fails with Spec and Para terms, among others.
Previously, I was loading my specifications with a piece of code similar to
this:
Source source = new FileSource(filename);
manager.put(new Key<Source>(filename, Source.class), source);
Spec spec = (Spec) manager.get(key);
String sectName = null;
for (Sect sect : spec.getSect()) {
if (sect instanceof ZSect) {
sectName = ((ZSect) sect).getName();
Key<SectTypeEnvAnn> typekey =
new Key<SectTypeEnvAnn>(sectName,
SectTypeEnvAnn.class);
manager.get(typekey);
}
}
but it fails to load specs with uses of variables before their declarations.
Any suggestion?
Cheers,
Pablo
On Sun, May 30, 2010 at 3:58 AM, Tim Miller <tm...@un...> wrote:
> Hi Pablo,
>
> The TypeCheckUtils class contains an overloaded static methods called
> "typecheck". The one you want is:
>
> typecheck(Term term, SectionManager sectInfo, boolean useBeforeDecl)
>
> Set useBeforeDecl to "true" if you want to enable the use of variables
> before declaration. There are several other "typecheck" methods in the same
> class that also do this, but which offer several other properties as well.
>
> Regards,
> Tim
>
> Pablo Rodriguez Monetti wrote:
>
>> Hi Czt'ers,
>>
>> I would like to know if there is any way to load, through the CZT API, Z
>> specifications that have uses of variables before their declaration. With
>> "load" I mean parse the specifications as well as typeckeck them. The
>> desired behaviour would be like the the one provided by the -d (dependency
>> analysis) feature of fuzz.
>>
>> Cheers,
>>
>> Pablo Rodríguez Monetti
>>
>>
>> ------------------------------------------------------------------------
>>
>>
>> ------------------------------------------------------------------------------
>>
>>
>>
>> ------------------------------------------------------------------------
>>
>> _______________________________________________
>> CZT-Users mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-users
>>
>
>
|
|
From: Tim M. <tm...@un...> - 2010-05-30 07:28:45
|
Hi Pablo, The TypeCheckUtils class contains an overloaded static methods called "typecheck". The one you want is: typecheck(Term term, SectionManager sectInfo, boolean useBeforeDecl) Set useBeforeDecl to "true" if you want to enable the use of variables before declaration. There are several other "typecheck" methods in the same class that also do this, but which offer several other properties as well. Regards, Tim Pablo Rodriguez Monetti wrote: > Hi Czt'ers, > > I would like to know if there is any way to load, through the CZT API, Z > specifications that have uses of variables before their declaration. > With "load" I mean parse the specifications as well as typeckeck them. > The desired behaviour would be like the the one provided by the -d > (dependency analysis) feature of fuzz. > > Cheers, > > Pablo Rodríguez Monetti > > > ------------------------------------------------------------------------ > > ------------------------------------------------------------------------------ > > > > ------------------------------------------------------------------------ > > _______________________________________________ > CZT-Users mailing list > CZT...@li... > https://lists.sourceforge.net/lists/listinfo/czt-users |
11 messages has been excluded from this view by a project administrator.
