Z Notation Example

This is the first formal specification I’ve created using Z Notation. It’s based on the usual Birthday Book example but is a little different. It also has some information regarding use of ZETA for type-checking the units. See links below for the source and generated output.

http://recluzepage.googlepages.com/StudentDB.pdf

http://recluzepage.googlepages.com/StudentDB.tex

Zeta + HOL-Z Presentation

Here’s the second presentation in the series. It deals with how HOL-Z can be used. It is only a skeletal presentation because honestly, you need to do a lot of reading before you can work with HOL-Z. This is just a rough guideline about the procedure followed. Here’s the link:

http://recluzepage.googlepages.com/ZetaPresent2.pdf