Hi,
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!
David
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.
