The use of ghost variables and virtual programming in the documentation and verification of programs. (English) Zbl 0544.68006
Summary: Using ghost variables and virtual programming, a method for documenting programs which exhibit some common characteristics is presented. The annotations required are expressed in a powerful high level assertion language. The usefulness of these annotations is illustrated by the generation of verification conditions for some small example programs written in a dialect of Pascal. Demonstrations of the correctness of these programs are also given.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
ghost variables; virtual programming; documenting programs; high level assertion language; verification conditions; Pascal; correctnessReferences:
| [1] | Clint, Acta Inform. 2 pp 50– (1973) |
| [2] | Katz, Acta Inform. 5 pp 333– (1975) |
| [3] | Luckham, Acta Inform. 8 pp 21– (1977) |
| [4] | Gries, Acta Inform. 6 pp 319– (1976) |
| [5] | Howard, Comm. ACM 19 pp 273– (1976) |
| [6] | Correctness of data representation, Doctoral Dissertation, The Queen’s University of Belfast, 1976. |
| [7] | Hoare, Acta Inform. 2 pp 335– (1973) |
| [8] | Malik, Australian Comp. Sc. Comm. 2 pp 217– (1980) |
| [9] | and , ’The annotation of program modules’, (submitted to Acta Informatica), 1979. |
| [10] | ’Data representations in high-level programming languages’, Doctoral Dissertation, The Queen’s University of Belfast, 1975. |
| [11] | ’The use of ghost variables in proofs of correctness of programs’, Master’s Dissertation, The Queen’s University of Belfast, 1977. |
| [12] | De Millo, Comm. ACM 22 pp 271– (1979) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
