SWIN

Abstract

Java program adaptation between different APIs is a common task in software development. When an old API is upgraded to an incompatible 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 transformation 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 application into a set of incompatible programs. We address this problem by providing a type-safe transformation language, SWIN, for Java program adaptation between different 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 importantly, 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 transformations in the case studies while guaranteeing the type safety of the transformations.