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