Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397

Issue N5 2015 year

Formal Models of Programming Languages and Programs. Part 1. Literature Review: 1930—1989
V. A. Vasenin, Head of the Laboratory, e-mail: vasenin@msu.ru, M. A. Krivchikov, Researcher, e-mail: maxim.krivchikov@gmail.com, Institute of Mechanics, Lomonosov Moscow State University

The main contribution of the present article is a historical literature review and a critical analysis of the publications on the following topics: the formal verification, formal models of software and the development of formally verifiable software. Publications on the listed topics are presented in a context of the software engineering development in general. The cited papers were published in the time frame of 1930-1989. One of the specific topic of interest of the presented research is the dependently-typed programming development from the untyped lambda-calculus to the calculus of constructions. The complexity introduced into general purpose programming languages from the formal verification point of view by the means of computational models having an inconsistent logical interpretation is noted. Fundamental results associated with the formal verification are also mentioned. In the last part of the article the commonly used distinction of the model-theoretic and the proof-theoretic (deductive) approaches to formal verification is considered.

As a conclusion, two points are stated. In the first place, the representation of the specification and especially the program code in a mathematically rigorous way nowadays is probably the most complex part of the formal verification problem. In the second place, despite active research since late 1960s, construction of the formal semantics for a general-purpose programming language is still a complex task. It is possible that for this reason the formal descrption of the programming language is still not required by international standards organizations and commitees.

Keywords: formal verication, programming languages, domain-specific languages, programming language formal semantics, software engineering, bibliography
pp. 10–19