×

Syntax directed analysis of liveness properties of while programs. (English) Zbl 0591.68016

Summary: A syntax directed proof system which allows to prove liveness properties of while-programs is introduced. The proof system is proved to be arithmetically sound and complete in the sense of D. Harel [First- order dynamic logic, Berlin (1979; Zbl 0403.03024)]. The results of the paper generalize a corresponding result A. Pnueli [Proc. 18th Sympos. FOCS, IEEE, Providence, R. I., 46-57 (1977)] proves for unstructured programs. The proof system decomposes into two parts. The first part allows to prove simple safety properties. These properties are used as axioms in the second proof system which deals with liveness properties. The completeness proof is constructive and provides a heuristic for proving specific liveness properties.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N01 General topics in the theory of software

Citations:

Zbl 0403.03024
PDFBibTeX XMLCite
Full Text: DOI