Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Issue N5 2015 year
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.