In:
ACM SIGPLAN Notices, Association for Computing Machinery (ACM), Vol. 10, No. 6 ( 1975-06), p. 482-492
Abstract:
This paper is an initial progress report on the development of an interactive system for verifying that computer programs meet given formal specifications. The system is based on the conventional inductive assertion method: given a program and its specifications, the object is to generate the verification conditions, simplify them, and prove what remains. The important feature of the system is that the human user has the opportunity and obligation to help actively in the simplifying and proving. The user, for example, is the primary source of problem domain facts and properties needed in the proofs. A general description is given of the overall design philosophy, structure, and functional components of the system, and a simple sorting program is used to illustrate both the behavior of major system components and the type of user interaction the system provides.
Type of Medium:
Online Resource
ISSN:
0362-1340
,
1558-1160
DOI:
10.1145/390016.808472
Language:
English
Publisher:
Association for Computing Machinery (ACM)
Publication Date:
1975
detail.hit.zdb_id:
2079194-X
detail.hit.zdb_id:
282422-X
Bookmarklink