A Semantic Basis for Program Verification

Publisher Website
Google Scholar
Abstract
There has been considerable development in recent years towards a general theory of program verification. Starting with the papers [3] and [4] there has been an increasing momentum towards the development and perfection of this theory. However, many of the treatments (see [2] for example) while containing ideas that are important seem to suffer from the lack of a clear and coherent theoretical framework. Such a framework is necessary in order to generate the verification rules and to justify them. The aim of this paper is to provide such a framework. The details of the approach represent in fact a choice among several possible, more or less equivalent approaches. However, the reader can devise these variants for himself. What is important here is the spirit of the approach which involves an explicit definition of the verification language and its semantics.

This publication has 0 references indexed in Scilit: