[ Home  |  FAQ-Related Q&As  |  General Q&As  |  Answered Questions ]

    Search the Q&A Archives

Dear all, I need to check an Object-Z specification. I...

<< Back to: comp.specification.z Frequently Asked Questions (FAQ)

Question by Denis Reilly
Submitted on 11/12/2003
Related FAQ: comp.specification.z Frequently Asked Questions (FAQ)
Rating: Not yet rated Rate this question: Vote
Dear all,

I need to check an Object-Z specification. I downloaded the Wizard checker from University of Queensland: http://www.itee.uq.edu.au/~smith/tools.html but failed to get this checker to run. Can anyone point me in the direction of another Object-Z checker or explain what is going wrong with the Wizard checker. I have tried to contact the University of Queensland group, but I have not received a reply.

Denis Reilly

Answer by Geoff Kassel
Submitted on 12/27/2003
Rating: Not yet rated Rate this answer: Vote
Hi Denis,

A couple of questions first:

1) How have you marked up your Object-Z specification? Wizard accepts an older version of the Object-Z LaTeX markup, and it can act oddly if it doesn't get exactly what it expects. (Segmentation faults are a common sign of that, in my experience.)

2) What output did you get from Wizard (if any?)

and mostly out of curiousity,

3) Who did you try to contact at UQ? I believe a few of the formal methods people have left recently, so you might have been sending e-mails into the ether.

As for another Object-Z checker, unfortunately, there isn't one - yet. There's been a lot of work done recently on heavier tools, like model checkers, theorem provers, and animators, but really not much on the lighter stuff. There is work on resolving this, but don't hold your breath for any usable tools soon.


Geoff Kassel, UQ ITEE/SVRC/SSE PhD student


Answer by Gasso Wilson Mwaluseke
Submitted on 5/23/2004
Rating:  Rate this answer: Vote
Wizard works perfectly with Linux.  If you tried to use it with another operating system, you probably need to tune your Wizard to suit your needs.  I am using Linux and I have no problems at all.  Even if you manage to get Wizard to work you need to be careful because it is very tricky.




Your answer will be published for anyone to see and rate.  Your answer will not be displayed immediately.  If you'd like to get expert points and benefit from positive ratings, please create a new account or login into an existing account below.

Your name or nickname:
If you'd like to create a new account or access your existing account, put in your password here:
Your answer:

FAQS.ORG reserves the right to edit your answer as to improve its clarity.  By submitting your answer you authorize FAQS.ORG to publish your answer on the WWW without any restrictions. You agree to hold harmless and indemnify FAQS.ORG against any claims, costs, or damages resulting from publishing your answer.


FAQS.ORG makes no guarantees as to the accuracy of the posts. Each post is the personal opinion of the poster. These posts are not intended to substitute for medical, tax, legal, investment, accounting, or other professional advice. FAQS.ORG does not endorse any opinion or any product or service mentioned mentioned in these posts.


<< Back to: comp.specification.z Frequently Asked Questions (FAQ)

[ Home  |  FAQ-Related Q&As  |  General Q&As  |  Answered Questions ]

© 2008 FAQS.ORG. All rights reserved.