SWIN: Towards Type-Safe Java Program Adaptation between APIs

Java program adaptation between different APIs is a common task in software development. When an old API is upgraded to an in-compatible new version, or when we want to migrate an application from one platform to another platform, we need to adapt programs between different APIs. Although different program transforma-tion tools have been developed to automate the program adaptation task, no tool ensures type safety in transforming Java programs: given a transformation program and any well-typed Java program, the transformed result is still well-typed. As a matter of fact, it is often observed that a dedicated adaptation tool turns a working ap-plication into a set of incompatible programs. We address this problem by providing a type-safe transforma-tion language, SWIN, for Java program adaptation between differ-ent APIs. SWIN is based on Twinning, a modern transformation language for Java programs. SWIN enhances Twinning with more flexible transformation rules, formal semantics, and, most impor-tantly, full type-safe guarantee. We formally prove the type safety of SWIN on Featherweight Java, a known minimal formal core of Java. Our experience with three case studies shows that SWIN is as expressive as Twinning in specifying useful program transforma-tions in the case studies while guaranteeing the type safety of the transformations. 1