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

[CZT-Users] Needs help in parsing

[Abbas W. <ac...@sh...>]

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

Re: [CZT-Users] Problems with certain characters in jEdit

[Petra M. <pe...@cs...>]

Tim Miller wrote:
> Petra, the set_toolkit section defines set minus as the unicode 
> character 005C, while the ZTable in the zcharmap plugin defines it 
> as 2216. The version of the standard that I have specifies it as 
> 005C, but I'm not sure whether my version is still up to date. Any 
> clues?

It got changed from 005C to 2216 in the Technical Corrigenda for Defect
Reports 13568/001..013 (December 2006) so I'd expect CZT to use 2216.
I thought I'd chanaged all characters to the new ones but I must have
missed set minus somehow.  Anyway, it should be fixed now (in the SVN
repository).

Thanks for finding and report this bug, Nelis.

Petra

Re: [CZT-Users] Problems with certain characters in jEdit

[Tim M. <T.M...@li...>]

nelis wrote:
> Hello,
>=20
> I'm continuing my efforts in using Z, and thanks to Tim I've made great=
=20
> progress. But I still run into problems (in Unicode markup):
>=20
> - the 'section' concept is not accepted by the parser, it gives a synta=
x=20
> error on the first character.
> ? section NAME parents standard_toolkit ?
>=20
Can you post the full example, including the error message? This=20
works fine for me.

