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. © 2007 Elsevier B.V. All rights reserved.

Original publication

DOI

10.1016/j.entcs.2007.03.021

Type

Journal article

Journal

Electronic Notes in Theoretical Computer Science

Publication Date

12/07/2007

Volume

184

Pages

171 - 187