Search code examples
alloy

Try to build a Java program to convert from Alloy instance to any language code


I am working on a research project that an Alloy generated instance holds entities (such as Signatures, Fields, Relations or Tuples) that resemble a programming language (such as java, c, etc).

For example, there are entities for Arithmetic operations (such as Add, Sub, Multiply, etc), for Relational operations (such equals, greater than, less than or equal, etc.) for variables, constants, and so on.

A tree view and graph view examples (max of two integers algorithm) of the model solution (instance found) are showing next. Those figures were extracted from Alloy Analyzer GUI.

Tree view of max2 of two integers

Graph view of max2 of two integers

My question is there a quick way to convert that alloy instance to any common language source code (Java would be the preferred language)?

Or should I do everything (Sigs, Fields, Atoms, language brackets, indentation, etc) by starting this way (going through an A4Solution) to build a kind of translator?

The main goal here is to build a Java program that is able to convert an Alloy instance to a Java source code file ready to compile and run.

//max of 2 integers' java source code at mymax2.java file
class MyMax2 {
    public static void main(String[] args) {
        int x;
        int y;
        int res;
        if(y <= X) {
            res = x;
        } else {
            res = y;
        }
    }
}

Finally, convert from XML to Java, by starting this way is not a desired option.

Thank you for help me on :)


Solution

  • Yours is really a formatted printing problem, with a tree as the data input. The tree is roughly an Abstract Syntax Tree (AST).

    Do a post-order transversal of the tree, adding in the sensible text to each node as you travel back up the tree.

    This means your "text for the node" function will look like a visitor, with lots of "policies" for each node type; however, there will be some wrinkles to address when it comes to variable scoping. Basically, the position of the declaration seems to be lost in your AST, and so you will have to write some code to cache the variable names in play, and define them in the upper blocks.

    Since it might be ambiguous which block you would "unroll" your "variables to be declared" as you collapse your tree from the bottom up, your code will not be 100% identical to the input code. For example

    public static void main(String[] args) {
       int x;
       if (x > 3) {
         int y = 3 + x;
         return x + y;
       } else {
         return 4;
       }
    }
    

    might (after a full round trip of being converted to AST and back) read as

    public static void main(String[] args) {
       int x;
       int y;
       if (x > 3) {
         y = 3 + x;
         return x + y;
       } else {
         return 4;
       }
    }
    

    Also, this assumes your AST has a pretty tight fit to the target programming language. For example, if you wanted to convert the presented AST to Prolog; you would quickly find out that the constructs in your AST are a poor fit for Prolog generation.

    Should you need some direction, look into Pretty Printers which leverage most of the components of a compiler, with the exception that after they have their AST, they process it back out as source code.

    There are a few wrinkles, but nothing too severe (provided your AST isn't missing a critical piece of information for the reverse back to source code).