An axiomatic basis for proving total correctness of goto-programs
Material type:
ArticlePublication details: ref_localidad@NULL : , 1976Subject(s): Online resources: Summary: 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.
| Item type | Current library | Call number | Status | Date due | Barcode |
|---|---|---|---|---|---|
Capítulo de libro
|
Biblioteca Fac.Informática | A0087 (Browse shelf(Opens below)) | Available | DIF-A0087 |
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.
BIT Numerical Mathematics, Vol. 16 No. 1 (Mar. 1976), pp. 88-102.
There are no comments on this title.