czt-users — For end-users of the CZT tools

[CZT-Users] Loading specs with uses of variables before their declaration

[Pablo R. M. <rod...@gm...>]

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

Re: [CZT-Users] Mutually recursive free type inconsistency

[Nicolas Wu <nic...@co...>]

For the record, I think I've answered my own question by adding:

%%Zinword \& {&}

at the beginning of the file.

Thanks,

Nick

On Wed, Mar 3, 2010 at 5:27 PM, Nicolas Wu <nic...@co...> wrote:
> I've just come across an inconsistency in the CZT typechecker, and how
> it fits with the czt.sty file, with regards to mutually recursive free
> types.
>
> The typechecker allows the following code:
>
> \begin{zed}
>  A ::= a | aa \ldata B \rdata &
>  B ::= b | bb \ldata A \rdata
> \end{zed}
>
> However, this isn't LaTeX friendly, since '&' is used for alignment.
> The czt-guide.pdf document (Section 5.1, page 13), which documents
> czt.sty, claims that the LaTeX for the '&' should be '\&', which makes
> sense. However, using this breaks the typechecker, which reports:
>
> nwu@clpc181~/scrap$ java -jar czt_1_5_0_bin.jar Freetypes.tex
> 1 warnings and errors
> line 5 column 31 in "Freetypes.tex": Unknown latex command
>
> Is there a quick work around for this?
>
> Thanks,
>
> Nick
>

[CZT-Users] Mutually recursive free type inconsistency

[Nicolas Wu <nic...@co...>]

I've just come across an inconsistency in the CZT typechecker, and how
it fits with the czt.sty file, with regards to mutually recursive free
types.

The typechecker allows the following code:

\begin{zed}
  A ::= a | aa \ldata B \rdata &
  B ::= b | bb \ldata A \rdata
\end{zed}

However, this isn't LaTeX friendly, since '&' is used for alignment.
The czt-guide.pdf document (Section 5.1, page 13), which documents
czt.sty, claims that the LaTeX for the '&' should be '\&', which makes
sense. However, using this breaks the typechecker, which reports:

nwu@clpc181~/scrap$ java -jar czt_1_5_0_bin.jar Freetypes.tex
1 warnings and errors
line 5 column 31 in "Freetypes.tex": Unknown latex command

Is there a quick work around for this?

Thanks,

Nick

Re: [CZT-Users] Custom LaTeX commands

[James W. <jw...@cs...>]

Hi Tim,

Thanks very much! Fingers crossed that's the last time I'll bug you for a while :)

*Gets back to writing tool in time for ABZ...*

Cheers!

James

On 16 Feb 2010, at 22:57, Tim Miller wrote:

> Hi James,
> 
> You wrote:
>>    %I define my generic:
>>    %%Zpreword \mult mult
>>    \begin{zed}
>>    \generic (\mult~\_)
>>    \end{zed}
> <snipped>
>>    % I define mult mathematically
>>    \begin{gendef}[X, Y]
>>      \mult\_: \power  ((X \rel  Y) \cross  \power  X \cross  \power  Y
>>    \cross  MultTy \cross  \finset  \nat  \cross  \finset  \nat )
>>    \where
>>    \forall  r: X \rel  Y; sx: \power  X; sy: \power  Y; s_1, s_2: \finset
>>    \nat  @ \\ \t1
>>         (\mult (r, sx, sy, mm, s_1, s_2)) \iff  r \in sx \rel  sy
>>    \also
>>    ...
>>    \end{gendef}
>>    But I get the following error:
>> 
> It appears that you are defining \mult as a relation. So the first paragraph above should be:
> 
> \begin{zed}
> \relation (\mult~\_)
> \end{zed}
> 
> This tells the parser that \mult should be treated as a relation, not a function, although the error message that it generates is not so useful! It is actually parsing this as a function, which parses fine, but then the typechecker is complaining.
> 
>> \newcommand{\oset}{\mathcal{O}}
>> %%Zword \oset
>> \begin{schema}{Example}
>> \oset : \num
>> \end{schema}
>> 
> You just left off the unicode definition for \oset. So it should be:
> 
> %%Zword \oset oset
> 
> for a word, or
> 
> %%Zchar \oset U+???
> 
> for some unicode character.
> 
> Cheers,
> Tim

Re: [CZT-Users] Custom LaTeX commands

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

