This paper explains precisely 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 predicatespre- and post-conditions. Following the automatic incorporation of model invariants, including those arising from class associations, these predicates are extendedagain, automaticallyto address issues of consistency, definition, and dependency, before being transformed into imperative programs. The result is a formal method for transforming object models into complete, working systems.
http://www.lbd.dcc.ufmg.br/colecoes/sbmf/2005/013.pdfCaso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web