@inproceedings{DBLP:journals/entcs/FaitelsonWD07,
  abstract = "This paper explains how a declarative method language, based upon the formal notations of Z and B, can be used as a basis for automatic code generation. The language is used to describe the intended effect of operations, or methods, upon the components of an object model; each method is defined by a pair of predicates: a precondition, and a post-condition. Following the automatic incorporation of model invariants, including those arising from class associations, these predicates are extended--again, automatically--to address issues of consistency, definition, and dependency, before being translated into imperative programs. The result is a formal method for transforming object models into complete, working systems.",
  author = "David Faitelson and James Welch and Jim Davies",
  booktitle = "Proceedings of SBMF 2005",
  doi = "10.1016/j.entcs.2007.03.021",
  journal = "Electronic Notes in Theoretical Computer Science",
  pages = "171--187",
  publisher = "Electronic Notes in Theoretical Computer Science",
  title = "From Predicates to Programs: The Semantics of a Method Language",
  volume = "184",
  year = "2007",
}