×

zbMATH — the first resource for mathematics

Graph-based object-oriented Hoare logic. (English) Zbl 1390.68192
Liu, Zhiming (ed.) et al., Theories of programming and formal methods. Essays dedicated to Jifeng He on the occasion of his 70th birthday. Berlin: Springer (ISBN 978-3-642-39697-7/pbk). Lecture Notes in Computer Science 8051, 374-393 (2013).
Summary: We are happy to contribute to this volume of essays in honor of He Jifeng on the occasion of his 70th birthday. This work combines and extends two recent pieces of work that He Jifeng has made significant contributions: the rCOS relational semantics of object-oriented programs [J. He et al., Theor. Comput. Sci. 365, No. 1–2, 109–142 (2006; Zbl 1118.68049)] and the trace model for pointers and objects [C. A. R. Hoare and J. He, NATO ASI Ser., Ser. F, Comput. Syst. Sci. 3–23, 3–23 (1999; Zbl 0954.68045)]. It presents a graph-based Hoare logic that deals with most general constructs of object-oriented (oo) programs such as assignment, object creation, local variable declaration and (possibly recursive) method invocation. The logic is built on a graph-based operational semantics of oo programs so that assertions are formalized as properties on graphs of execution states. We believe the logic is simple because 1) the use of graphs provides an intuitive visualization of states and executions of oo programs and thus it is helpful in thinking of and formulating clear specifications, 2) the logic follows almost the whole traditional Hoare logic and the only exception is the backward substitution law which is not valid for oo programs, and 3) the mechanical implementation of the logic would not be much more difficult than traditional Hoare logic. Despite the simplicity, the logic is powerful enough to reason about important oo properties such as aliasing and reachability.
For the entire collection see [Zbl 1269.68023].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q55 Semantics in the theory of computing
Software:
rCOS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apt, K., de Bakker, J.: Semantics and proof theory of pascal procedures. In: Salomaa, A., Steinby, M. (eds.) ICALP 1977. LNCS, vol. 52, pp. 30–44. Springer, Heidelberg (1977) · Zbl 0353.68036 · doi:10.1007/3-540-08342-1_3
[2] Chen, Z., Liu, Z., Ravn, A.P., Stolz, V., Zhan, N.: Refinement and verification in component-based model driven design. Science of Computer Programming 74(4), 168–196 (2009) · Zbl 1178.68158 · doi:10.1016/j.scico.2008.08.003
[3] Corradini, A., Dotti, F.L., Foss, L., Ribeiro, L.: Translating java code to graph transformation systems. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 383–398. Springer, Heidelberg (2004) · Zbl 1116.68382 · doi:10.1007/978-3-540-30203-2_27
[4] He, J., Liu, Z., Li, X.: rCOS: A refinement calculus of object systems. Theor. Comput. Sci. 365(1-2), 109–142 (2006) · Zbl 1118.68049 · doi:10.1016/j.tcs.2006.07.034
[5] Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969) · Zbl 0179.23105 · doi:10.1145/363235.363259
[6] Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. In: Symposium on Semantics of Algorithmic Languages. Lecture Notes in Mathematics, vol. 188, pp. 102–116. Springer (1971) · Zbl 0221.68020
[7] Hoare, C.A.R., He, J.: A trace model for pointers and objects. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, pp. 1–17. Springer, Heidelberg (1999) · Zbl 0954.68045 · doi:10.1007/3-540-48743-3_1
[8] Kastenberg, H., Kleppe, A., Rensink, A.: Defining object-oriented execution semantics using graph transformations. In: Gorrieri, R., Wehrheim, H. (eds.) FMOODS 2006. LNCS, vol. 4037, pp. 186–201. Springer, Heidelberg (2006) · doi:10.1007/11768869_15
[9] Ke, W., Liu, Z., Wang, S., Zhao, L.: A graph-based operational semantics of OO programs. In: Breitman, K., Cavalcanti, A. (eds.) ICFEM 2009. LNCS, vol. 5885, pp. 347–366. Springer, Heidelberg (2009) · Zbl 05635818 · doi:10.1007/978-3-642-10373-5_18
[10] Ke, W., Liu, Z., Wang, S., Zhao, L.: Graph-based type system, operational semantics and implementation of an object-oriented programming language. Technical Report 410, UNU-IIST, P.O. Box 3058, Macau (2009), http://www.iist.unu.edu/www/docs/techreports/reports/report410.pdf
[11] Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994) · doi:10.1145/177492.177726
[12] Liu, Z., Morisset, C., Stolz, V.: rCOS: theory and tools for component-based model driven development. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 62–80. Springer, Heidelberg (2010) · Zbl 05663805 · doi:10.1007/978-3-642-11623-0_3
[13] Parkinson, M., Bierman, G.: Separation logic and abstraction. In: POPL 2005, pp. 247–258. ACM, New York (2005) · Zbl 1369.68151
[14] Pierik, C., de Boer, F.S.: A syntax-directed Hoare logic for object-oriented programming concepts. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 64–78. Springer, Heidelberg (2003) · Zbl 1253.68087 · doi:10.1007/978-3-540-39958-2_5
[15] Poetzsch-Heffter, A., Müller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999) · doi:10.1007/3-540-49099-X_11
[16] Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55–74. IEEE Computer Society (2002) · doi:10.1109/LICS.2002.1029817
[17] von Oheimb, D., Nipkow, T.: Hoare logic for NanoJava: Auxiliary variables, side effects and virtual methods revisited. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 89–105. Springer, Heidelberg (2002) · Zbl 1064.68543 · doi:10.1007/3-540-45614-7_6
[18] Zhao, L., Liu, X., Liu, Z., Qiu, Z.: Graph transformations for object-oriented refinement. Formal Aspects of Computing 21(1-2), 103–131 (2009) · Zbl 1165.68025 · doi:10.1007/s00165-007-0067-y
[19] Zhao, L., Wang, S., Liu, Z.: Graph-based object-oriented Hoare logic. Technical Report 458, UNU-IIST, P.O. Box 3058, Macau (2012), http://iist.unu.edu/sites/iist.unu.edu/files/biblio/report458.pdf · Zbl 1390.68192
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.