World's most popular travel blog for travel bloggers.

[Answers] The importance of the language semantics for code generation and frameworks for code generation in model-driven development

, , No Comments
Problem Detail: 

I am implementing worflow where the code in industrial programming languages (JavaScript and Java) should be generated from the formal (formally verified) expressions (from ontologies as objects and rule formulas as behaviors). What is the best pratice for such code generation? Are some frameworks available for this?

In my opinion the semantics of the programming language is required. And I should be able to do the code generation in two steps: 1) translate my formal epxressions into semantic expressions of the target language; 2) translate semantic expressions into executable code. In reality I can not find any work that connects semantics of programming language with the code generation.

Is there special kind of semantics of programming languages that is usable not only for the analysis of the programs but also for the generation of the programs?

My guess is that it should be really useful approach for generating formally verified code but I can not find research work about this. Are there trends of better keywords avilable for this?

Maybe - more relevant question is - what kind of compilers/translators the Model Driven Development tools use for the generation of source code (platform dependent code) and how semantics of programming language can be used for the construction of such compilers?

Note added. There already is complete unifying (denotational and operational) semantics of Java, JavaScript and other industrial programmin languages in the K framework. So - this is more question about application of K framework for code generation is that is possible at all?

Asked By : TomR

Answered By : ivcha

In general when we talk about code generation (or model-to-model transformation in general), clearly defined semantics is quite important, since such transformations usually make sense when both the source and the target model semantically match according to some criteria. For example, programmers might describe the behaviour of a program with a formal specification, which, according to the semantics, defines possible implementations in the target language (i.e. outputs of code generation). Failing to precisely define the semantics might lead to ambiguous or, in general invalid, transformations.

Is there special kind of semantics of programming languages that is usable not only for the analysis of the programs but also for the generation of the programs?

In general, there is no need for a special kind of semantics for targeting generation of programs. However, different code generation systems target different domains of code generation and thus leverage different kinds of programming languages and their semantics. (Some overview of code generation in the context of program synthesis can be found in [1]).

There exists a body of work for which a programming language is coupled with language verification and program synthesis (described below). A seemingly well-fitting example of this is the Leon framework, which uses a subset of Scala as the main programming language, that expresses both programs and formal specifications. The framework allows not only verifying that the program matches the given specification (again, strictly defined by the semantics of the language and the interpretation of the logic used in the specification), but also generating code. In the latter case, programmers can only give formal specifications of the program in terms of its precondition and postcondition and the framework, it's code generation part (i.e. its synthesizer), generates the program that matches the given specification [2].

My guess is that it should be really useful approach for generating formally verified code but I can not find research work about this. Are there trends of better keywords avilable for this?

One of the fields that seems to be closely matching what you described is software synthesis. Program synthesis is the task of automatically discovering an executable piece of code given user intent expressed using various forms of constraints such as input-output examples, demonstrations, natural language, etc [1].

In reality I can not find any work that connects semantics of programming language with the code generation.

In general, the compiler for many general-purpose modern (high-level) languages perform some form of code generation that has to satisfy the rules of the language semantics (i.e. its language specification). E.g. the compiler for the Scala programming language emits Java bytecode---which can be thought of as a language which elements semantically closer match the instructions of the actual hardware---according to the Scala language specification.

[About compiler and other tools for] Model Driven Development useful for code generation. What is the best pratice or framework for code generation?

Although, in my answer, I was focusing on the connection of the semantics of the programming language and code generation in the context of (general-purpose) program synthesis, these concepts are by all means applicable to other domains or practices such as Model-Driven Development. For general pointers on this direction, it might be useful to check out books that try to summarize them [4], [5].

So - this is more question about application of K framework for code generation is that is possible at all?

Although, it might be the most suitable for your problem and intended use, there are other alternatives that might also work and perhaps could work for you as well, such as some of the transformation languages like Stratego or rewriting systems like Maude.

[1] Gulwani, Sumit. "Dimensions in program synthesis." In Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, pp. 13-24. ACM, 2010.

[2] Kneuss, Etienne, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. "Synthesis modulo recursive functions." Acm Sigplan Notices 48, no. 10 (2013): 407-426.

[3] Scala Language Specification

[4] Brambilla, Marco, Jordi Cabot, and Manuel Wimmer. "Model-driven software engineering in practice." Synthesis Lectures on Software Engineering 1, no. 1 (2012): 1-182.

[5] Milicev, Dragan. Model-driven development with executable UML. John Wiley & Sons, 2009.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/55781

3.2K people like this

 Download Related Notes/Documents

0 comments:

Post a Comment

Let us know your responses and feedback