An axiomatization of the intermittent assertion method using temporal logic

Extended abstract
  • Krzysztof R. Apt
  • Carole Delporte
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 154)


The intermittent assertion method proposed by Burstall [B] and subsequently popularized by Manna and Waldinger [MW] is axiomatized using a fragment of temporal logic. The proposed proof system allows to reason about while-programs. The proof system is proved to be arithmetically sound and complete in the sense of Harel [H]. The results of the paper generalize a corresponding result of Pnueli

The system decomposes into two parts. The first part allows to prove liveness properties using as axioms theorems of the second part allowing to prove simple safety properties.

The completeness proof is constructive and provides a heuristic for proving specific limeness formulas.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [A]
    Apt, K.R., Ten Years of Hoare's logic, a survey, part I, TOPLAS, vol. 3,4, pp. 431–483, 1981.Google Scholar
  2. [B]
    Burstall, R.M., Program proving as hand simulation with a little induction, in: Proceedings IFIP 74, pp. 308–312, North Holland, Amsterdam, 1974.Google Scholar
  3. [H]
    Harel, D., First order dynamic logic, Lecture Notes in Computer Science, 68, Springer Verlag, 1979.Google Scholar
  4. [HP]
    Hennessy, M.C.B., Plotkin G.D., Full abstraction for a simple programming language, in: Proceedings 8th Symposium MFCS, Lecture Notes in Computer Science, 74, pp. 108–120, 1979.Google Scholar
  5. [Ho]
    Hoare, C.A.R., An axiomatic basis of computer programming, Communications ACM, vol. 12, 10, pp. 576–580, 583, 1969.Google Scholar
  6. [L]
    Lamport, L., The “Hoare Logic” of concurrent programs, Acta Informatica, vol. 14, 1, pp. 21–37, 1980.Google Scholar
  7. [MP1]
    Manna Z., Pnueli A., Verification of concurrent programs; The temporal framework, in: The Correctness Problem in Computer Science, International Lecture Series in Computer Science, Academic Press, London, 1981.Google Scholar
  8. [MP2]
    Manna Z., Pnueli A., Verification of concurrent programs; Temporal proof principles, in: Logic of Programs, Lecture Notes in Computer Science, 131, pp. 200–252, 1982.Google Scholar
  9. [MW]
    Manna Z., Waldinger R., Is “Sometime” sometimes better than “Always” ?, Communications ACM, vol. 21, 2, pp. 159–172, 1978.Google Scholar
  10. [OL]
    Owicki S., Lamport L., Proving liveness properties of concurrent programs, TOPLAS, vol. 4, 3, pp. 455–495, 1982.Google Scholar
  11. [P]
    Pnueli, A., The temporal logic of programs, in: Proceedings 18th Symposium FOCS, pp. 46–57, IEEE, Providence, R.l., 1977.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1983

Authors and Affiliations

  • Krzysztof R. Apt
    • 1
  • Carole Delporte
    • 2
  1. 1.LITP, Université Paris 7ParisFrance
  2. 2.LCR-ThomsonOrsayFrance

Personalised recommendations