Hi James,

You wrote:
>     %I define my generic:
>     %%Zpreword \mult mult
>     \begin{zed}
>     \generic (\mult~\_)
>     \end{zed}
<snipped>
>     % I define mult mathematically
>     \begin{gendef}[X, Y]
>       \mult\_: \power  ((X \rel  Y) \cross  \power  X \cross  \power  Y
>     \cross  MultTy \cross  \finset  \nat  \cross  \finset  \nat )
>     \where
>     \forall  r: X \rel  Y; sx: \power  X; sy: \power  Y; s_1, s_2: \finset
>     \nat  @ \\ \t1
>          (\mult (r, sx, sy, mm, s_1, s_2)) \iff  r \in sx \rel  sy
>     \also
>     ...
>     \end{gendef}
> 
>     But I get the following error:
>
It appears that you are defining \mult as a relation. So the first 
paragraph above should be:

\begin{zed}
\relation (\mult~\_)
\end{zed}

This tells the parser that \mult should be treated as a relation, not a 
function, although the error message that it generates is not so useful! 
It is actually parsing this as a function, which parses fine, but then 
the typechecker is complaining.

> \newcommand{\oset}{\mathcal{O}}
> %%Zword \oset
> 
> \begin{schema}{Example}
> \oset : \num
> \end{schema}
>
You just left off the unicode definition for \oset. So it should be:

%%Zword \oset oset

for a word, or

%%Zchar \oset U+???

for some unicode character.

Cheers,
Tim

Re: [CZT-Users] Custom LaTeX commands

[James W. <jw...@cs...>]

Hi again,

Further to my last e-mail, I was able to define mult in the way suggested by Tim Miller. However, I'm getting a type-check error that I don't understand:

%I define my generic:
%%Zpreword \mult mult
\begin{zed}
	\generic (\mult~\_)
\end{zed}

% This is used in the gendef
\begin{zed}
MultTy ::= mm | mo | om | mzo | zom | oo | zozo | zoo | ozo | ms | sm
| ss \\ \t1
| so | os | szo | zos
\end{zed}

% I define mult mathematically
\begin{gendef}[X, Y]
  \mult\_: \power  ((X \rel  Y) \cross  \power  X \cross  \power  Y \cross  MultTy \cross  \finset  \nat  \cross  \finset  \nat )
\where
\forall  r: X \rel  Y; sx: \power  X; sy: \power  Y; s_1, s_2: \finset
\nat  @ \\ \t1
     (\mult (r, sx, sy, mm, s_1, s_2)) \iff  r \in sx \rel  sy
\also
	...
\end{gendef}

But I get the following error:

Schema expression required in expression predicate
	Expression: ( mult ( r , sx , sy , mm , s_{1}~, s_{2} ) )
	Type: \power ( \power ( X \cross Y ) \cross \power X \cross \power Y \cross MultTy \cross \power \arithmos \cross \power \arithmos )
Name "mult~\_" requires no parameters within its own definition

