Automatically generating a program from its specification eliminates a large source of errors that is often unavoidable in a manual approach. This work investigates the theory behind Booster - a specification language and automatic code generator, developed by Dr. Ib Sorenson and his group at Oxford University's Computing Laboratory. The work focuses on three contributions: semantics, model completion and code generation. The semantics of a Booster model is a single abstract data type (ADT) where the invariants and the methods of all the model classes are promoted to the ADT. This work argues...