Papers
2024
- Equivalent Mutants in the Wild: Identifying and Efficiently Suppressing Equivalent Mutants for Java ProgramsIn Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis, 2024
The presence of equivalent mutants has long been considered a major obstacle to the widespread adoption of mutation analysis and mutation testing. This paper presents a study on the types and prevalence of equivalent mutants in real-world Java programs. We conducted a ground-truth analysis of 1,992 mutants, sampled from 7 open source Java projects. Our analysis identified 215 equivalent mutants, which we grouped based on two criteria that describe why the mutants are equivalent and how challenging their detection is. From this analysis, we observed that (1) the median equivalent mutant rate across the 7 projects is 2.97%; (2) many equivalent mutants are caused by common programming patterns and their detection is not much more complex than structural pattern matching over an abstract syntax tree. Based on the findings of our ground-truth analysis, we developed Equivalent Mutant Suppression (EMS), a technique that comprises 10 efficient and targeted analyses. We evaluated EMS on 19 open- source Java projects, comparing the effectiveness and efficiency of EMS to two variants of Trivial Compiler Equivalence (TCE), the current state of the art in equivalent mutant detection. Additionally, we analyzed all 9,047 equivalent mutants reported by any tool to better understand the types and frequencies of equivalent mutants found. Overall, EMS detects 8,776 equivalent mutants within 325 seconds; TCE detects 2,124 equivalent mutants in 2,938 hours.
2023
- Live Pattern Matching with Typed HolesProc. ACM Program. Lang., 2023
Several modern programming systems, including GHC Haskell, Agda, Idris, and Hazel, support typed holes. Assigning static and, to varying degree, dynamic meaning to programs with holes allows program editors and other tools to offer meaningful feedback and assistance throughout editing, i.e. in a live manner. Prior work, however, has considered only holes appearing in expressions and types. This paper considers, from type theoretic and logical first principles, the problem of typed pattern holes. We confront two main difficulties, (1) statically reasoning about exhaustiveness and irredundancy when patterns are not fully known, and (2) live evaluation of expressions containing both pattern and expression holes. In both cases, this requires reasoning conservatively about all possible hole fillings. We develop a typed lambda calculus, Peanut, where reasoning about exhaustiveness and redundancy is mapped to the problem of deriving first order entailments. We equip Peanut with an operational semantics in the style of Hazelnut Live that allows us to evaluate around holes in both expressions and patterns. We mechanize the metatheory of Peanut in Agda and formalize a procedure capable of deciding the necessary entailments. Finally, we scale up and implement these mechanisms within Hazel, a programming environment for a dialect of Elm that automatically inserts holes during editing to provide static and dynamic feedback to the programmer in a maximally live manner, i.e. for every possible editor state. Hazel is the first maximally live environment for a general-purpose functional language.
2022
- Contextualized Programming Language DocumentationIn Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, 2022
Learning the syntax and semantics of a new programming language is a challenge. It is common for learners to refer to language documentation many times and in many contexts as they build comfort and understanding. We review existing functional language documentation, finding that it tends to be organized according to the structure of the language. Each section interleaves narrative explanations, which introduce precise terminology that is then used consistently, with code examples. Sections often start with simpler special cases of a construct before considering it in full generality. To make use of language documentation, learners must step away from the code they are working with, e.g., in an exercise or tutorial, to locate and transfer knowledge from the documentation. We describe a system, ExplainThis, that automatically generates contextualized language documentation, structured based on our study of language documentation but specialized to the particular code at the cursor. This system is integrated into the structure editor of Hazel, a live functional environment. Documentation appears next to the editor and color is used as secondary notation to correlate the explanation with program terms. We also study syntactic and explanatory specificity with a formative user study. We find that participants desire documentation to be tailored to specific syntax of the code a user is working with, while allowing an adaptive level of specificity for code examples.
2020
- Hazel Tutor: Guiding Novices Through Type-Driven Development StrategiesHannah Potter, and Cyrus Omar2020
Hazel Tutor is a work-in-progress editor service for the Hazel programming environment designed to interactively help novices learn type-driven development strategies as they construct, edit, and debug code. The system provides both feedback and, when requested, suggestions on the basis of type information available at the cursor. Hazel is able to supply the Hazel Tutor with the necessary information at all times, including when there are holes in the program. When the cursor is on an empty hole, the system organizes the suggestions based on the type-driven development strategy that we aim to teach students. We are beginning to work on presenting debugging strategies when on an error hole. We outline our hypotheses, specific research questions of interest, and planned future studies.