LinLog

This week I've been playing around a little with the Community Z Tools. They are a set of free tools for working with the Z specification language. They're still not anywhere near complete, but I guess they're better than nothing.

If you're an average programmer, you're probably not familiar with Z. It's a formal specification language based on set theory and first-order predicate calculus. Basically, that means it's a mathematical language to write program specifications. You build schemas, the Z unit of encapsulation and reuse, using the notation of predicate logic and set theory, and then compose these schemas to describe the various states and operations of the system. This has several advantages over the traditional natural-language specification, including the ability to deductively prove various properties of the specified system, such as consistency, and the simple fact that formal languages are, by their very nature, much more precise than natural ones. If you're interested in learning more, take a look at the book Using Z. I've been reading it and I think it's pretty good. It's also available for free in PDF format, which is really nice.

So anyway, I was playing with the CZT. The current incarnation is pretty much just a bunch of Java classes that provide a plug-in to jEdit. The plug-in allows you write Z specificaitons in Unicode and LaTeX (note that Z, like most mathematical notaitons, uses lots fo funy symbols, so you can't just write it in a word processor), an XML schema, and a typechecker. The main problems, aside from being incomplete, are that saving and reloading Unicode specifications doesn't seem to work correctly and that installing CZT is hideously complex. OK, that's probably an overstatement, but it's cretainly not easy, and it's made more difficult by the fact that the main download site only offers source, not binaries (which makes no sense, since it's written in Java).

As a brief aside, jEdit seems pretty nice. It's not likely to replace Vim or Kate for my purposes, but I like it so far. My only real complaint is that Swing's GTK+ look doesn't seem to work the GTK/Qt theme engine.

Getting back to the point, since I had problems with editing specifications in Unicode, I decided to give LaTeX a try. I knew nothing about LaTeX other than it's related to TeX which is used for typesetting, so I went to the web site and ended up downloading The (Not So) Short Introduction to LaTeX2e.

I haven't gotten very far into it yet, but I have to say that LaTeX looks extremely cool. It's a "document preparation system" that, frankly, looks kind of like a programming language. It's generally written by editing text files, so it's not a WYSIWYG system. With LaTeX, you focus on the logical structure of the material rather than the details of how it looks on the screen. That immediately struck me as the right thing to do. I've seen too many Word documents that were an incoherent soup of seemingly random formatting that looked decent on paper, but was a huge pain to try to edit later. I'm actually kind of anxious to try LaTeX out.