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.
Similar content being viewed by others
References
Burstall, R.M.: Program proving with hand simulation and a little induction. In: Information processing, Vol. 74, pp. 308–312. North Holland 1974
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
Dijkstra, E.W.: Cooperating sequential processes. In: Programming languages (F. Genuys, ed.), pp. 43–112. New York-London: Academic Press 1968
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
Francez, N.: The analysis of cyclic programs. Dept. of Applied Maths., The Weizmann Institute of Science, Rehovat, Israel, Ph.D. Thesis, July 1976
Gilbert, P., Chander, W.J.: Interference between communicating parallel processes. Comm. ACM 15, 427–137 (1972)
Hoare, C.A.R.: Private communication
Manna, Z.: Mathematical theory of computation. New York: McGraw Hill 1974
Milner, R.: Processes — a mathematical model of computing agents. Proceedings of the Logic Colloquium, Bristol, pp. 157–173. North Holland 1973
Newton, G.: Proving properties of interacting processes. Acta Informat. 4, 117–126 (1975)
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. I. Acta Informat. 6, 319–340 (1976)
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
Author information
Authors and Affiliations
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
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
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00289074