Abstract
This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Program configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use of the matching logic proof system is equivalent to IMP’s Hoare logic proof system, in that any proof derived using either can be turned into a proof using the other. Extensions to IMP including a heap with dynamic memory allocation and pointer arithmetic are given, requiring no extension of the underlying first-order logic; moreover, heap patterns such as lists, trees, queues, graphs, etc., are given algebraically using fist-order constraints over patterns.
Supported in part by NSF grants CCF-0916893, CNS-0720512, and CCF-0448501, by NASA contract NNL08AA23C, by a Samsung SAIT grant, and by several Microsoft gifts.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)
Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. Tech. Rep. MSR-TR-2009-15, Microsoft Research (2009)
Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)
Distefano, D., Parkinson, M.J.: jStar: Towards practical verification for Java. In: OOPSLA 2008, pp. 213–226 (2008)
Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002, pp. 234–245 (2002)
Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Proceedings of the Symposium on Applied Mathematics, 19th edn., pp. 19–32. AMS, Providence (1967)
Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)
Gordon, M., Collavizza, H.: Forward with Hoare. In: Reflections on the Work of C.A.R. Hoare. History of Computing Series, Springer, Heidelberg (2010)
Gries, D.: The Schorr-Waite graph marking algorithm. Acta Informatica 11, 223–232 (1979)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Handbook of Philosophical Logic, pp. 497–604 (1984)
Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12(10), 576–580 (1969)
Hubert, T., Marché, C.: A case study of C source code verification: The Schorr-Waite algorithm. In: SEFM 2005, pp. 190–199 (2005)
Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL 2006, pp. 115–126 (2006)
Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S.: Simulating reachability using first-order logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 99–115. Springer, Heidelberg (2005)
Loginov, A., Reps, T., Sagiv, M.: Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 261–279. Springer, Heidelberg (2006)
Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoretical Computer Science 373(3), 213–237 (2007)
Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. SIGPLAN Not. 36(5), 221–231 (2001)
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics. Formal Aspects of Computing 10(2), 171–186 (1998)
O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5, 215–244 (1999)
Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: ASE 2001, pp. 157–165 (2001)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55–74 (2002)
Roşu, G., Schulte, W.: Matching logic–Extended report. Tech. Rep. UIUCDCS-R-2009-3026, University of Illinois (2009)
Roşu, G., Ellison, C., Schulte, W.: From rewriting logic executable semantics to matching logic program verification. Tech. Rep. UIUC (2009), http://hdl.handle.net/2142/13159
Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Roşu, G., Ellison, C., Schulte, W. (2011). Matching Logic: An Alternative to Hoare/Floyd Logic. In: Johnson, M., Pavlovic, D. (eds) Algebraic Methodology and Software Technology. AMAST 2010. Lecture Notes in Computer Science, vol 6486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17796-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-17796-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17795-8
Online ISBN: 978-3-642-17796-5
eBook Packages: Computer ScienceComputer Science (R0)