We propose an extension to Z whereby generic parameters may have their types partially constrained. Using this mechanism it becomes possible to define in Z much of its own schema calculus and refinement rules.
Full paper : PDF 192K
@inproceedings(SS-ZB2000d,
author = "Samuel H. Valentine and Ian Toyn and Susan Stepney and Steve King",
title = "Type-constrained Generics for Z",
pages = "250--263",
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
)