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.
