Resumen
In today's team-based software development, good commit messages - comments on changes made in natural language - are essential. The metric for evaluating a commit message is its relevance. A good commit message should not only describe the changes made, but also their context.With the growing popularity of version control systems, the number of studies aimed at creating tools for automatic generation of commit messages has increased. The most promising for this task are methods based on deep learning and neural machine translation. Such methods have program code or something to which it can be reduced as input. The only possible way to automatically generate a message for a commit is to "look" at the history of changes (diff). All modern version control systems provide the user with such a history, and special algorithms have been designed to compare changes between two versions of program code. But there are a great many programming paradigms, even more there are programming languages with their own features and syntax. To make a tool for generating commit messages universal, it is necessary to be able to reduce the program code in any programming language to a single "notation".One possible example of such notation is formal specifications. A specification shows what a program should do. There are many ways to write formal specifications, from algebraic expressions and specification languages to deterministic finite state machines. Since a commit message should give an indication of what and how the new software version has changed, the idea of using program specifications in commit message generation tools seems very rich.Currently, most programs do not have a formal specification. It is believed that the time spent on elaborating specifications is not worth the result. One of the effective approaches to solve this problem is specification mining.