Nothing Special   »   [go: up one dir, main page]

Skip to main content
Log in

A proof method for cyclic programs

  • Published:
Acta Informatica Aims and scope Submit manuscript

Summary

We consider the specification and verification of cyclic (sequential and concurrent) programs. The input-output based concept of correctness traditionally applied to functional programs is replaced by another, based on the concept of eventual behaviour. Various types of eventual behaviour are introduced. In the case of concurrency, the introduction of interface-predicates reduces the proof complexity and achieves greater readability. All specifications use explicitly the auxiliary variables of a location counter π and elapsing time t.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Similar content being viewed by others

References

  1. Burstall, R.M.: Program proving with hand simulation and a little induction. In: Information processing, Vol. 74, pp. 308–312. North Holland 1974

  2. Dijkstra, E.W.: Hierarchical ordering of sequential processes. In: Operating systems techniques (C.A.R. Hoare, R.H. Perrott, eds.), pp. 72–93. New York-London: Academic Press 1972

    Google Scholar 

  3. Dijkstra, E.W.: Cooperating sequential processes. In: Programming languages (F. Genuys, ed.), pp. 43–112. New York-London: Academic Press 1968

    Google Scholar 

  4. Floyd, R.W.: Assigning meanings to programs. In: Proc. Symp. Applied Maths., Vol. 19, Aspects of computer science, pp. 19–32. New York: American Mathematical Society 1967

    Google Scholar 

  5. Francez, N.: The analysis of cyclic programs. Dept. of Applied Maths., The Weizmann Institute of Science, Rehovat, Israel, Ph.D. Thesis, July 1976

    Google Scholar 

  6. Gilbert, P., Chander, W.J.: Interference between communicating parallel processes. Comm. ACM 15, 427–137 (1972)

    Google Scholar 

  7. Hoare, C.A.R.: Private communication

  8. Manna, Z.: Mathematical theory of computation. New York: McGraw Hill 1974

    Google Scholar 

  9. Milner, R.: Processes — a mathematical model of computing agents. Proceedings of the Logic Colloquium, Bristol, pp. 157–173. North Holland 1973

    Google Scholar 

  10. Newton, G.: Proving properties of interacting processes. Acta Informat. 4, 117–126 (1975)

    Google Scholar 

  11. Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. I. Acta Informat. 6, 319–340 (1976)

    Google Scholar 

  12. Schwartz, J.: Event based reasoning — a system for proving correct termination of programs. Dept. of A.I., University of Edinburgh, D.A.I. Report No. 12, 1975

Download references

Author information

Authors and Affiliations

Authors

Additional information

The research of N.F. was partially supported by The Fund for Aiding Research, Histadrut, The Federation of Hebrew workers in Israel

Rights and permissions

Reprints and permissions

About this article

Cite this article

Francez, N., Pnueli, A. A proof method for cyclic programs. Acta Informatica 9, 133–157 (1978). https://doi.org/10.1007/BF00289074

Download citation

  • Received:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF00289074

Keywords

Navigation