[CZT-Devel] Evaluating Z in Java

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

Dear Petra, Tim and others

I am interested in the development of a z-evaluation tool similar to 
Jaza (by Mark) in Java.
Moreover, is there any interest in working on the development of  a 
Z-toolkit in Java?
Is there any work in these fronts? If so, any plans/architecture/models 
for it already?
If not, apart from Jaza, JML and Jakarta-Common-Collections, do you know of
any other interesting sources on this? I would be very interested in 
participating.

This Z evaluator will be used as part of the development of a 
model-checker for Circus, a language that
combines CSP and Z in the unifying theories of programming. After 
working in the theoretic background,
we are now at the implementation stage. Eventually, we expect this to 
become a sort of Z-Evaluator/Prover.

Best regards,
Leo

-- 
-------------------------------------------
Leonardo Freitas
PhD - Circus Model Checking
Formal Methods - HISE Group
HISE - High Integrity Software Engineering
http://www.cs.york.ac.uk/~leo
-------------------------------------------
Beyond reason, there is no court to appeal
-------------------------------------------