Formal Methods, Z Notation

ZETA Presentation

I’ve just finished creating the first presentation about using ZETA for creation/analysis of Z Notation. It’s a basic presentation and is not meant to be used as a reference. See a good book for Z notation (Using Z is pretty good) and the ZETA site for the tool’s reference. The presentation is more about experience in learning to use these tools.

This is the first in a series of presentations hopefully leading to the complete use of Z Notation for formal verification and specification.

See PDF here

Articles, research, resources

HOLZ and Zeta

Installing HOLZ isn’t as easy as you may think it would be. After much efforts, I’ve managed to do it and I thought I should post it here to save you guys some time.

First of all, install Isabelle2005 if you haven’t already.
Then, get zeta and install that using the provided installation classfile. It’s pretty straight forward.

The tricky part is installing HOlZ on top of it. Here’s what needs to be done:

  1. Read the Install file which comes with the HOLZ tarball. (Read the file carefully and make the configuration changes it asks you to.) 
  2. Try installing HOLZ.
  3. It shouldn’t work. (If it does, you don’t need to read this.) You will probably get a message saying, “Build failed”.
  4. Now, locate zeta.sty and put it in HOLZ/src/latex/. This file can be found in lib/latex subdir in the zeta installation directory.
  5. Modify IsaMakefile in HOLZ installation source directory and put a command to copy zeta.sty to the same target as the holz.sty. (You’ll understand what I’m saying when you open IsaMakefile in an editor.)
  6. Now, redo the isatool make command. It should work now.

Secondly, to install the Zeta Adaptor, here’s what needs to be done:

  1. Go to “zeta” subdirectory in HOLZ’s src directory,
  2. Do an “isatool make”.
  3. It will tell you where it’s put the just-installed holz adaptor jar.
  4. Now, go to zeta-1.5/bin where zeta-1.5 is your zeta installation directory
  5. vi zeta
  6. Modify to include the just copied jar.

More on how to get from zeta to Isabelle/HOLZ later. Stay tuned.

Geek stuff, Linux, resources, Web

Gmail, firefox and fonts on Linux

If you’re like me, you’d hate the default look of web pages (especially gmail) on firefox in Linux. I was beginning to think something was wrong with firefox because the rest of Linux fonts look alright. This is what I got after tinkering around for a day. Looks sweet, doesn’t it.

Here’s how to do it:

  1. Get webcore-fonts package. It’s fonts from Microsoft but only the free ones. You’d know Verdana if you come from Windows. If you hate Microsoft… well, write your own fonts of the same quality.
  2. Get Greasemonkey for firefox.
  3. Get Gmail RL Skin Userscript. Very nice script. I did a few modifications for my own use. Here’s my file in case you need it for reference.

Oh, and send a mail to Google telling them to please stop using ‘Arial’ on all their pages. If Verdana isn’t available by default on Linux, other fonts much better than Arial are! You’d think they’d at least look at their pages on a Linux firefox browser. Sheesh!

Announcements, Geek stuff, Linux, Pedagogy, Personal, research

The hapennings…

Well, it’s been a long time but I’m finally back. The reasons for such a long absence are countless but boil down to just one: I got lazy.

Anyway, here’s what I’ve been working on lately:

  • Formal Mathematics (Set theory and logic)
  • Isabelle (automated theorem prover)
  • LaTeX (lovely, lovely typesetting engine. I don’t need a word processor any more)
  • My MS thesis
  • My MS research publication (more on this later)
  • My “Software Engineering Education” paper – that one’s going to be published by IEEE inshallah very soon.
  • And moving my stuff on to linux. I have to live with my conscious

Well, enough for the time being.