Have I defined mult incorrectly? This isn't my own Z, and has been used in the past (but not on ISO Z). I'm just trying to get it to type-check. (For those interested in what mult is meant to do - it's defining multiplicities between classes - mm=many to many, mo=many to one, and so on)

One other thing, related to latex definitions. I do the following:

\newcommand{\oset}{\mathcal{O}}
%%Zword \oset

\begin{schema}{Example}
	\oset : \num
\end{schema}

But I get a "Syntax error at symbol COLON" parse exception. How should I define \oset if I want to use it as a declaration name? I've been looking through the Z standard, but can't work it out.

Thanks again, your help is really appreciated.

James

Re: [CZT-Users] Custom LaTeX commands

[James W. <jw...@cs...>]

Thanks to both Petra and Tim for their quick response.

I've managed to get that working now, thanks very much :) I'll have to stop using fuzz from now on!

Kind regards,
James

On 16 Feb 2010, at 03:33, Tim Miller wrote:

> Hi James,
> 
> You wrote:
>> I get an "Unknown latex command \mult" exception when this is parsed. How can I make CZT recognise these custom commands?
>> 
> There are two steps that you will have to take.
> 
> The first is related to the unicode character/word that the command represents. The CZT scanner/parser only accepts unicode as input, so latex specifications are translated into unicode first. In conforming with the Z standard, each latex command must be accompanied with a corresponding unicode character or word. Your command appears to be a prefix word, so would be declared using:
> 
> %%Zpreword \mult mult
> 
> in which "mult" is the unicode word.
> 
> The second is related to the parser. As specified in the Z standard, the format of user-defined operators must be declared using operator templates. In your example, this would be:
> 
> \begin{zed}
> \generic (\mult \_)
> \end{zed}
> 
> With any luck, this should parse for you now.
> 
> Regards,
> Tim

Re: [CZT-Users] Custom LaTeX commands

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

Hi James,

You wrote:
> I get an "Unknown latex command \mult" exception when this is parsed. How can I make CZT recognise these custom commands?
>
There are two steps that you will have to take.

The first is related to the unicode character/word that the command 
represents. The CZT scanner/parser only accepts unicode as input, so 
latex specifications are translated into unicode first. In conforming 
with the Z standard, each latex command must be accompanied with a 
corresponding unicode character or word. Your command appears to be a 
prefix word, so would be declared using:

%%Zpreword \mult mult

in which "mult" is the unicode word.

The second is related to the parser. As specified in the Z standard, the 
format of user-defined operators must be declared using operator 
templates. In your example, this would be:

\begin{zed}
\generic (\mult \_)
\end{zed}

With any luck, this should parse for you now.

Regards,
Tim

Re: [CZT-Users] Custom LaTeX commands

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

Hi James,

> I'm writing a tool that utilises CZT's parser and type-checker, but
> I'm unsure how to make CZT recognise custom LaTeX commands.
> 
> For example, I define a new relation "mult":
> 
> \newcommand{\mult}{\textsf{mult}}
> %%prerel \mult

I don't think prerel is recognised in ISO Z.  You probably want
something like
%%Zpreword \mult mult

See the ISO Z Standard for a definition of these %%-thingies, or have a
look at one of the toolkit specifications for examples how they are used.
http://czt.svn.sourceforge.net/viewvc/czt/trunk/parser/src/main/resources/lib/relation_toolkit.tex?revision=4221&view=markup

Hope this helps,
Petra

Re: [CZT-Users] Custom LaTeX commands

[James W. <jw...@cs...>]

Hi there,

I'm writing a tool that utilises CZT's parser and type-checker, but I'm unsure how to make CZT recognise custom LaTeX commands.

For example, I define a new relation "mult":

\newcommand{\mult}{\textsf{mult}}
%%prerel \mult

\begin{gendef}[X, Y]
	\mult \_ : \power (........)
\where
	.....
\end{gendef}

I get an "Unknown latex command \mult" exception when this is parsed. How can I make CZT recognise these custom commands?

Any help is much appreciated.

Kind regards,

James Williams

Re: [CZT-Users] CZT jEdit Plugin

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

Vincent DIEMUNSCH wrote:
> [...]
> Then I downloaded the jEdit editor and installed it properly, but I
> could'nt find the
> files of the plugin mentionned in the jEdit plugin page
> (http://czt.sourceforge.net/jedit/index.html) :
> ZCharMap.jar, ZSideKick.jar, CZT.jar, ZLivePlugin.jar...
> 
> Where can I find them ? The best would be as binaries...

CZT can be downloaded from
http://sourceforge.net/projects/czt/files/czt/
Version 1.5.0 does not seem to have binaries for the plugins, but
version 1.0 does.  Download either czt-1.0-bin.tar.bz2 or
czt-1.0-bin.tar.gz or czt-1.0-bin.zip, unzip and have a look in
directory lib (or bin).

Hope this helps,
Petra

[CZT-Users] CZT jEdit Plugin

[Vincent D. <vin...@gm...>]

Hello

I would like to install the CZT plugin for jEdit.

I downloaded the "czt_1_5_0_bin.jar" file, and launched it but I couldn't do
anything :
it can only read a file and I have no files to give to it, I wanted to
create a new one
but I don't know how...

Then I downloaded the jEdit editor and installed it properly, but I could'nt
find the
files of the plugin mentionned in the jEdit plugin page (
http://czt.sourceforge.net/jedit/index.html) :
ZCharMap.jar, ZSideKick.jar, CZT.jar, ZLivePlugin.jar...

Where can I find them ? The best would be as binaries...

Thanks in advance for your help.

Vincent

[CZT-Users] [eclipse plugin] inclusion/reference of specification in another file

[sylvain n. <syl...@go...>]

Hi,
first of all, congratulation for the Eclipse CZT plugin. It works well.

Do you plan to integrate a Z animator in it?

One complain: it seems that the plugin does not accept another file ending
as .zed{8,16} (it crashes).
This is a shame, because a file can actually contain at least three types of
texts:
- informal, narrative specifications
- Z specifications
- source code
It would be great to be able to edit the same file with different editors
depending on the "view" I need to.
For example I would like to write a specification with the CZT plugin and
then add C code using CDT, close to the specification it implements.
For now I have to rename the file to do this.

In fact, my most urgent question is the following: how can I reference a
specification written in a file into another?

Another question: do you know of any ready-to-use Z specification for real
numbers?

Thanks in advance for your answers,
Sylvain

Re: [CZT-Users] how to ?

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

Hi Massimo,

Object-Z supports polymorphism via class union and polymorphic
declarations (see Object-Z books for details). In the example

\begin{class}{Account}
\end{class}

\begin{class}{SavingsAccount}
Account
\end{class}

\begin{class}{Bank}
\begin{state}
  accts: \power (\poly Account)
\end{state}
\end{class}

accts can contain SavingsAccounts as well as normal Accounts.

There are polymorphic extensions to Object-Z
(see Waheed, Khan, Nadeem: Polymorphic Extensions to Object-Z
specifications), which claim to provide better support for polymorphism
but are not supported in CZT yet.

Hope this helps,
Petra

Re: [CZT-Users] how to ?

[Massimo C. <cos...@pa...>]

Dear Nelis,
it worked thanks!
Any idea for polimorphism?


Regards
Massimo



Il giorno 18/mar/09, alle ore 16:53, Nelis Boucke ha scritto:

> Hallo Massimo,
>
> For the second question: did you enable use before declaration?
>
> Go to the menu "Plugins" --> "Plugin Options" --> "ZSideKick", and  
> then select the option that enables used before declaration.
>
> If the option is not there, you might have an older version. If the  
> newest version is not yet downloadable, I can send you a later  
> version compiled by Tim Miller including this option.
>
> greetings,
> Nelis
>
> On 18-mrt-09, at 16:10, Massimo Cossentino wrote:
>
>> Dear all,
>> in my lab we are using CZT (Jedit version) in order to specify the
>> structure of a system that will be probably initially developed in
>> Java but later we are going to define a specific language to  
>> support it.
>> The application domain is the definition of a new multi-agent system
>> inheritance paradigm.
>>
>> As I said we are using the Jedit based verson of the tool and this is
>> proving very useful. In our opinion it does not make any sense to use
>> a formal language for specifying something if I do not have any check
>> on the correctness of my specification.
>>
>> I am now writing this email because for our purposes the tool has two
>> significant limits. Indeed we are not sure these are really limits,
>> perhaps we just do not know how to do and for this reason I am asking
>> the help of this community.
>>
>> Here is what we need:
>> 1) we need to specify polimorfism in a class (we are using object-Z)
>> 2) we have a class that can be composed of other instances of the  
>> same
>> class (aggregation relationship self-loop).
>>
>> Problems we had with that:
>> 1) we do not know how to specify polimorfism
>> 2) if in our class (ConceptGene) we specify an attribute of type
>> ConceptGene we receive a syntax error message.
>>
>>
>> thanks for your help with that
>>
>> Best Regards
>> Massimo
>>
>>
>>
>>
>>
>> ------------------------------------------------------------------------------
>> Apps built with the Adobe(R) Flex(R) framework and Flex Builder(TM)  
>> are
>> powering Web 2.0 with engaging, cross-platform capabilities.  
>> Quickly and
>> easily build your RIAs with Flex Builder, the Eclipse(TM)based  
>> development
>> software that enables intelligent coding and step-through debugging.
>> Download the free 60 day trial. http://p.sf.net/sfu/www-adobe-com
>> _______________________________________________
>> CZT-Users mailing list
>> CZT...@li...
>> https://lists.sourceforge.net/lists/listinfo/czt-users
>
> -----
> Nelis Boucké
> Phd Researcher,
> DistriNet Labs, Departement of Computer Science, KULeuven
> Phone: +3216327575
> E-mail: nel...@cs...
>
>
>

