Automatic Generation of Implementations For Object-Oriented Abstractions ∗

We present a general-purpose code transformation system, the POET system, for the purpose of automatic code genera-tion from high-level behavior specifications of object-oriented abstractions to low-level efficient implementations in C++ and Java. In particular, we have developed an extended finite-state-machine-based language, iFSM, which models the behavior logic together with implementation details of arbi-trary OO abstractions. We then use the POET system to au-tomatically translate the behavior specifications to type-safe OO implementations in Java or C++. Finally, we use the POET system to automatically translate the behavior speci-fications to the input language of a model-checker (NuSMV) and apply model checking to validate the correctness of the specification. If the iFSM specification is correct, our ap-proach can always generate a correct and type-safe imple-mentation. 1