Update and Questions
April 23rd, 2007 By recluze

A.A. everyone.

Nothing going on in the group scene? Isn’t anybody doing anything? Or should I say, isn’t anybody writing anything about what they’re doing?

Here’s my update on my work with Z.

I’ve almost finished the Using Z book. I’m on to the chapter that has the first case study – the file system. This book not only has the specification part of Z but also the analysis/verification part. Very good book, not only for learning but also as a reference.

I’ve also covered the Birthday Book example that comes with all tools of Z. I’ve seen how HOL-Z takes Z notation specification and performs verification on it. I’ve done practicle upto the point where one generates .holz file. I’ve yet to load it in Isabelle and actually perform the verification.

I believe I need two things now:

  1. The Using Z book needs to be printed. It’s great to be kept as reference. Since I’ve covered a whole semester’s worth of notes in a week, it keeps sliping out of my mind. I need some sort of printed material next to me so that I can keep reading it whenever I get a minute free. Unfortunately, this is outside my resources as the book is 409 pages long. It would be really nice if “someone” (I dunno, probably someone who’s in ims’s faculty :) can get it printed. I only need it for a month or two. It can go back to IMS as a reference book or something. Is it possible?
  2. Like Mr. T said in the last meeting, it would be really nice to have the base work that Mr. MM is working on. Now, I can understand Z almost completely and it would be really nice to be able to practice on the targetted area alongside the textbook case studies. I’m continuing with the book case studies but it would be better (and less time consuming) to also start work on the targetted specification. Mr. MM?

I have paper going on currently, so I can’t give full time. I’ll be free by 28th of this month inshaallah. I’m really hoping we can get some sort of publication in verification area.

2 Responses to " Update and Questions "
Asher Heimermann
April 23rd, 2007

What is the “Z” book?

Asher Heimermann

April 24th, 2007

The “Z” book is Using Z. You can find it at http://www.usingz.com.

If you don’t know what Z is, try searching for “Z Notation” in wikipedia. Tell me if you need help with it. I’ll be glad to help.

Leave a Reply