Wilmer Ricciotti
Jan Stolarek
Abstract
Program slicing provides explanations that illustrate how program outputs were produced from inputs. We build on an approach introduced in prior work, where dynamic slicing was defined for pure higher-order functional programs as a Galois connection between lattices of partial inputs and partial outputs. We extend this approach to imperative functional programs that combine higher-order programming with references and exceptions. We present proofs of correctness and optimality of our approach and a proof-of-concept implementation and experimental evaluation.
Supplemental Material
Available for Download
We provide a virtual machine in Open Virtual Appliance format supported by the most popular virtualization software (VirtualBox, VMWare). Our software is written in Haskell. Provided virtual machine comes with Glasgow Haskell Compiler 8.0.2 and all the libraries required to compile our program. You can also visit online repository to find the latest version of our source code: https://github.com/jstolarek/slicer or the exact version submitted to the ICFP 2017: https://github.com/jstolarek/slicer/tree/icfp2017
- Umut A. Acar, Amal Ahmed, James Cheney, and Roly Perera. A core calculus for provenance. Journal of Computer Security, 21:919–969, 2013. Full version of a POST 2012 paper.Google Scholar
Digital Library
- Jean-Francois Bergeretti and Bernard A. Carré. Information-flow and data-flow analysis of while-programs. ACM Trans. Program. Lang. Syst., 7(1):37–61, January 1985. ISSN 0164-0925. doi: 10.1145/2363.2366. URL Google ScholarDigital Library
- S. Biswas. Dynamic Slicing in Higher-Order Programming Languages. PhD thesis, University of Pennsylvania, 1997.Google ScholarDigital Library
- Arthur Charguéraud. Pretty-big-step semantics. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Proceedings, pages 41–60, 2013. doi: 10.1007/978-3-642-37036-6_3. URL Google ScholarDigital Library
- James Cheney, Amal Ahmed, and Umut A. Acar. Database queries that explain their work. In Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming (PPDP), pages 271–282, 2014. Google ScholarDigital Library
- Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’77, pages 238–252, New York, NY, USA, 1977. ACM. doi: 10.1145/512950.512973. URL Google ScholarDigital Library
- David Darais and David Van Horn. Constructive Galois connections: Taming the Galois connection framework for mechanized metatheory. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 311–324, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-4219-3. doi: 10.1145/2951913.2951934. URL Google ScholarDigital Library
- B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 2002. Google ScholarCross Ref
- John Field and Frank Tip. Dynamic dependence in term rewriting systems and its application to program slicing. Information and Software Technology, 40(11–12):609–636, November/December 1998. Google ScholarCross Ref
- Nate Foster, Kazutaka Matsuda, and Janis Voigtländer. Three complementary approaches to bidirectional programming. In Jeremy Gibbons, editor, Spring School on Generic and Indexed Programming, volume 7470, pages 1–46. Springer, 2010. doi: 10.1007/978- 3- 642- 32202- 0_1.Google Scholar
- Ronald Garcia, Alison M. Clark, and Éric Tanter. Abstracting gradual typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’16, pages 429–442, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-3549-2. doi: 10.1145/2837614.2837670. URL Google ScholarDigital Library
- Christian Haack and J. B. Wells. Type error slicing in implicitly typed higher-order languages. Sci. Comput. Program., 50(1-3): 189–224, March 2004. ISSN 0167-6423. doi: 10.1016/j.scico.2004.01.004. URL Google ScholarDigital Library
- Amir Kishon and Paul Hudak. Semantics directed program execution monitoring. J. Funct. Prog., 5(4):501–547, 1995. doi: 10.1017/S0956796800001465. Google ScholarCross Ref
- Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. Comput., 185(2):182–210, September 2003. ISSN 0890-5401. doi: 10.1016/S0890-5401(03)00088-9. URL Google ScholarDigital Library
- Ian MacLarty, Zoltan Somogyi, and Mark Brown. Divide-and-query and subterm dependency tracking in the mercury declarative debugger. In Proceedings of the Sixth International Symposium on Automated Analysis-driven Debugging, AADEBUG’05, pages 59–68, New York, NY, USA, 2005. ACM. ISBN 1-59593-050-7. doi: 10.1145/1085130.1085138. URL Google ScholarDigital Library
- Claudio Ochoa, Josep Silva, and Germán Vidal. Dynamic slicing of lazy functional programs based on redex trails. Higher Order Symbol. Comput., 21(1-2):147–192, 2008. ISSN 1388-3690. doi:Google ScholarDigital Library
- Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer. Hazelnut: A bidirectionally typed structure editor calculus. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, pages 86–99, New York, NY, USA, 2017. ACM. ISBN 978-1-4503-4660-3. doi: 10.1145/3009837.3009900. URL Google ScholarDigital Library
- Roland Perera. Interactive Functional Programming. PhD thesis, University of Birmingham, Birmingham, UK, July 2013. http://etheses.bham.ac.uk/4209/ .Google Scholar
- Roly Perera, Umut A. Acar, James Cheney, and Paul Blain Levy. Functional programs that explain their work. In ICFP, pages 365–376, New York, NY, USA, 2012. ACM. Google ScholarDigital Library
- Roly Perera, Deepak Garg, and James Cheney. Causally consistent dynamic slicing. In 27th International Conference on Concurrency Theory (CONCUR 2016), pages 18:1–18:15, 2016.Google Scholar
- Justin Pombrio and Shriram Krishnamurthi. Resugaring: Lifting evaluation sequences through syntactic sugar. In Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, pages 361–371, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2784-8. doi: 10.1145/2594291.2594319. URL Google ScholarDigital Library
- Justin Pombrio and Shriram Krishnamurthi. Hygienic resugaring of compositional desugaring. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 75–87, New York, NY, USA, 2015. ACM. ISBN 978-1-4503-3669-7. doi: 10.1145/2784731.2784755. URL Google ScholarDigital Library
- Nuno F. Rodrigues and Luís S. Barbosa. Higher-order lazy functional slicing. Journal of Universal Computer Science, 13(6): 854–873, June 2007.Google Scholar
- Eric L. Seidel, Ranjit Jhala, and Westley Weimer. Dynamic witnesses for static type errors (or, ill-typed programs usually go wrong). In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pages 228–242, New York, NY, USA, 2016. ACM. ISBN 978-1-4503-4219-3. doi: 10.1145/2951913.2951915. URL Google ScholarDigital Library
- Josep Silva and Olaf Chitil. Combining algorithmic debugging and program slicing. In PPDP, pages 157–166, 2006. Google ScholarDigital Library
- Meng Wang, Jeremy Gibbons, and Nicolas Wu. Incremental updates for efficient bidirectional transformations. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, pages 392–403, 2011. doi: 10.1145/2034773.2034825. URL Google ScholarDigital Library
- Mark Weiser. Program slicing. In ICSE, pages 439–449, 1981.Google ScholarDigital Library
- Baowen Xu, Ju Qian, Xiaofang Zhang, Zhongqiang Wu, and Lin Chen. A brief survey of program slicing. SIGSOFT Softw. Eng. Notes, 30:1–36, March 2005. ISSN 0163-5948. doi: Google ScholarDigital Library
Index Terms
- Imperative functional programs that explain their work
Recommendations
Functional programs that explain their work
ICFP '12We present techniques that enable higher-order functional computations to "explain" their work by answering questions about how parts of their output were calculated. As explanations, we consider the traditional notion of program slices, which we show ...
Functional programs that explain their work
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programmingWe present techniques that enable higher-order functional computations to "explain" their work by answering questions about how parts of their output were calculated. As explanations, we consider the traditional notion of program slices, which we show ...
A brief survey of program slicing
Program slicing is a technique to extract program parts with respect to some special computation. Since Weiser first proposed the notion of slicing in 1979, hundreds of papers have been presented in this area. Tens of variants of slicing have been ...
Comments