×

Proof theory for exception handling in a tasking environment. (English) Zbl 0706.68076

Summary: We develop a syntax-directed proof system for a fragment of Ada consisting of the essential features of tasking and exception handling. The proof system is based on a correctness formula for the robust specification of single-entry-multiple-exit structures that provides a unified framework for exception handling mechanisms in the presence of nondeterminism, concurrency and communication. The proof system uses the technique of cooperating proofs, which ws developed for proving the correctness of communicating sequential processes [K. R. Apt, N. Francez and W. P. de Roever, ACM Trans. Program. Lang. Syst. 2, 359-385 (1980; Zbl 0468.68023)] and extended to a concurrent fragment of Ada in R. Gerth and W. P. de Roever [Sci. Comput. Program. 4, 159-204 (1984; Zbl 0536.68009)]. We build upon the latter. The soundness and completeness are established formally in K. Lodaya [Proof theory for exception handling in distributed programs, Tech. Rep. CS- 87/30, TIFR (1987)]. The proof rules are structured so that exceptions can be used as a structured escape mechanism in accordance with the design objectives of Ada. Examples are given to show how the rules highlight the annotation required for establishing the robustness of Ada programs.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68Q55 Semantics in the theory of computing
68N15 Theory of programming languages

Software:

Ada95
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] American National Standards Institute, The programming language Ada Reference Manual, ANSI/MIL-STD-1815A (1983), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York
[2] Apt, K. R.; Francez, N.; DeRoever, W. P., A proof system for communicating sequential processes, ACM Trans. Prog. Lang. Syst., 2, 3, 359-385 (1980) · Zbl 0468.68023 · doi:10.1145/357103.357110
[3] Apt, K. R., Formal justification of a proof system for communicating sequential processes, JACM, 30, 1, 197-216 (1983) · Zbl 0503.68021 · doi:10.1145/322358.322372
[4] Apt, K. R.; Broy, M., Proving correctness of CSP programs — a tutorial, Control flow and data flow: concepts of distributed programming, 441-474 (1985), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0566.68018
[5] Arbib, M. A.; Alagic, S., Proof rules for gotos, Acta Informatica, 11, 139-148 (1978) · doi:10.1007/BF00264021
[6] Clint, M.; Hoare, C. A.R., Program proving: jumps and functions, Acta Informatica, 1, 214-224 (1972) · Zbl 0229.68003 · doi:10.1007/BF00288686
[7] Cristian, F., Correct and robust programs, IEEE Trans. Softw. Eng., 10, 2, 163-174 (1984) · Zbl 0532.68021 · doi:10.1109/TSE.1984.5010218
[8] DeBruin, A., Goto statements: semantics and deduction systems, Acta Informatica, 15, 385-424 (1981) · Zbl 0445.68005 · doi:10.1007/BF00264536
[9] Flint, R. S., An approach to modeling database activity (1984), Irvine: University of California, Irvine
[10] Gehani, N., Ada: an advanced introduction (1984), Englewood Cliffs: Prentice-Hall, Englewood Cliffs
[11] Gerth, R., A sound and complete Hoare axiomatization of the Ada rendezvous, 252-265 (1982), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York
[12] Gerth, R.; DeRoever, W. P., A proof system for concurrent Ada programs, Sci. Comput. Program, 4, 2, 159-204 (1984) · Zbl 0536.68009 · doi:10.1016/0167-6423(84)90018-2
[13] Gerth, R.; DeRoever, W. P., Proving monitors revisited: a first step towards verifying object-oriented systems, Fund. Inform., 9, 371-400 (1986) · Zbl 0617.68026
[14] Hoare, C. A.R., Communicating sequential processes, Commun. ACM, 21, 8, 666-677 (1978) · Zbl 0383.68028 · doi:10.1145/359576.359585
[15] Ichbiah, J., Rationale for the design of the programming language Ada, ACM Sigplan Notices, 14, 6-6 (1979)
[16] [Li82] Li, W.: An operational semantics for tasking and exception handling in Ada. Proc. Ada TEC82, Washington, 1982, pp. 138-151
[17] [Lod87] Lodaya, K.: Proof theory for exception handling in distributed programs. Ph.D. Thesis, Tech. Rep. CS-87/30. TIFR, 1987
[18] Luckham, D. C.; Polak, W., Ada exception handling: an axiomatic approach, ACM Trans. Prog. Lang. Syst., 2, 2, 225-233 (1980) · Zbl 0468.68014 · doi:10.1145/357094.357100
[19] Misra, J.; Chandy, K. M., Proofs of networks of processes, IEEE Trans. Softw. Eng., 7, 4, 417-426 (1981) · Zbl 0468.68030 · doi:10.1109/TSE.1981.230844
[20] Owicki, S. S.; Gries, D., An axiomatic technique for parallel programs I, Acta Informatica, 6, 319-340 (1976) · Zbl 0312.68011 · doi:10.1007/BF00268134
[21] Pandya, P. K., Compositional Verification of Distributed Programs (1988), Bombay: Tata Institute of Fundamental Research, Bombay
[22] [Plo81] Plotkin, G.D.: A structural approach to operational semantics. DAIMI FN-19. Arhus University 1981
[23] [Plo83] Plotkin, G.D.: An operational semantics for CSP. Proc. IFIP Conf. Formal Description of Programming Concepts II, Garmisch-Partenkirchen, 1983, pp. 199-225 · Zbl 0512.68012
[24] Zwiers, J.; DeRoever, W. P.; Van Emde Boas, P., Compositionality and concurrent networks: soundness and completeness of a proof system, 509-519 (1885), Berlin Heidelberg New York: Springer, Berlin Heidelberg New York · Zbl 0566.68014
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.