[OOPSLA23] Explainable Program Synthesis by Localizing Specifications

Описание: Explainable Program Synthesis by Localizing Specifications (Video, OOPSLA2 2023)
Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, and Mukund Raghothaman
(University of Southern California, USA; University of Southern California, USA; Purdue University, USA; Microsoft, USA; University of Southern California, USA)

Abstract: The traditional formulation of the program synthesis problem is to find a program that meets a logical correctness specification. When synthesis is successful, there is a guarantee that the implementation satisfies the specification. Unfortunately, synthesis engines are typically monolithic algorithms, and obscure the correspondence between the specification, implementation and user intent. In contrast, humans often include comments in their code to guide future developers towards the purpose and design of different parts of the codebase. In this paper, we introduce subspecifications as a mechanism to augment the synthesized implementation with explanatory notes of this form. In this model, the user may ask for explanations of different parts of the implementation; the subspecification generated in response is a logical formula that describes the constraints induced on that subexpression by the global specification and surrounding implementation. We develop algorithms to construct and verify subspecifications and investigate their theoretical properties. We perform an experimental evaluation of the subspecification generation procedure, and measure its effectiveness and running time. Finally, we conduct a user study to determine whether subspecifications are useful: we find that subspecifications greatly aid in understanding the global specification, in identifying alternative implementations, and in debugging faulty implementations.

Article: https://doi.org/10.1145/3622874

Supplementary archive: https://doi.org/10.5281/zenodo.8331495 (Badges: Artifacts Available, Artifacts Evaluated — Reusable)

ORCID: https://orcid.org/0009-0000-5675-247X, https://orcid.org/0009-0006-5675-4065, https://orcid.org/0009-0000-2456-217X, https://orcid.org/0000-0002-5559-5932, https://orcid.org/0000-0003-2879-0932

Video Tags: Program synthesis, program comprehension, explainability, oopslab23main-p769-p, doi:10.1145/3622874, doi:10.5281/zenodo.8331495, orcid:0009-0000-5675-247X, orcid:0009-0006-5675-4065, orcid:0009-0000-2456-217X, orcid:0000-0002-5559-5932, orcid:0000-0003-2879-0932, Artifacts Available, Artifacts Evaluated — Reusable

Presentation at the OOPSLA2 2023 conference, October 22–27, 2023, https://2023.splashcon.org/track/spla...
Sponsored by ACM SIGPLAN,