Abstract
Common programming tools, like compilers, debuggers, and IDEs, crucially rely on the ability to analyse program code to reason about its behaviour and properties. There has been a great deal of work on verifying compilers and static analyses, but far less on verifying dynamic analyses such as program slicing. Recently, a new mathematical framework for slicing was introduced in which forward and backward slicing are dual in the sense that they constitute a Galois connection. This paper formalises forward and backward dynamic slicing algorithms for a simple imperative programming language, and formally verifies their duality using the Coq proof assistant.
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
Similar content being viewed by others
Notes
- 1.
In the literature Imp is also referred to as WHILE.
- 2.
We overload the \(\Rightarrow \) notation to mean one of three evaluation relations. It is always clear from the arguments which relation we are referring to.
- 3.
We again overload \(\nearrow \) and \(\searrow \) arrows in the notation to denote one of three forward/backward slicing relations. This is important in the rules for boolean slicing, whose premises refer to the slicing relation for arithmetic expressions, and command slicing, whose premises refer to slicing relation for boolean expressions.
- 4.
When some partial value v is used as a slicing criterion we say that we “slice w.r.t. v”.
- 5.
This example is adapted from [9].
- 6.
Name comes from a term “prefix set” introduced in [17] to refer to a set of all partial values smaller than a given value. So a prefix set of a top element of a lattice denotes a set of all elements in that (complete) lattice.
- 7.
In order to make the code snippets in the paper easier to read we omit the ordering relation when indexing prefix.
- 8.
Authors of [9] use the name WHILE, but the language is the same.
References
Backhouse, R.: Galois connections and fixed point calculus. In: Backhouse, R., Crole, R., Gibbons, J. (eds.) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. LNCS, vol. 2297, pp. 89–150. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-47797-7_4
Binkley, D., Danicic, S., Gyimóthy, T., Harman, M., Kiss, A., Korel, B.: A formalisation of the relationship between forms of program slicing. Sci. Comput. Program. 62(3), 228–252 (2006). Special issue on Source code analysis and manipulation (SCAM 2005)
Blazy, S., Maroneze, A., Pichardie, D.: Verified validation of program slicing. In: Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP 2015, pp. 109–117. ACM, New York (2015)
Cheney, J., Acar, U.A., Perera, R.: Toward a theory of self-explaining computation. In: Tannen, V., Wong, L., Libkin, L., Fan, W., Tan, W.-C., Fourman, M. (eds.) In Search of Elegance in the Theory and Practice of Computation. LNCS, vol. 8000, pp. 193–216. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-41660-6_9
Chiang, Y., Mu, S.: Formal derivation of greedy algorithms from relational specifications: a tutorial. J. Log. Algebr. Meth. Program. 85(5), 879–905 (2016). https://doi.org/10.1016/j.jlamp.2015.12.003
Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. Cambridge University Press, Cambridge (2002)
Gibbons, J.: Fission for program comprehension. In: Proceedings of Mathematics of Program Construction, 8th International Conference, MPC 2006, Kuressaare, Estonia, 3–5 July 2006, pp. 162–179 (2006). https://doi.org/10.1007/11783596_12
Korel, B., Laski, J.: Dynamic program slicing. Inf. Process. Lett. 29(3), 155–163 (1988)
Léchenet, J., Kosmatov, N., Gall, P.L.: Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects Comput. 30(1), 107–131 (2018)
Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: Compcert - a formally verified optimizing compiler. In: ERTS 2016: Embedded Real Time Software and Systems. SEE (2016)
Mu, S., Ko, H., Jansson, P.: Algebra of programming in Agda: dependent types for relational program derivation. J. Funct. Program. 19(5), 545–579 (2009). https://doi.org/10.1017/S0956796809007345
Mu, S., Oliveira, J.N.: Programming from Galois connections. J. Log. Algebr. Program. 81(6), 680–704 (2012). https://doi.org/10.1016/j.jlap.2012.05.003
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-662-03811-6
Perera, R., Garg, D., Cheney, J.: Causally consistent dynamic slicing. In: CONCUR, pp. 18:1–18:15 (2016)
Perera, R., Acar, U.A., Cheney, J., Levy, P.B.: Functional programs that explain their work. In: ICFP, pp. 365–376. ACM (2012)
Pierce, B.C., et al.: Software Foundations. Electronic textbook (2017), version 5.0. http://www.cis.upenn.edu/~bcpierce/sf
Ricciotti, W., Stolarek, J., Perera, R., Cheney, J.: Imperative functional programs that explain their work. In: Proceedings of the ACM on Programming Languages (PACMPL) 1(ICFP), September 2017
Silva, J.: An analysis of the current program slicing and algorithmic debugging based techniques. Technical University of Valencia, Tech. rep. (2008)
Stolarek, J.: Verified self-explaining computation, May 2019. https://bitbucket.org/jstolarek/gc_imp_slicing/src/mpc_2019_submission/
The Coq Development Team: The Coq proof assistant, version 8.7.0, October 2017. https://doi.org/10.5281/zenodo.1028037
Weiser, M.: Program slicing. In: ICSE, pp. 439–449. IEEE Press, Piscataway (1981)
Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)
Acknowledgements
We gratefully acknowledge help received from Wilmer Ricciotti during our work on the Coq formalisation, and Jeremy Gibbons for comments on a draft. This work was supported by ERC Consolidator Grant Skye (grant number 682315).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Stolarek, J., Cheney, J. (2019). Verified Self-Explaining Computation. In: Hutton, G. (eds) Mathematics of Program Construction. MPC 2019. Lecture Notes in Computer Science(), vol 11825. Springer, Cham. https://doi.org/10.1007/978-3-030-33636-3_4
Download citation
DOI: https://doi.org/10.1007/978-3-030-33636-3_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-33635-6
Online ISBN: 978-3-030-33636-3
eBook Packages: Computer ScienceComputer Science (R0)