An axiomatic basis for proving total correctness of goto-programs

Título:

An axiomatic basis for proving total correctness of goto-programs

Autor:

Wang, Arne

Colaboradores:

; 

Temas:

CORRECCIÓN DE PROGRAMAS

En:

BIT Numerical Mathematics, Vol. 16 No. 1 (Mar. 1976), pp. 88-102.

Resumen:

The paper presents an axiomatic basis, similar to that of Hoare, for proving properties about programs by decomposition into proofs about the syntactical program-components. In addition to the partial correctness, which can be proved by Hoare's method, the present basis includes the aspect of termination, i.e. total correctness. Moreover, it is shown how partial and total correctness may be handled within a unified framework. Among the basic program components agoto-statement is considered. Thewhile-statement is defined in terms of more basic constructions, and some useful and familiar theorems are proved. The subject of recursive procedures is treated briefly.

URL/DOI:

Medio:

Soporte electrónico

Tipo de documento:

Artículo

Idioma:

Inglés

Publicación:

, 1976

Puede solicitar más fácilmente el ejemplar con: A0087