Re: [CZT-Users] how to ?

[Nelis B. <nel...@cs...>]

Hallo Massimo,

For the second question: did you enable use before declaration?

Go to the menu "Plugins" --> "Plugin Options" --> "ZSideKick", and  
then select the option that enables used before declaration.

If the option is not there, you might have an older version. If the  
newest version is not yet downloadable, I can send you a later version  
compiled by Tim Miller including this option.

greetings,
Nelis

On 18-mrt-09, at 16:10, Massimo Cossentino wrote:

> Dear all,
> in my lab we are using CZT (Jedit version) in order to specify the
> structure of a system that will be probably initially developed in
> Java but later we are going to define a specific language to support  
> it.
> The application domain is the definition of a new multi-agent system
> inheritance paradigm.
>
> As I said we are using the Jedit based verson of the tool and this is
> proving very useful. In our opinion it does not make any sense to use
> a formal language for specifying something if I do not have any check
> on the correctness of my specification.
>
> I am now writing this email because for our purposes the tool has two
> significant limits. Indeed we are not sure these are really limits,
> perhaps we just do not know how to do and for this reason I am asking
> the help of this community.
>
> Here is what we need:
> 1) we need to specify polimorfism in a class (we are using object-Z)
> 2) we have a class that can be composed of other instances of the same
> class (aggregation relationship self-loop).
>
> Problems we had with that:
> 1) we do not know how to specify polimorfism
> 2) if in our class (ConceptGene) we specify an attribute of type
> ConceptGene we receive a syntax error message.
>
>
> thanks for your help with that
>
> Best Regards
> Massimo
>
>
>
>
>
> ------------------------------------------------------------------------------
> Apps built with the Adobe(R) Flex(R) framework and Flex Builder(TM)  
> are
> powering Web 2.0 with engaging, cross-platform capabilities. Quickly  
> and
> easily build your RIAs with Flex Builder, the Eclipse(TM)based  
> development
> software that enables intelligent coding and step-through debugging.
> Download the free 60 day trial. http://p.sf.net/sfu/www-adobe-com
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users

