Abstract
In this paper an approach to proving properties of programs is presented, which slightly differs from the methods developed up to now. In contrast to other approaches it needs no formal program notion but only a formalization of some basic program properties.
The key idea in this approach is to associate with any program under consideration a formal theory in such a way that all the processes, which may be thougth as possible executions of the program considered, become models of the associated theory. Such a theory can be constructed by formulating axioms about the program executions, and about quantities which explicitly or implicitly occur in the program and change their values while the program is being executed. Appropriate axioms and the properties which are to be proved can easily be described by formulas of the predicate logic. This enables one to consider various properties of the program as theorems of the resulting theory and to prove them by usual means of the predicate logic.
Get full access to this article
View all access options for this article.