This paper presents some of our requirements for a Z typechecker: that the typechecker accept all well-typeable formulations, however contrived; that it gather information about uses of declarations as needed to support interactive browsing and formal reasoning; that it fit the description given by draft standard Z; and that it be able to check some particular extenstions to Z that are intended to allow explicit definitions of schema calculus operators. The paper presents a specification for such a Z typechecker, which we have implemented.
Full paper : PDF 314K
@inproceedings(SS-ZB2000c, author = "Ian Toyn and Samuel H. Valentine and Susan Stepney and Steve King", title = "Typechecking Z", pages = "264--285", crossref = "ZB2000" ) @proceedings(ZB2000, title = "ZB2000: First International Conference of B and Z Users, York, UK, August 2000", booktitle = "ZB2000: First International Conference of B and Z Users, York, UK, August 2000", editor = "Jonathan P. Bowen and Steve Dunne and Andy Galloway and Steve King", series = "LNCS", volume = 1878, publisher = "Springer", year = 2000 )