-----
Nelis Boucké
Phd Researcher,
DistriNet Labs, Departement of Computer Science, KULeuven
Phone: +3216327575
E-mail: nel...@cs...

[CZT-Users] how to ?

[Massimo C. <cos...@pa...>]

Dear all,
in my lab we are using CZT (Jedit version) in order to specify the  
structure of a system that will be probably initially developed in  
Java but later we are going to define a specific language to support it.
The application domain is the definition of a new multi-agent system  
inheritance paradigm.

As I said we are using the Jedit based verson of the tool and this is  
proving very useful. In our opinion it does not make any sense to use  
a formal language for specifying something if I do not have any check  
on the correctness of my specification.

I am now writing this email because for our purposes the tool has two  
significant limits. Indeed we are not sure these are really limits,  
perhaps we just do not know how to do and for this reason I am asking  
the help of this community.

Here is what we need:
1) we need to specify polimorfism in a class (we are using object-Z)
2) we have a class that can be composed of other instances of the same  
class (aggregation relationship self-loop).

Problems we had with that:
1) we do not know how to specify polimorfism
2) if in our class (ConceptGene) we specify an attribute of type  
ConceptGene we receive a syntax error message.


thanks for your help with that

Best Regards
Massimo

Re: [CZT-Users] [CZT-Devel] ZLive limitations and problem buildn with maven

[Pablo R. M. <rod...@gm...>]

Hi Mark,

I am back again to tell you about a new problem I am facing using ZLive. I
attempted to use ZLive intensively, running a number of threads that iterate
and call the evalPred() method over approximately 500 predicates. Since each
thread creates a new ZLive object, and each ZLive object consumes a
considerable amount of memory, I had to run my java app with a "-Xmx500m"
parameter, or someone similar, in order to give more memory to the JVM (Java
Virtual Machine).

Anyway, some executions finish well but others crash my JVM:

java version "1.6.0_03"
Java(TM) SE Runtime Environment (build 1.6.0_03-b05)
Java HotSpot(TM) Client VM (build 1.6.0_03-b05, mixed mode, sharing)



I have reproduced the problem with the following program, which try to
evaluate the same predicate 500 times in 12 threads:



//**************************************************
package pruebas;

import java.io.*;
import java.util.*;

