home > publications > Z > Typechecking Z

Ian Toyn, Samuel H. Valentine, Susan Stepney, and Steve King
Typechecking Z.

In Jonathan P. Bowen, Steve Dunne, Andy Galloway, Steve King, editors, ZB2000: First International Conference of B and Z Users, York, UK, August 2000 . Volume 1878 of Lecture Notes in Computer Science, pp 264--285. Springer, 2000.

Abstract:

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
)