I hope this question does not sound like "hey guys, I am feeling lazy, just tell me how to do it". I'm indeed spending hours of google-searching for papers, but I'm beginning to run in circles. Therfore I seek external hints.

In short: I've written a parser for a Java-like language which is expected to produce JVM bytecode.

As a second step, now I want to write the mapping into a semantic model, validate that model (type checking, scopes checking and so on).

A third step will be transforming the semantic model into JVM bytecode.

An additional requirement is that I want to implement the second and third step with formal methods.

So, to be more concise about what I want to achieve: 

-Let S be my language (the one I am implementing).
-Let O be a model for OOP formal semantics (general enough, language-agnostic); let S(O) my language's formal semantics defined within O; and let JVM(O) JVM bytecode's formal semantics defined within O. Note that both S(O) and JVM(O) are defined within O.
-- [JVM bytecode -> JVM(O)] is injective, so it is reversable and I can transform models written in O into JVM bytecodes.
-- [S->S(O)] is a subfunction of [S->JVM(O)], so everything written in S source will have a meaning within JVM(O).

-Let S1 be a source program written in my language S.

Now, I am pursuing one or more frameworks that will assist me as much as possible in automatizing these three processes:

1) The formal sematics specification of my language S, 
2) Writing and testing the compiler itself (including its formal verification),
3) Executing users' compilations (for a given source, generate and validate a semantics model and then a target bytecode model).

I have found frameworks (either theoretical and/or executable frameworks) that assist in each one of the steps, but I failed to find an out-of-the-box ready framework that I might use for 1, 2 and 3.

Do you happen to know one, or perhaps you can suggest a least resistance path (in terms of mandays) to implement one?

Every contribution will be appreciated!


PS: I am omitting the frameworks I have been playing with in order to first focus on the theoretical problem and make sure I am understood. Later on I can give implementation details. 

jvm.jpg 7.11 Kb . 0 Views
guide.jpg 52.95 Kb . 0 Views
Be the first person to like this.