import net.sourceforge.czt.z.ast.Pred;
import net.sourceforge.czt.animation.eval.*;
import net.sourceforge.czt.typecheck.z.*;


public class EvalTest{
    public static void main(String[] args) {

        for(int i=0; i<12; i++){
            (new ThreadTest(i)).start();
        }
    }
}


class ThreadTest extends Thread{

    private int threadNumber;
     private ZLive zLive = new ZLive();

    public ThreadTest(int threadNumber){
        this.threadNumber = threadNumber;
    }

    public void run(){
        try{
             TextUI textUI = new TextUI(zLive, new PrintWriter(System.out,
true));

            String string = "0 \\in \\dom \\{ ( 1 , \\negate 1 ) , ( 2 ,
\\negate 1 ) \\} \\land 1 > 0 \\land 1";
            string += " \\leq \\{ ( 1 , \\negate 1 ) , ( 2 , \\negate 1 )
\\} 1 \\land";
            string += "\\{ ( 1 , \\negate 1 ) , ( 2 , \\negate 1 ) \\} 0 >
10000";


            Pred pred = (Pred) textUI.parseTerm(string, new
PrintWriter(System.out, true));
            List<? extends ErrorAnn> errors =
                TypeCheckUtils.typecheck(pred, zLive.getSectionManager(),
false, zLive.getCurrentSection());
             if(errors.size() >0)
                return;

            for(int i=0; i<500; i++){
                System.out.println("Thread: " + threadNumber + " Iteración:
" + i) ;
                zLive.evalPred(pred);
            }

        }
        catch(Exception e){
            e.printStackTrace();
        }
    }
}

//**************************************************






In most executions, after printing a number of lines the JVM crashes and the
error report is:


#
# An unexpected error has been detected by Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x06302f07, pid=7736, tid=3047447440
#
# Java VM: Java HotSpot(TM) Client VM (1.6.0_03-b05 mixed mode, sharing)
# Problematic frame:
# V  [libjvm.so+0x302f07]
#
# An error report file with more information is saved as hs_err_pid7736.log
#
# If you would like to submit a bug report, please visit:
#   http://java.sun.com/webapps/bugreport/crash.jsp
#
Cancelado (core dumped)


I have attached hs_err_pid7736.log.


I believe it could be a JVM bug. What do you think?


Cheers,

Pablo

Re: [CZT-Users] Problem typechecking OZ

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

Hi Stefan,

You wrote:
> To reproduce my problem here a little spec:
> 
> \begin{class}{Element}
> \end{class}
> 
> \begin{class}{SElement}
> Element
> \end{class}
> 
> \begin{class}{List}
> \begin{state}
>  head : Element\\
>  tail : \power Element\\
> \end{state}
> \end{class}
> 
> The type checker returns
> 
> Type mismatch in membership predicate
>    Predicate: head \in SElement
>    LHS type: Element
>    RHS type: \power SElement
> 
> Is this a problem with the type checker in OZ or
> how can I define that the head of a SList is always a SElement?
> Thanks in advance?
> 
This is the correct behaviour, because head is in the class SElement, 
not in class Element. To declare head as an SElement, you can just use 
head : SElement, however, it is important that you understand the 
different between the Object-Z type system, and that of other 
object-oriented languages.

In your case, head \in SElement is not type-correct because the classes 
SElement and Element define disjoint sets of objects -- that is, an 
object cannot be of type SElement and Element. To declare that head is 
in either SElement OR Element, you can use class union

   head : SElement \classuni Element

which defines the union of all objects in SElement with all objects in 
Element.

Or better yet, use polymorphism:

   head : \poly Element

The above says that head is in the class Element *or any of Element's 
subclasses*. I think this is the semantics that you were intending.

Hope this helps,
Tim

[CZT-Users] Problem typechecking OZ

[Stefan N. <Ste...@df...>]

Hi

I am a beginner in Z/OZ.
I used the czt eclipse plugin to write some Object-Z specification in
latex.
But it seems the typechecker for OZ has some problems with subclasses.

To reproduce my problem here a little spec:

\begin{class}{Element}
\end{class}

\begin{class}{SElement}
Element
\end{class}

\begin{class}{List}
\begin{state}
 head : Element\\
 tail : \power Element\\
\end{state}
\end{class}

\begin{class}{SList}
List
\begin{state}
\where
 head \in SElement\\
