From Predicates to Programs: The Semantics of a Method Language

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.