> - the set substraction does not work when choosing it from the ZCharMap=
=20
> (with some strange error saying "Application of a non-function=20
> Expression: Cannot be printed ..."), but it seems to work if I use a=20
> normal backslash. Does it mean the same thing?
>=20
Yes, they mean the same thing, but you have discovered a bug!

Petra, the set_toolkit section defines set minus as the unicode=20
character 005C, while the ZTable in the zcharmap plugin defines it=20
as 2216. The version of the standard that I have specifies it as=20
005C, but I'm not sure whether my version is still up to date. Any=20
clues?

Cheers,
Tim

[CZT-Users] Problems with certain characters in jEdit

[nelis <nel...@cs...>]

Hello,

I'm continuing my efforts in using Z, and thanks to Tim I've made great 
progress. But I still run into problems (in Unicode markup):

- the 'section' concept is not accepted by the parser, it gives a syntax 
error on the first character.
? section NAME parents standard_toolkit ?

- the set substraction does not work when choosing it from the ZCharMap 
(with some strange error saying "Application of a non-function 
Expression: Cannot be printed ..."), but it seems to work if I use a 
normal backslash. Does it mean the same thing?

Kind regards,
Nelis

Re: [CZT-Users] Typechecker: cyclic definition of schema's

[Tim M. <T.M...@li...>]

Petra Malik wrote:
> Tim Miller wrote:
>> do you object to me adding this to the options in the zsidekick?
> 
> No, not at all.  Please go ahead and add this option.
> 
Done! It was much more straightforward than I thought it would be too.

Nelis, if you are building CZT from the SVN repository on 
sourceforge, you should be able update your local copy and use 
this new option. If not, email me (not the mailing list) and I'll 
send you the updated plugin.

Cheers,
Tim

Re: [CZT-Users] Typechecker: cyclic definition of schema's

[Petra M. <pe...@cs...>]

Tim Miller wrote:
> I had a quick look at the code, and I can't figure out 
> where this property is set.

Setting this property in jEdit is not yet supported.

> do you object to me adding this to the options in the zsidekick?

No, not at all.  Please go ahead and add this option.

Cheers,
Petra

Re: [CZT-Users] Typechecker: cyclic definition of schema's

[Tim M. <T.M...@li...>]

nelis wrote:
> Thank you for your quick answer. Alas this does not seem to work. I 
> changed the extension of the file, and it still refuses to accept this 
> definition. I think JEdit is correctly using the Object-z parser (since 
> it mentions the parser in the status bar when it is finished).
> 
I've just installed the jEdit plugin, and you are right: it is 
using the Object-Z parser, but use before declaration is not 
enabled. I had a quick look at the code, and I can't figure out 
where this property is set.

Petra, are you able to help with this? Also, if this property is 
not able to be changed via the interface, do you object to me 
adding this to the options in the zsidekick?

> Questions:
> 2. Are there constructs that only exist in Object-z so that I can test 
> that it effectively uses the Object-z parser?

I think you are using the Object-Z tools, but try the following 
specification:

\begin{class}{C}
\end{class}

\begin{zed}
   D == C
\end{zed}

The Object-Z typechecker will allow this, but the Z typechecker 
will raise an error that the name "C" is undeclared.

> 3. If you don't use this JEdit plugin, how do you specify your Z 
> documents in a practical way?
> 
I use a text editor and then typecheck the specification on the 
command line (in unix):

java -jar czt.jar zedtypecheck filename.tex

If you want to enable use before declaration, use the -d flag, 
like so:

java -jar czt.jar zedtypecheck -d filename.tex

The above reports no errors for your example.

The other option is to use the CZT plugin for Eclipse 
(http://www.cs.waikato.ac.nz/~marku/czt/eclipse.html), but I'm not 
sure whether that will solve your use before declaration problem.

Cheers,
Tim

Re: [CZT-Users] Typechecker: cyclic definition of schema's

[nelis <nel...@cs...>]

Tim Miller schreef:
> nelis wrote:
>   
>> I want to define something like:
>>
>> \begin{schema}{SUBSTRUCTURE}\\
>>  components : \power COMPONENT \\
>>  connectors : \power CONNECTORS \\
>>  links : \power LINKS \\
>>  interfaceMappings : \power INTERFACEMAPPING
>> \end{schema}
>>
>> \begin{schema}{COMPONENT}\\
>>  identifier : IDENTIFIER \\
>>  description : TEXT \\
>>  interfaces : \power INTERFACE \\
>>  subStructure : SUBSTRUCTURE
>> \end{schema}
>>
>> But I get the follow problem: the typechecker seems unable to handle a 
>> schema definition that relies on a schema that is specified further in 
>> the document. Like in the example, Substructure can not rely on the 
>> definition of component.
>>
>>     
> Just as a note, the above is not permitted by Z. The scope of the
> schema SUBSTRUCTURE is restricted only to the paragraphs that have
> been declared before it; that is, Z does not permit use before
> declaration, except in the special case of recursive given types.
>
> However! ... I have implemented the CZT typechecker such that it
> allows users to turn on use before declaration. I'm not sure how
> to turn this on from the jedit plugin (I don't use that particular
> plugin -- someone else on the project may be able to answer that),
> but for now, the easiest way is if you change the file extension
> of your specifications to .oz (e.g. from file.tex to file.oz).
> Then the jedit plugin will automatically use the Object-Z
> typechecker, which has use before declaration enabled by default,
> and the above should then typecheck without problems.
>
> Cheers,
> Tim
>
>
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Splunk Inc.
> Still grepping through log files to find problems?  Stop.
> Now Search log events and configuration files using AJAX and a browser.
> Download your FREE copy of Splunk now >> http://get.splunk.com/
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users
>   
Dear Tim,

Thank you for your quick answer. Alas this does not seem to work. I 
changed the extension of the file, and it still refuses to accept this 
definition. I think JEdit is correctly using the Object-z parser (since 
it mentions the parser in the status bar when it is finished).

Questions:
1. Is there anybody with experience in JEdit who could help me getting 
it to work?
2. Are there constructs that only exist in Object-z so that I can test 
that it effectively uses the Object-z parser?
3. If you don't use this JEdit plugin, how do you specify your Z 
documents in a practical way?

Kind regards,
Nelis

Re: [CZT-Users] Typechecker: cyclic definition of schema's

[Tim M. <T.M...@li...>]

nelis wrote:
> I want to define something like:
> 
> \begin{schema}{SUBSTRUCTURE}\\
>  components : \power COMPONENT \\
>  connectors : \power CONNECTORS \\
>  links : \power LINKS \\
>  interfaceMappings : \power INTERFACEMAPPING
> \end{schema}
> 
> \begin{schema}{COMPONENT}\\
>  identifier : IDENTIFIER \\
>  description : TEXT \\
>  interfaces : \power INTERFACE \\
>  subStructure : SUBSTRUCTURE
> \end{schema}
> 
> But I get the follow problem: the typechecker seems unable to handle a 
> schema definition that relies on a schema that is specified further in 
> the document. Like in the example, Substructure can not rely on the 
> definition of component.
> 
Just as a note, the above is not permitted by Z. The scope of the
schema SUBSTRUCTURE is restricted only to the paragraphs that have
been declared before it; that is, Z does not permit use before
declaration, except in the special case of recursive given types.

However! ... I have implemented the CZT typechecker such that it
allows users to turn on use before declaration. I'm not sure how
to turn this on from the jedit plugin (I don't use that particular
plugin -- someone else on the project may be able to answer that),
but for now, the easiest way is if you change the file extension
of your specifications to .oz (e.g. from file.tex to file.oz).
Then the jedit plugin will automatically use the Object-Z
typechecker, which has use before declaration enabled by default,
and the above should then typecheck without problems.

Cheers,
Tim

Re: [CZT-Users] Example specifications

[Tim M. <T.M...@li...>]

There are quite a few examples available in the ZML subproject of
CZT. You can access these by using SVN to download the 'zml'
subfolder, or you can browse and download them via sourceforge:
http://czt.svn.sourceforge.net/viewvc/czt/trunk/zml/src/main/resources/net/sourceforge/czt/zml/examples/

The Object-Z and Circus examples accessible from the above link
may be of some use as well.

Cheers,
Tim

nelis wrote:
> Dear CZT developers,
> 
> I'm now using the JEdit plug-in to produce a Z specification for a few 
> weeks, but it is not always easy to find your way with so few 
> documentation and examples. I'm wondering if you could provide more 
> examples through the website of z specifications, possibly annotated 
> with some explanation? Some of you must have other examples then the 
> BirthdayDay example.
> 
> Kind regards,
> Nelis
> 
> 
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Splunk Inc.
> Still grepping through log files to find problems?  Stop.
> Now Search log events and configuration files using AJAX and a browser.
> Download your FREE copy of Splunk now >> http://get.splunk.com/
> _______________________________________________
> CZT-Users mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-users

[CZT-Users] Example specifications

[nelis <nel...@cs...>]

Dear CZT developers,

I'm now using the JEdit plug-in to produce a Z specification for a few 
weeks, but it is not always easy to find your way with so few 
documentation and examples. I'm wondering if you could provide more 
examples through the website of z specifications, possibly annotated 
with some explanation? Some of you must have other examples then the 
BirthdayDay example.

Kind regards,
Nelis

[CZT-Users] Typechecker: cyclic definition of schema's

[nelis <nel...@cs...>]

Dear,

I want to define something like:

\begin{schema}{SUBSTRUCTURE}\\
 components : \power COMPONENT \\
 connectors : \power CONNECTORS \\
 links : \power LINKS \\
 interfaceMappings : \power INTERFACEMAPPING
\end{schema}

\begin{schema}{COMPONENT}\\
 identifier : IDENTIFIER \\
 description : TEXT \\
 interfaces : \power INTERFACE \\
 subStructure : SUBSTRUCTURE
\end{schema}

But I get the follow problem: the typechecker seems unable to handle a 
schema definition that relies on a schema that is specified further in 
the document. Like in the example, Substructure can not rely on the 
definition of component.

At first sight this might seem as a minor constraint, but for my formal 
specification I fast run into problems. For example, a component can 
have a substructure that exists of components and connectors. Thus I 
need to define substructure in terms of components, and a component in 
terms of a substructure. Why does the typechecker not support such 
cases? As far as I understood, schema's are independent 'entities' in 
the Z description, so I would expect this to be possible. Does anyone 
have suggestions on how to circumvent this problem?

Kind regards,
Nelis

Re: [CZT-Users] Help with getting started II

[<pe...@cs...>]

Hi Pablo,

> When I tryed to load the following specification, I
> received parsing errors related to the /defs latex command.

CZT implements ISO standard Z, which doesn't use "/defs"; please use "=="
instead.

> Then, I tried with the following, and I received typechecking errors that
> undoubtely are related to the InitBirthdayBook schema.
> [...]
> \begin{schema}{InitBirthdayBook}
>     BirthdayBook '
> \where

The decoration on the BirthdayBook reference must be separated from the
schema name.  It is not sufficient to just have a space there, you need to
have a hard space: "BirthdayBook~".

See also http://www-users.cs.york.ac.uk/~ian/cadiz/standard.html for a
list of differences between ISO Z and Spivey's Z Reference Manual.

Hope that helps,
Petra

[CZT-Users] Help with getting started II

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

Hi czt'ers,
I'm interested in exploit the power of zlive but I had problems trying to
load some .zed files.  When I tryed to load the following specification, I
received parsing errors related to the /defs latex command.

\documentclass{article}
\usepackage{oz}   % oz or z-eves or fuzz styles
\newenvironment{machine}[1]{
    \begin{tabular}{@{\qquad}l}\textbf{\kern-1em machine}\ #1\\ }{
    \\ \textbf{\kern-1em end} \end{tabular} }


\begin{document}

\begin{zed}
%    [NAME, DATE]
   NAME == 1 \upto 5
\end{zed}
\begin{zed}
   DATE == 10 \upto 15
\end{zed}


\begin{schema}{BirthdayBook}
    known: \power NAME \\
    birthday: NAME \pfun DATE
\where
    known=\dom birthday
\end{schema}

\begin{schema}{InitBirthdayBook}
    BirthdayBook '
\where
    known' = \{ \}
\end{schema}

\begin{schema}{AddBirthday}
    \Delta BirthdayBook \\
    name?: NAME \\
    date?: DATE
\where
    name? \notin known
\\
    birthday' = birthday \cup \{name? \mapsto date?\}
\end{schema}

\begin{schema}{FindBirthday}
    \Xi BirthdayBook \\
    name?: NAME \\
    date!: DATE
\where
    name? \in known
\\
    date! = birthday(name?)
\end{schema}

\begin{schema}{Remind}
    \Xi BirthdayBook \\
    today?: DATE \\
    cards!: \power NAME
\where
    cards! = \{ n: known | birthday(n) = today? \}
\end{schema}

\begin{schema}{RemindOne}
    \Xi BirthdayBook \\
    today?: DATE \\
    card!: NAME
\where
    card! \in known \\
    birthday ~ card! = today?
\end{schema}


\begin{zed}
    REPORT ::= ok | already\_known | not\_known
\end{zed}

\begin{schema}{Success}
    result!: REPORT
\where
    result! = ok
\end{schema}

\begin{schema}{AlreadyKnown}
    \Xi BirthdayBook \\
    name?: NAME \\
    result!: REPORT
\where
    name? \in known \\
    result! = already\_known
\end{schema}


\begin{schema}{NotKnown}
    \Xi BirthdayBook \\
    name?: NAME \\
    result!: REPORT
\where
    name? \notin known \\
    result! = not\_known
\end{schema}

\begin{zed}
    RAddBirthday \defs (AddBirthday \land Success) \lor AlreadyKnown \\
    RFindBirthday \defs (FindBirthday \land Success) \lor NotKnown \\
    RRemind \defs Remind \land Success
\end{zed}


\end{document}




Then, I tried with the following, and I received typechecking errors that
undoubtely are related to the InitBirthdayBook schema.



\documentclass{article}
\usepackage{oz}   % oz or z-eves or fuzz styles
\newenvironment{machine}[1]{
    \begin{tabular}{@{\qquad}l}\textbf{\kern-1em machine}\ #1\\ }{
    \\ \textbf{\kern-1em end} \end{tabular} }


\begin{document}

\begin{zed}
%    [NAME, DATE]
   NAME == 1 \upto 5
\end{zed}
\begin{zed}
   DATE == 10 \upto 15
\end{zed}


\begin{schema}{BirthdayBook}
    known: \power NAME \\
    birthday: NAME \pfun DATE
\where
    known=\dom birthday
\end{schema}


\begin{schema}{InitBirthdayBook}
    BirthdayBook '
\where
    known' = \{ \}
\end{schema}

\end{document}


Any help??
Thanks,
Pablo

[CZT-Users] CZT typechecker v1.0 release

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

CZT-ers,

In keeping up with the tradition of releasing standalone jar files 
for the Z/Object-Z typechecker (which seem to be quite popular), I 
have released a new version to coincide with the recent CZT 1.0 
release.

For those unfamiliar with these releases, they are lighter 
versions of the CZT tools, containing only the parsers and 
typecheckers for Z/Object-Z, and are used via the command line. 
The new version can be run the same as previous versions:
java -jar czt_typecheck_v1.0.jar filename1 filename2 ...

You can download it from the CZT sourceforge site, or directly via 
the link 
http://prdownloads.sourceforge.net/czt/czt_typecheck_v1.0.jar?download

Cheers,
Tim

[CZT-Users] First stable CZT relase v.1.0 !!!

[<le...@cs...>]

Dear CZT User/Developer,

We delighted to announce that after a lot of effort,
our first stable realease v.1.0 is now available at
"http://czt.sourceforge.net". This includes tools for
Z, Object-Z, and Circus, such as parser, typechecker,
pretty-printer, developing environments like jEdit and
Eclipse, a Z animator (ZLive), and so on.
They have been thoroughly used and tested within our
developping team. Nevertheless, there is plenty of room
for improvement!
Thus, we would be greatful if you could send us your
views, comments, bugs, suggestion, feature requests,
and so on at "http://sourceforge.net/projects/czt/".

With best regards,
CZT development team

[CZT-Users] CZT session at ZUM07

[Mark U. <ma...@cs...>]

Dear CZT users,

There will be a special session on CZT at the 2007 Z User Meeting.

See http://www.cs.waikato.ac.nz/~stever/ZUM07.html

I would encourage you to submit Z papers to ZUM07, including papers that 
deal with the use of the CZT tools.  Note that there is a new 
Eclipse/CZT beta release available now

(see http://www.cs.waikato.ac.nz/~marku/czt/eclipse.html )

and a new binary release of CZT 1.0 (the command line and jEdit 
interfaces) will be available in a few weeks.

Happy Z'ing...
Mark

Dr Mark Utting, Associate Professor, Dept. of Computer Science,
The University of Waikato, Private Bag 3105, Hamilton, New Zealand.
Phone: +64 7 838 4791     Web:   http://www.cs.waikato.ac.nz/~marku
Fax:   +64 7 858 5095     Email: ma...@cs...

Re: [CZT-Users] [CZT-Devel] New CZT wiki page

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

Mark Utting wrote:
> Good.  This seems to work nicely, though I had a few glitches.
> 
> 1. It seems that you have to create a new (and insecure! -- don't use 
> your sourceforge password) Wiki account -- it does not use your 
> Sourceforge login -- no problem.
> 
Yes, it isn't linked to sourceforge at all... it's just installed 
in the htdocs of the sourceforge account. You don't need an 
account to edit the pages, but perhaps it may be useful if we all 
use accounts when we edit though, so we know who is making the 
changes?

> 2. After creating a new account I had to log in and out a couple of 
> times before I could edit the page as me.
> 
> 3. When I saved the page, it gave an error (something about the server 
> losing information), but allowed me to try again, and it worked the 
> second time.
> 
Hmmm... that's not good. I didn't have either of these problems 
though, so hopefully this was just a problem with connections or 
something.

> So the big question: what content will be useful for us all?
> * A summary of the status of each tool/project?
> * A summary of what we are each working on?
> * A HowTo/FAQ section?
> * A RoadMap for the future?
> 
Yes, all this should go on there. I think it would be nice if we 
had user-guides for many of the sub-projects (e.g. parser, 
typechecker, rules, zlive), with example code. This way, users may 
be encouraged to add their own solutions/code. An installation 
guide should also be on there, as well as links to downloading 
etc. Really, anything that users can contribute to.

Tim

Re: [CZT-Users] [CZT-Devel] New CZT wiki page

[Mark U. <ma...@cs...>]

Tim Miller wrote:
> Hi everyone,
>
> After some messing about, I've (finally!) gotten around to 
> creating a wiki page for CZT:
>
> http://czt.sourceforge.net/wiki
>
> At the moment, there's nothing on there, but feel free to create 
> articles and write anything that you may feel is useful to both 
> the developers, and to users.
>   

Good.  This seems to work nicely, though I had a few glitches.

1. It seems that you have to create a new (and insecure! -- don't use 
your sourceforge password) Wiki account -- it does not use your 
Sourceforge login -- no problem.

2. After creating a new account I had to log in and out a couple of 
times before I could edit the page as me.

3. When I saved the page, it gave an error (something about the server 
losing information), but allowed me to try again, and it worked the 
second time.

But after these teething problems, it works very well.

So the big question: what content will be useful for us all? 

* A summary of the status of each tool/project?
* A summary of what we are each working on?
* A HowTo/FAQ section?
* A RoadMap for the future?

Mark

[CZT-Users] New CZT wiki page

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

Hi everyone,

After some messing about, I've (finally!) gotten around to 
creating a wiki page for CZT:

http://czt.sourceforge.net/wiki

At the moment, there's nothing on there, but feel free to create 
articles and write anything that you may feel is useful to both 
the developers, and to users.

Cheers,
Tim

[CZT-Users] ICECCS 2007 - Paper Submission Extended to Jan. 31st

[Jing S. <j....@cs...>]

Due to many requests, the deadline for the ICECCS07 paper submission has =
been
extended to January 31st, 2007. Please help us to further advertise this
extension.

-----------------------------------------------------------------------
We apologize if you've received multiple copies of the following message.
-----------------------------------------------------------------------

CALL FOR PAPERS

The Twelfth IEEE International Conference on Engineering of Complex Compu=
ter
Systems (ICECCS 2007)

The University of Auckland, New Zealand, 11-14 July 2007

http://www.cs.auckland.ac.nz/iceccs07/

-----------------------------------------------------------------------
Complex computer systems are common in many sectors, such as
manufacturing, communications, defense, transportation, aerospace,
hazardous environments, energy, and health care. These systems are
frequently distributed over heterogeneous networks, and are driven by
many diverse requirements on performance, real-time behavior, fault
tolerance, security, adaptability, development time and cost, long life
concerns, and other areas. Such requirements frequently conflict, and
their satisfaction therefore requires managing the trade-off among them
during system development and throughout the entire system life.

The goal of this conference is to bring together industrial, academic,
and government experts, from a variety of user domains and software
disciplines, to determine how the disciplines' problems and solution
techniques interact within the whole system. Researchers,
practitioners, tool developers and users, and technology transition
experts are all welcome. The scope of interest includes long-term
research issues, near-term complex system requirements and promising
tools, existing complex systems, and commercially available tools.
-----------------------------------------------------------------------

SCOPE AND TOPICS
-----------------------------------------------------------------------
Papers are solicited in all areas related to complex computer-based
systems, including the causes of complexity and means of avoiding,
controlling, or coping with complexity. Topic areas include, but are
not limited to:

+ Avionics and Automobile Software
+ Content Production and Distribution Systems, Mobile and Multi-channel S=
ystems
+ Context Awareness Computing
+ Formal Methods and Approaches to Manage and Control Complex Systems
+ Human Factors and Collaborative Aspects
+ Integration of Heterogeneous Technologies
+ Interoperability and Standardization
+ Pervasive and Ubiquitous Computing
+ Real-time and Embedded Systems
+ Sensor Network Systems and Applications
+ Software and System Development and Control Processes for Complex Syste=
ms
+ Software Architecture and System Engineering
+ Software Complexity Visualization
+ Systems and Software Safety and Security
+ Tools, Environments, and Languages for Complex Systems
+ Verification Techniques for Complex Software Systems
+ Virtual Environments for Managing Complexity
+ Web Services Modeling and Compositions

Different kinds of contributions are sought, including research papers,
lessons learned, status reports, and discussion of practical problems
faced by industry and user domains. The ultimate goal is to build a
rich and comprehensive conference program that can fit the interests
and needs of different classes of attendees: professionals,
researchers, managers, and students. A program goal is to organize
several sessions that include both academic and industrial papers on a
given topic and culminate panels to discuss relationships between
industrial and academic research.

Papers are divided into two categories: Technical Papers and Experience
Reports. The papers submitted to both categories will be reviewed by
program committee members, and papers accepted in either category will
be published in the conference proceedings. Technical papers should
describe original research, and industrial experience reports should
describe practical projects carried out in industry, and reflect on the
lessons learnt from them.
-----------------------------------------------------------------------

PAPER SUBMISSION
-----------------------------------------------------------------------
Submitted manuscripts should be in English and formatted in the style
of the IEEE Computer Society Proceedings Format. Papers should not
exceed 10 pages including figures, references, and appendices and be in
PDF format. Submissions of papers will be carried out electronically
via the Web (Submission Page). Authors of accepted papers will be
required to sign a copyright release form. IEEE Computer Society Press
will publish the proceedings. Final versions of accepted papers will be
limited to 10 pages in the aforementioned IEEE proceedings format.
-----------------------------------------------------------------------

WORKSHOP PROPOSAL SUBMISSION
-----------------------------------------------------------------------
If you are interested in proposing Workshops, please contact Steve Reeves
<st...@cs...>. There will also be a Special Session on Grand
Challenges --- Complex Program Verifier. If you are interested in this,
please contact Jim Woodcock <Jim...@cs...>.
-----------------------------------------------------------------------

IMPORTANT DATES
-----------------------------------------------------------------------
Paper submission: January 31, 2007
Workshop proposal submission: February 20, 2007
Notification of acceptance: March 9, 2007
Camera ready copy due: April 8, 2007
-----------------------------------------------------------------------

KEYNOTE SPEAKERS
-----------------------------------------------------------------------
Jim Woodcock, University of York, United Kingdom
Wolfram Schulte, Microsoft Research, USA
Paul Strooper, The University of Queensland, Australia
-----------------------------------------------------------------------

CONFERENCE ORGANIZERS
-----------------------------------------------------------------------
GENERAL CHAIRS
Michael G Hinchey, Loyola College in Maryland, USA
Gillian Dobbie, The University of Auckland, New Zealand

PROGRAM CHAIRS
Jin Song Dong, National University of Singapore, Singapore
Jing Sun, The University of Auckland, New Zealand

WORKSHOP CHAIR
Steve Reeves, The University of Waikato, New Zealand

SPECIAL SESSION CHAIR
Jim Woodcock, Special Session Chair on Grand Challenges - Complex
Program Verifier, University of York, United Kingdom

LOCAL ORGANIZATION CHAIR
John Hamer, The University of Auckland, New Zealand

SPONSORSHIP CHAIR
Ian Warren, The University of Auckland, New Zealand

PROGRAM COMMITTEE
Timo Aaltonen, Tampere University of Technology, Finland
Yamine Ait Ameur, LISI/ENSMA, France
Robert Amor, The University of Auckland, New Zealand
Doo-Hwan Bae, Korea Advanced Institute of Science and Technology, Korea
Pierfrancesco Bellini, University of Florence, Italy
Shawn Bohner, Virginia Tech, USA
Jan Bosch, Nokia Research Center, Finland
Jonathan Bowen, Museophile Limited, United Kingdom
Manfred Broy, Technical University of Munich, Germany
Michael Butler, University of Southampton, United Kingdom
W.K. Chan, City University of Hong Kong, China
Albert M. K. Cheng, University of Houston, USA
Wei Ngan Chin, National University of Singapore, Singapore
Myra Cohen, University of Nebraska-Lincoln, USA
Jim Davies, University of Oxford, United Kingdom
Ewen Denney, RIACS / NASA Ames Research Center, USA
Jurgen Dingel, Queen's University, Canada
Jin Song Dong, National University of Singapore, Singapore
Jose Luiz Fiadeiro, University of Leicester, United Kingdom
Colin Fidge, Queensland University of Technology, Australia
Robert France, Colorado State University, USA
Yuxi Fu, Shanghai Jiaotong University, China
Chris George, United Nations University, China
Jeremy Gibbons, University of Oxford, United Kingdom
Lindsay Groves, Victoria University of Wellington, New Zealand
Volker Gruhn, University of Leipzig, Germany
Jun Han, Swinburne University of Technology, Australia
Ian Hayes, University of Queensland, Australia
Jane E. Hayes, University of Kentucky, USA
John Hosking, The University of Auckland, New Zealand
Zhenjiang Hu, University of Tokyo, Japan
Pankaj Jalote, Indian Institute of Technology Kanpur, India
Phillip Laplante, Penn State University, USA
Kung-Kiu Lau, The University of Manchester, United Kingdom
Kueng Hae Lee, Hankuk Aviation University, Korea
Xuandong Li, Nanjing University, China
Peter Lindsay, University of Queensland, Australia
Zhiming Liu, United Nations University, China
Shaoying Liu, Hosei University, Japan
Brendan Mahony, Defence Science and Technology Organisation, Australia
Andrew Martin, University of Oxford, United Kingdom
Hong Mei, Peking University, China
Huaikou Miao, Shanghai University, China
Shin Nakajima, National Instutite of Informatics, Japan
Paolo Nesi, University of Florence, Italy
Richard Paige, University of York, United Kingdom
Sungyong Park, Sogang University, Korea
Mauro Pezze, University of Lugano, Switzerland
Shengchao Qin, Durham University, United Kingdom
Zongyan Qiu, Peking University, China
Steve Reeves, The University of Waikato, New Zealand
Motoshi Saeki, Tokyo Institute of Technology, Japan
Emil Sekerinski, McMaster University, Canada
Rudolph E. Seviora, University of Waterloo, Canada
Xiaoyu Song, Portland State University, USA
Mark Staples, National ICT Australia, Australia
Frank Stomp, Wayne State University, USA
Paul Strooper, The University of Queensland, Australia
Jing Sun, The University of Auckland, New Zealand
Paul Swatman, University of South Australia, Australia
Kenji Taguchi, National Institute of Informatics, Japan
Tetsuo Tamai, The University of Tokyo, Japan
Mark Utting, The University of Waikato, New Zealand
Farn Wang, National Taiwan University, Taiwan
Hai Wang, University of Southampton, United Kingdom
Ian Warren, The University of Auckland, New Zealand
Jim Woodcock, University of York, United Kingdom
Wang Yi, Uppsala University, Sweden
Huiqun Yu, East China University of Science and Technology, China
Daqing Zhang, Institute for Infocomm Research, Singapore
Hong Zhu, Oxford Brookes University, United Kingdom

[CZT-Users] ICECCS 2007: Call for Papers

[Jing S. <j....@cs...>]

CALL FOR PAPERS

The Twelfth IEEE International Conference on Engineering of Complex Compu=
ter
Systems (ICECCS 2007)

The University of Auckland, New Zealand, 11-14 July 2007

http://www.cs.auckland.ac.nz/iceccs07/

-----------------------------------------------------------------------
Complex computer systems are common in many sectors, such as
manufacturing, communications, defense, transportation, aerospace,
hazardous environments, energy, and health care. These systems are
frequently distributed over heterogeneous networks, and are driven by
many diverse requirements on performance, real-time behavior, fault
tolerance, security, adaptability, development time and cost, long life
concerns, and other areas. Such requirements frequently conflict, and
their satisfaction therefore requires managing the trade-off among them
during system development and throughout the entire system life.

The goal of this conference is to bring together industrial, academic,
and government experts, from a variety of user domains and software
disciplines, to determine how the disciplines' problems and solution
techniques interact within the whole system. Researchers,
practitioners, tool developers and users, and technology transition
experts are all welcome. The scope of interest includes long-term
research issues, near-term complex system requirements and promising
tools, existing complex systems, and commercially available tools.
-----------------------------------------------------------------------

SCOPE AND TOPICS
-----------------------------------------------------------------------
Papers are solicited in all areas related to complex computer-based
systems, including the causes of complexity and means of avoiding,
controlling, or coping with complexity. Topic areas include, but are
not limited to:

+ Avionics and Automobile Software
+ Content Production and Distribution Systems, Mobile and Multi-channel S=
ystems
+ Context Awareness Computing
+ Formal Methods and Approaches to Manage and Control Complex Systems
+ Human Factors and Collaborative Aspects
+ Integration of Heterogeneous Technologies
+ Interoperability and Standardization
+ Pervasive and Ubiquitous Computing
+ Real-time and Embedded Systems
+ Sensor Network Systems and Applications
+ Software and System Development and Control Processes for Complex Syste=
ms
+ Software Architecture and System Engineering
+ Software Complexity Visualization
+ Systems and Software Safety and Security
+ Tools, Environments, and Languages for Complex Systems
+ Verification Techniques for Complex Software Systems
+ Virtual Environments for Managing Complexity
+ Web Services Modeling and Compositions

Different kinds of contributions are sought, including research papers,
lessons learned, status reports, and discussion of practical problems
faced by industry and user domains. The ultimate goal is to build a
rich and comprehensive conference program that can fit the interests
and needs of different classes of attendees: professionals,
researchers, managers, and students. A program goal is to organize
several sessions that include both academic and industrial papers on a
given topic and culminate panels to discuss relationships between
industrial and academic research.

Papers are divided into two categories: Technical Papers and Experience
Reports. The papers submitted to both categories will be reviewed by
program committee members, and papers accepted in either category will
be published in the conference proceedings. Technical papers should
describe original research, and industrial experience reports should
describe practical projects carried out in industry, and reflect on the
lessons learnt from them.
-----------------------------------------------------------------------

PAPER SUBMISSION
-----------------------------------------------------------------------
Submitted manuscripts should be in English and formatted in the style
of the IEEE Computer Society Proceedings Format. Papers should not
exceed 10 pages including figures, references, and appendices and be in
PDF format. Submissions of papers will be carried out electronically
via the Web (Submission Page). Authors of accepted papers will be
required to sign a copyright release form. IEEE Computer Society Press
will publish the proceedings. Final versions of accepted papers will be
limited to 10 pages in the aforementioned IEEE proceedings format.
-----------------------------------------------------------------------

WORKSHOP PROPOSAL SUBMISSION
-----------------------------------------------------------------------
If you are interested in proposing Workshops, please contact Steve Reeves
<st...@cs...>. There will also be a Special Session on Grand
Challenges --- Complex Program Verifier. If you are interested in this,
please contact Jim Woodcock <Jim...@cs...>.
-----------------------------------------------------------------------

IMPORTANT DATES
-----------------------------------------------------------------------
Abstract submission: January 5, 2007
Paper submission: January 20, 2007
Workshop proposal submission: February 20, 2007
Notification of acceptance: March 9, 2007
Camera ready copy due: April 8, 2007
-----------------------------------------------------------------------

KEYNOTE SPEAKERS
-----------------------------------------------------------------------
Jim Woodcock, University of York, United Kingdom
Wolfram Schulte, Microsoft Research, USA
Paul Strooper, The University of Queensland, Australia
-----------------------------------------------------------------------

CONFERENCE ORGANIZERS
-----------------------------------------------------------------------
GENERAL CHAIRS
Michael G Hinchey, NASA Goddard Space Flight Center, USA
Gillian Dobbie, The University of Auckland, New Zealand

PROGRAM CHAIRS
Jin Song Dong, National University of Singapore, Singapore
Jing Sun, The University of Auckland, New Zealand

WORKSHOP CHAIR
Steve Reeves, The University of Waikato, New Zealand

SPECIAL SESSION CHAIR
Jim Woodcock, Special Session Chair on Grand Challenges - Complex
Program Verifier, University of York, United Kingdom

LOCAL ORGANIZATION CHAIR
John Hamer, The University of Auckland, New Zealand

SPONSORSHIP CHAIR
Ian Warren, The University of Auckland, New Zealand

PROGRAM COMMITTEE
Timo Aaltonen, Tampere University of Technology, Finland
Robert Amor, The University of Auckland, New Zealand
Doo-Hwan Bae, Korea Advanced Institute of Science and Technology, Korea
Pierfrancesco Bellini, University of Florence, Italy
Shawn Bohner, Virginia Tech, USA
Jan Bosch, Nokia Research Center, Finland
Jonathan Bowen, Museophile Limited, United Kingdom
Manfrey Broy, Technical University of Munich, Germany
Michael Butler, University of Southampton, United Kingdom
W.K. Chan, City University of Hong Kong, China
Albert M. K. Cheng, University of Houston, USA
Wei Ngan Chin, National University of Singapore, Singapore
Myra Cohen, University of Nebraska-Lincoln, USA
Jim Davies, University of Oxford, United Kingdom
Ewen Denney, RIACS / NASA Ames Research Center, USA
Jurgen Dingel, Queen's University, Canada
Jin Song Dong, National University of Singapore, Singapore
Jose Luiz Fiadeiro, University of Leicester, United Kingdom
Colin Fidge, Queensland University of Technology, Australia
Robert France, Colorado State University, USA
Yuxi Fu, Shanghai Jiaotong University, China
Chris George, United Nations University, China
Jeremy Gibbons, University of Oxford, United Kingdom
Lindsay Groves, Victoria University of Wellington, New Zealand
Volker Gruhn, University of Leipzig, Germany
Jun Han, Swinburne University of Technology, Australia
Ian Hayes, University of Queensland, Australia
Jane E. Hayes, University of Kentucky, USA
John Hosking, The University of Auckland, New Zealand
Zhenjiang Hu, University of Tokyo, Japan
Pankaj Jalote, Indian Institute of Technology Kanpur, India
Phillip Laplante, Penn State University, USA
Kung-Kiu Lau, The University of Manchester, United Kingdom
Kueng Hae Lee, Hankuk Aviation University, Korea
Xuandong Li, Nanjing University, China
Peter Lindsay, University of Queensland, Australia
Zhiming Liu, United Nations University, China
Shaoying Liu, Hosei University, Japan
Brendan Mahony, Defence Science and Technology Organisation, Australia
Andrew Martin, University of Oxford, United Kingdom
Hong Mei, Peking University, China
Huaikou Miao, Shanghai University, China
Shin Nakajima, National Instutite of Informatics, Japan
Paolo Nesi, University of Florence, Italy
Richard Paige, University of York, United Kingdom
Sungyong Park, Sogang University, Korea
Mauro Pezze, University of Lugano, Switzerland
Shengchao Qin, Durham University, United Kingdom
Zhongyan Qiu, Peking University, China
Steve Reeves, The University of Waikato, New Zealand
Motoshi Saeki, Tokyo Institute of Technology, Japan
Emil Sekerinski, McMaster University, Canada
Rudolph E. Seviora, University of Waterloo, Canada
Xiaoyu Song, Portland State University, USA
Mark Staples, National ICT Australia, Australia
Frank Stomp, Wayne State University, USA
Paul Strooper, The University of Queensland, Australia
Jing Sun, The University of Auckland, New Zealand
Paul Swatman, University of South Australia, Australia
Kenji Taguchi, National Institute of Informatics, Japan
Tetsuo Tamai, The University of Tokyo, Japan
Mark Utting, The University of Waikato, New Zealand
Farn Wang, National Taiwan University, Taiwan
Hai Wang, The University of Manchester, United Kingdom
Ian Warren, The University of Auckland, New Zealand
Jim Woodcock, University of York, United Kingdom
Wang Yi, Uppsala University, Sweden
Huiqun Yu, East China University of Science and Technology, China
Daqing Zhang, Institute for Infocomm Research, Singapore
Hong Zhu, Oxford Brookes University, United Kingdom

[CZT-Users] CZT Typechecker v0.5 released

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

Hi everyone,

I've (finally!) gotten around to producing a new binary, 
command-line version of the Z/Object-Z typechecker, which is the 
same version of the typechecker released with CZT 0.5. It can be 
run like so:
java -jar czt_typecheck_0_5.jar filename1 filename2 ...

This fixes a few problems that were reported from version 0.4.

Cheers,
Tim

[CZT-Users] Minutes of Second Annual CZT Workshop

[Mark U. <ma...@cs...>]

Dear CZT-interested people,

Here are some minutes and notes that I wrote up about the
CZT workshop that we held this week at York University, UK.


Minutes of the Second Annual CZT Workshop
24-25 Aug, York University, UK


Overview:
We held a public CZT seminar on Thursday, with about 18 people
attending, then more specific user-oriented discussions on Thursday
afternoon (7 people) and developer discussions on Friday (5 people).

The public seminar was called "CZT: Past, Present and Future" and included
short demos of the command line, jEdit and Eclipse interfaces to CZT.


The audience feedback was encouraging and several people said that
the GUI interfaces looked very useful, particularly the Eclipse interface
because lots of people are already using Eclipse for other purposes.


Here are some of the specific feedback points that I recorded on Thursday:

* Our CZT architecture diagram needs updating to show the connections
  that CZT now has with many existing tools, such as jEdit, Eclipse,
  the Circus tools, the Z/EVES connection, and other Z provers
  (via the Spivey-Z printer).

* In the GUIs, it might be more readable if some of the error messages
  were multiline, rather than having to scroll sideways to see the message.

* "Are there any plans to develop reasoning tools?"  [I said no, because
  we aim to connect to existing provers.]  "Are there any plans to make the
  GUIs usable as front-ends for a proving environment?"  [This seems
  useful, and we are starting to move towards this with the term
  selection facility in jEdit and Eclipse, so that you can select a
  term, then send it to a prover, unfolder, animator or other tool.]

* In error messages, we should use the Z standard terminology "name"
  rather than "identifiers".

* In the jEdit and Eclipse ZCharMap panels, it might be nice to provide
  keyboard shortcuts for entering each character, in addition to the
  entry by mouse click.

* "It would be nice to show real boxes around the schemas, especially
  in the Unicode WYSIWYG editors."  [This could be done by having
  a very custom editor in Eclipse, or by using sequences of line-drawing
  Unicode characters, and stripping them out before saving.]

* We discussed the possibility of changing the Unicode part of the Z
  standard to use separate characters for \where and |.  Ian Toyn noted
  that this requires changes to about 14 places in the Z standard.
  [This change would simplify the Unicode-to-Latex converter a lot,
  and could make it easier to provide the line-drawing support mentioned
  in the previous point.]

* While demonstrating the necessity of having spaces in some places
  in a Unicode spec, but not in others, we noticed that \finset did
  not correctly form a word like \power.  This turns out to be a
  bug in the way jflex(?) handles 32-bit unicode characters.

* We noted that ZLive does not yet unfold declarations within quantifiers.
  This should be implemented quickly.

* It would be useful if ZLive could allow given sets to be replaced by
  some finite set (supplied by the user) for animation purposes, like
  the B-tool.

* Several people commented that Jaza (my old Z animator) had been very
  useful in their projects and that they are keen to try ZLive once it is
  more complete.



[The rest of this email is probably only of interest to CZT developers]

Here is a very brief summary of the discussions in the CZT developer
sessions held on Friday.  [Personal note: I found these discussions to
be extremely valuable and interesting.  It was inspiring and enjoyable
to work together as a group of people who have similar goals, who all
have deep understanding of various aspects of the CZT framework and
are actively contributing to the various tools and standards.]


* The change from CVS to SVN (on sourceforge) is working well.

* We should all try to log bugs in the sourceforge bug system,
  so that we have good records of the number of bugs found and fixed.
  For example, we can use such records to calculate our DDP (Defect
  Detection Percentage), which is the percentage of bugs found during
  development, compared with all bugs found.

  Our goal is to report all bugs found after the code is committed.
  But some flexibility is expected here so that we do not have to
  log bugs in work-in-progress code that is not yet being used by others.

* We will continue the migration from ant to maven and eventually
  drop support for ant.  Petra is writing several Maven plugins to
  support the CZT build process better (eg. so it knows how gnast
  generates Java code from our XML schemas, and how all our parsers
  are generated from XML template files.)

* We will try to see if we can make the projects and maven dependencies
  more fine-grained, so that it is possible to build just the Z tools,
  or just the Circus tools, or some tools without the JAXB stuff, etc.
  This will probably mean lots more smaller top-level projects, with
  names like:  parser_templates, parser_z, parser_oz, parser_circus...

* It would be useful to have a CZT Wiki, for better documentation
  and FAQ for the CZT tools, as well as for developers to communicate
  current status information etc.  Tim will investigate setting up
  a Wiki later this year.

* Flyweight ASTs.  We had a long discussion on Leo and Petra's
  design for having immutable versions of the AST nodes, with a
  factory that guarantees that all identical nodes are shared.
  However, it must still be possible to add/remove annotations,
  which leads to several possible designs.  We did not come to a
  conclusion on how best to support 'unshared' annotations (which
  are attached to a given occurrence of a term, rather than to all
  occurrences), but decided to try out this flyweight AST idea and
  measure its impact on performance.  Initially, we will support
  'shared' annotations only (where annotations are common to all
  occurrences of each term).

  We noted that {} seems to be the only term that would have multiple
  type annotations, yet be shared in a flyweight tree.  To avoid this,
  it might be worth adding the type explicitly into the {} (SetExpr) term
  so that it is not shared?

* Rules.  Mark explained the rationale and design of the CZT inference
  rules, plus the Prolog-like prover that allows them to be applied
  recursively to rewrite terms, unfold schemas etc.

  We discussed the problem of how to unify the unique-ids attached to
  bound variables in CZT terms and came up with 5 possible solutions.
  1. Ban ZDeclNames (concrete bound variables) in rules.
  2. Error when two jokers are unified within the scope of bound variables.
  3. Record the unique-id equivalence relation (IdEq) when two jokers are
     bound, so that future instantiations can use the correct bound variable.
  4. Return the IdEq relation from the unification like the joker
     bindings are already returned.
  5. Like 4, but change the unification to *only* return the unifier
     information (Joker map and IdEq relation), so that terms are not
     destructively updated at all.
  I concluded that we should use 2 first, because it involves few
  changes, and investigate changing to 5 in the longer term.

  We also discussed the current Z-only limitation of rules, because gnast
  supports only single inheritance XML schemas.  We decided that in the
  short to medium term we will live with this, and just change the OZ
  and Circus XML schemas to inherit from the ZPattern one, rather than
  the Z schema.  This will allow the Object-Z and Circus tools to use
  the rules facilities with minimal changes.

* Browsing.  Ian suggested that now that we can select terms in the
  GUIs, we could expand the number of commands that can be applied to
  the selected term.  For example:
    show its syntactic category,
    show its type,
    unfold it using some rules like the schema expansion rules
      (result could be displayed elsewhere, or could replace the selection),
    evaluate with ZLive,
    send to a theorem prover,
    etc.

* Section Manager.  The current section manager is useful, but does not
  support different versions (updates) of a specification, so it has to
  be cleared/reset after every change.  A better approach would be to
  track dependencies, but this has been found difficult to do.
  Rather than reinventing the wheel, we should investigate the Rodin
  core database, which is designed to work with Eclipse, to see if we
  could use it as a replacement for our CZT section manager.

* Some Future Goals.
  A primary goal of the NZ CZT effort is to complete the ZLive and Z2B
  tools in order to perform some industry case studies with the CZT
  tools in the next 12 months.
  One of Leo's goals is to have a complete Circus parser and typechecker
  integrated into Eclipse by March 2007, then to investigate the use
  of ZLive within the Circus model-checker.


Thanks to Leo and Ian for hosting this workshop at York!
Mark

Dr Mark Utting, Senior Lecturer, Dept. of Computer Science,
The University of Waikato, Private Bag 3105, Hamilton, New Zealand.
Phone: +64 7 838 4791     Web:   http://www.cs.waikato.ac.nz/~marku
Fax:   +64 7 858 5095     Email: ma...@cs...

[CZT-Users] CZT seminar + workshop at York University, 24 August

[Mark U. <ma...@cs...>]

Dear Z people,

In just less than 2 weeks time, we are holding a CZT
(Community Z Tools) seminar at York University, followed
by a CZT discussion and workshop afternoon.

    Thursday, 24 August from 12:15 to 13:15 in CS103

You are all warmly invited.  And please invite others who you
think might be interested to hear about CZT.
See http://czt.sourceforge.net for general information about CZT.


Title:  The Past, Present and Future of the Community Z Tools

Speakers: Mark Utting and Petra Malik
          The University of Waikato, New Zealand

Abstract: This talk will give an overview of the goals and
history of the CZT project, a presentation of the current
tools and their capabilities, and a discussion of possible
future directions.  The talk will include a brief
demonstration of several different interfaces to the
CZT tools (command-line, jEdit, Eclipse).

This talk is aimed primarily at Z users, so they can evaluate
the CZT tools, provide feedback and have some input into
future directions.  After lunch, there will be
further discussions on CZT design, usability and technical
issues that all interested people are also welcome to join.


We hope to see you there...
Mark

Dr Mark Utting, Senior Lecturer, Dept. of Computer Science,
The University of Waikato, Private Bag 3105, Hamilton, New Zealand.
Phone: +64 7 838 4791     Web:   http://www.cs.waikato.ac.nz/~marku
Fax:   +64 7 858 5095     Email: ma...@cs...