\end{state}
\end{class}

The type checker returns

Type mismatch in membership predicate
   Predicate: head \in SElement
   LHS type: Element
   RHS type: \power SElement

Is this a problem with the type checker in OZ or
how can I define that the head of a SList is always a SElement?
Thanks in advance?

best regards
stefan

Re: [CZT-Users] Removing printing warnings

[Petra M. <Pet...@mc...>]

Hi Pablo,

> I believe I do have to create a new SectionManager where I could
> transfer all the information. The example I gave was a simplified
> version of my problem. Actually, I don't have the information I want to
> print contained in a .tex file.
> 
> Assume that you have a method that takes an AxPara object and returns a
> different AxPara object, while preserving the original one. Then, the
> new AxPara object is not linked from any Spec object and then, from any
> SectionManager.  Could a solution be adding the new AxPara object to the
> ZParaList where the original AxPara object is contained so I can follow
> the way you suggested?

Dealing with transformed specifications or even parts of specifications
in the section manager is a bit tricky and I can't give you a nice
general answer.  The problem with your current approach is that you take
the transformed AxPara out of its context.  This works fine as long as
it does not contain user defined operators.  If there are user defined
operators in it, the precedence of these operators is needed when the
term is printed (brackets may be required in some places).

If you don't change anything about the user defined operators, you might
copy the operator table (class OpTable) to the new section manager, too
(just ask the old section manager for the Key(specName, OpTable.class)).
There is a similar problem regarding the latex markup table (class
LatexMarkupFunction).  This information is used when you try to print
funny latex characters (like the one for \fun).  In the AST, there is
only the Unicode character but when you want to print it in LaTeX you
have to define a latex command first (like %%Zinchar \fun U+2192).  It
is best to reuse existing definitions, that is, use \fun whenever the
Unicode character 2192 needs printing.  Again, you might just copy the
latex markup table into the new section manager, or try to create an
empty one to get rid of the warning.

The other option is the one you mentioned above but it sounds ugly too.
 You probably can just add the new AxPara to the ZParaList but then you
change the original specification and you might get into trouble later.
 Is this changed specification still typecheckable, for example?

I'd suggest try copying OpTable and LatexMarkupFunction (if it exists)
to the new section manager and see how it goes.

Cheers,
Petra

Re: [CZT-Users] Removing printing warnings

[Petra M. <Pet...@mc...>]

Hi Pablo,

If you want to print in LaTeX markup, you not only need the AST but the
operator table, for example, too.  You could use the original section
manager (that contains all that information) to get the latex
        FileSource source = new FileSource("bbook.tex");
	String name = source.getName();
        SectionManager manager = new SectionManager();
        manager.put(new Key(name, Source.class), source);
	LatexString latex = (LatexString) manager.get(new Key(name,
LatexString.class));
rather than creating a new one and transfering the data from one to the
other.

Petra


Pablo Rodriguez Monetti wrote:
> Hi czt'ers! I would like to transform  Java AST objects into a .tex
> file, so I make some attempts (using the release 1.0 of czt) with a
> program similar to the following:
> 
> 
> //
> *****************************************************************************************************************
> import net.sourceforge.czt.print.util.LatexString;
> import net.sourceforge.czt.session.*;
> import net.sourceforge.czt.z.ast.*;
> import net.sourceforge.czt.z.impl.*;
> import net.sourceforge.czt.base.ast.*;
> import net.sourceforge.czt.base.ast.Term;
> import net.sourceforge.czt.util.ReflectionUtils;
> import java.io.*;
> 
> public class TexPrinting{
> 
>     public static void main(String[] args) {
>         FileSource source = new FileSource("bbook.tex");
>         SectionManager manager = new SectionManager();
>         manager.put(new Key(source.getName(), Source.class), source);
>         try{
>             Spec spec = (Spec) manager.get(new Key(source.getName(),
> Spec.class));
>             manager = new SectionManager();
>             manager.put(new Key("bbook", Spec.class), spec);
>             LatexString latex = (LatexString) manager.get(new
> Key("bbook", LatexString.class));
>             System.out.println(latex);
>         }
>         catch(Exception e){
>             System.out.println (e);
>         }
>     }
> 
> }
> //
> *****************************************************************************************************************
> 
> 
> 
> The results were correct (so quite useful for the tool  I am developing)
> but it also prints the following warning messages:
> 
> 11/03/2008 15:10:25 net.sourceforge.czt.parser.util.WarningManager warn
> ADVERTENCIA: Cannot get operator table for Specification; try to print
> anyway ...
> 11/03/2008 15:10:25
> net.sourceforge.czt.print.z.CUP$Unicode2Latex$actions setupMarkupTable
> ADVERTENCIA: Cannot get latex markup for section Specification caused by
> net.sourceforge.czt.session.SourceLocator$SourceLocatorException: Cannot
> find source location for section Specification
> 
> 
> I was trying to modify my local version of czt in order to avoid the
> printing of these warnings but the attempt was not successfull. Any
> suggestions? Which (source?) files I should modify?
> 
> Thanks,
> 
> Pablo
> 
> 
> ------------------------------------------------------------------------
> 
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users

