Sven Lämmermann and Enn Tyugu
We discuss logic and specification language of a program synthesizer for Java intended for dynamic synthesis of services. We introduce metainterfaces as logical specifications of classes. They can be used in two ways: as specifications of computational usage of classes or as specifications of new classes composed from metaclasses - the classes already supplied with metainterfaces. The specification language used has a straightforward translation into a restricted first-order constructive logic. New programs are composed by a deductive synthesis method close to the structural synthesis of programs. An example of composition of a transaction service is presented.