×

zbMATH — the first resource for mathematics

Total correctness of CSP programs. (English) Zbl 0596.68026
Summary: In this paper we propose an axiomatic system for proving the total correctness of CSP programs. The system is based on the partial correctness system of the author, ACM Trans. Program. Lang. Syst. 6, 647- 662 (1984; Zbl 0542.68013). We use the proposed system to prove the total correctness of a program for set partitioning.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apt, K.R., Francez, N., de Roever, W.P.: A proof system for CSP. ACM TOPLAS 2, 359-385 (1980) · Zbl 0468.68023 · doi:10.1145/357103.357110
[2] Apt, K.R.: Formal justification for a proof system for CSP. J. Assoc. Comput. Mach. 30, 197-216 (1983) · Zbl 0503.68021
[3] Apt, K.R., Pneuli, A., Stavi, J.: Fair termination revisted with delay, in Proc. 2nd conf. FST and TCS. pp. 146-170, Bangalore, Tata Institute of Fundamental Research, Bombay 1982 (Also to appear in Theoret. Comput. Sci.)
[4] Levin, G., Gries, D.: A proof technique for CSP. Acta Inf. 15, 281-302 (1981) · Zbl 0463.68034 · doi:10.1007/BF00289266
[5] Manna, Z., Pneuli, A.: Axiomatic approach to total correctness of programs. Acta Inf. 3, 243-264 (1974) · Zbl 0302.68022 · doi:10.1007/BF00288637
[6] Soundararajan, N.: Axiomatic semantics of CSP. ACM TOPLAS 6, 647-662 (1984) · Zbl 0542.68013 · doi:10.1145/1780.1805
[7] Soundararajan, N., Dahl, O.J.: Partial correctness semantics of CSP. (To appear in BIT)
[8] Soundararajan, N.: Total correctness of CSP programs. Draft, 1984 · Zbl 0596.68026
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.