Vimes
Vimes is a typechecker for Z specifications.
Z is a standard (ISO/IEC 13568) language for formally specifying systems, principally software systems, but it has been used on hardware systems.
Vimes is a command line utility which accepts a specification using LaTeX markup and reports any syntax or type errors. It can report the signatures of each paragraph or the type of every entity in the specification and how it worked out that type. It conforms to the ISO standard and adds some bits from oz.sty. For more details see the manual page.
It comes with the definitions of the prelude and standard toolkit, of course, and also with the definitions from Valentine, Stepney and Toyn’s Z Patterns Catalogue II. This provides a much richer and more powerful toolkit than the standard. (You can find the full thing here.)
It is distributed as GPLed source code in vimes-0.2.7.tar.gz and built using the familiar configure, make, make check and make install. I would deem it a favour if, when you have downloaded and built a copy, you would contact me at the address given below to tell me you had done so and what problems you encountered.
Vimes is not derived from, based on or inspired by any other typechecker, so its idiosyncrasies and short-comings are all its own.
While it is at present simply a typechecker, it is intended to add theorem proving capabilities. We have a Cunning Plan.
