[CZT-Devel] Examples of CZT transformation rules

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

Dear Petra and Tim and others,

Here is an updated draft of my proposal for implementing transformation
rules (and eventually a simple theorem prover) within CZT.

You don't need to read the whole document, but
I've put more examples in (Section 3), for unfolding schema expressions,
and would like to see what you think of  them.  Does this look a nice
way of implementing schema unfolding?  

I've also updated the syntax of the proposal (Section 2), which
may interest parsing people.

Rationale:
The whole area of unfolding schema constructs is the bottleneck
in developing new CZT tools at the moment.  Virtually all Z tools
want to transform schemas etc. so need an unfolded version of them.
So we either need to implement rules like these, or hand-code schema
unfolding in Java.  If possible, I prefer the rule approach, because
*  it will allow us to prove the rules correct (not possible for Java code)
* it has many other uses (other kinds of unfolding)
* and (most importantly) it records the design of the rules at a higher
    and more readable level than Java code would.

TODO: more comparison of this proposal with CADiZ tactics
and with the rules of the Z_C and V logics for Z.

Comments?
Mark.