Verifying Transformations of Java Programs Using Alloy

In this paper we verify Java transformations by using a fourth–stage strategy. Initially we embed models in Alloy: a metamodel for a subset of the Java, a model for each program transformation being investigated, and another one for a program called Validator that exercises methods of each side of the transformation. Secondly, we use the Alloy Analyzer to find valid instances, corresponding to pairs (left and right-hand sides of a program transformation) and instances of the Validator. If instances can be found, this means they describe well–formed programs as long as transformation conditions, structural and type constraints are formally stated in our models. Thirdly we developed a tool that translates the Alloy instances to Java; finally, these are executed and the results used to verify whether there are any dynamic semantic problems in the resulting programs.