[CZT-Users] Removing printing warnings

[Pablo R. M. <rod...@gm...>]

Hi czt'ers! I would like to transform  Java AST objects into a .tex file, so
I make some attempts (using the release 1.0 of czt) with a program similar
to the following:


//
*****************************************************************************************************************
import net.sourceforge.czt.print.util.LatexString;
import net.sourceforge.czt.session.*;
import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.z.impl.*;
import net.sourceforge.czt.base.ast.*;
import net.sourceforge.czt.base.ast.Term;
import net.sourceforge.czt.util.ReflectionUtils;
import java.io.*;

public class TexPrinting{

    public static void main(String[] args) {
        FileSource source = new FileSource("bbook.tex");
        SectionManager manager = new SectionManager();
        manager.put(new Key(source.getName(), Source.class), source);
        try{
            Spec spec = (Spec) manager.get(new Key(source.getName(),
Spec.class));
            manager = new SectionManager();
            manager.put(new Key("bbook", Spec.class), spec);
            LatexString latex = (LatexString) manager.get(new Key("bbook",
LatexString.class));
            System.out.println(latex);
        }
        catch(Exception e){
            System.out.println (e);
        }
    }

}
//
*****************************************************************************************************************



The results were correct (so quite useful for the tool  I am developing) but
it also prints the following warning messages:

11/03/2008 15:10:25 net.sourceforge.czt.parser.util.WarningManager warn
ADVERTENCIA: Cannot get operator table for Specification; try to print
anyway ...
11/03/2008 15:10:25
net.sourceforge.czt.print.z.CUP$Unicode2Latex$actionssetupMarkupTable
ADVERTENCIA: Cannot get latex markup for section Specification caused by
net.sourceforge.czt.session.SourceLocator$SourceLocatorException: Cannot
find source location for section Specification


I was trying to modify my local version of czt in order to avoid the
printing of these warnings but the attempt was not successfull. Any
suggestions? Which (source?) files I should modify?

Thanks,

Pablo

Re: [CZT-Users] Needs help in parsing

[Petra M. <Pet...@mc...>]

Hi,

I think the best way to get help is by reading source code and asking
questions on this mailing list; there isn't much up-to-date
documentation or tutorial material around.
To get a helpful answer, you should be as specific about your problem as
possible.  Include, for example, information about which version you are
using, give example code snippets, etc.

Hope this helps,
Petra

Re: [CZT-Users] Needs help in parsing

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

Hi,

I'm not quite sure I understand, but I think you just want to know how 
to parse a ZML file into an AST?

The class you want is called net.sourceforge.czt.parser.z.ParseUtils.
There is an example of parsing a latex file using ParseUtils on the wiki:

http://czt.wiki.sourceforge.net/Using+the+Z+parser+and+typechecker

If I recall correctly, parsing a ZML file is much the same. You just 
have to give you file the extension .zml

Cheers,
Tim

Abbas Wali wrote:
> Dear Members,
> hope all doing well. we are students from university of sheffield, UK. 
> we are doing a group project about developing a XML based SAL translator 
> using CZT parser. we need a bit of your help in parsing ZML 
> specification. can we get some help via some kind of tutorial or any 
> other documentation. we have gone through the API documentation but its 
> not that clear there.
> it would be wonderful if some one can give us a hand.
> thanks alot
> will be waiting for your reply.
> Darwin Group,
> University of Sheffield
> United Kingdom
> 
> 
> ------------------------------------------------------------------------
> 
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users