An official website of the United States government
In this paper we generalise the notion of extensional (functional) equivalence of programs to abstract equivalences induced by abstract interpretations. The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalised forms. On the other hand, the generalised framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and only if they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code ransformations. To construct these transformations, we introduce a novel technique for building incompleteness cliques of extensionally equivalent yet abstractly distinguishable programs: They are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow ransformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis.
more »
« less
Checking equivalence in a non-strict language
Program equivalence checking is the task of confirming that two programs have the same behavior on corresponding inputs. We develop a calculus based on symbolic execution and coinduction to check the equivalence of programs in a non-strict functional language. Additionally, we show that our calculus can be used to derive counterexamples for pairs of inequivalent programs, including counterexamples that arise from non-termination. We describe a fully automated approach for finding both equivalence proofs and counterexamples. Our implementation, Nebula, proves equivalences of programs written in Haskell. We demonstrate Nebula's practical effectiveness at both proving equivalence and producing counterexamples automatically by applying Nebula to existing benchmark properties.
more »
« less
- Award ID(s):
- 2131476
- PAR ID:
- 10387956
- Date Published:
- Journal Name:
- Proceedings of the ACM on Programming Languages
- Volume:
- 6
- Issue:
- OOPSLA2
- ISSN:
- 2475-1421
- Page Range / eLocation ID:
- 1469 to 1496
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Similarity analysis plays a crucial role in various software engineering tasks, such as detecting software changes, version merging, identifying plagiarism, and analyzing binary code. Equivalence analysis, a stricter form of similarity, focuses on determining whether different programs or versions of the same program behave identically. While extensive research exists on code and binary similarity as well as equivalence analysis, there is a lack of quantitative reasoning in these areas. Non-equivalence is a spectrum that requires deeper exploration, as it can manifest in different ways across the input domain space. This paper emphasizes the importance of quantitative reasoning on non-equivalence which arises due to semantic differences. By quantitatively reasoning about non-equivalence, it becomes possible to identify specific input ranges for which programs are equivalent or non-equivalent. We aim to address the gap in quantitative reasoning in symbolic similarity analysis, enabling a more comprehensive understanding of program behavior.more » « less
-
Karunakaran, S. S.; & Higgins, A. (Ed.)This paper describes a model of student thinking around equivalence (conceptualized as any type of equivalence relation), presenting vignettes from student conceptions from various college courses ranging from developmental to linear algebra, and courses in between (e.g., calculus). In this model, we conceptualize student definitions along a continuous plane with two dimensions: the extent to which definitions are extracted vs. stipulated; and the extent to which conceptions of equivalence are operational or structural. We present examples to illustrate how this model may help us to recognize ill-defined or limited thinking on the part of students even when they appear to be able to provide “standard” definitions of equivalence, as well as to highlight cases in which students are providing mathematically valid, if non-standard, definitions of equivalence. We hope that this framework will serve as a useful tool for analyzing student work, as well as exploring instructional and curricular handling of equivalence.more » « less
-
Over the last several decades, Emerging Scholars Programs (ESPs) have incorporated active learning strategies and challenging problems into collegiate mathematics, resulting in students, underrepresented minority (URM) students in particular, earning at least half of a letter grade higher than other students in Calculus. In 2009, West Virginia University (WVU) adapted ESP models for use in Calculus I in an effort to support the success and retention of URM STEM students by embedding group and inquiry-based learning into a designated section of Calculus I. Seats in the class were reserved for URM and first-generation students. We anticipated that supporting students in courses in the calculus sequence, including Calculus I, would support URM Calculus I students in building learning communities and serve as a mechanism to provide a strong foundation for long-term retention. In this study we analyze the success of students that have progressed through our ESP Calculus courses and compare them to their non-ESP counterparts. Results show that ESP URM students succeed in the Calculus sequence at substantially higher rates than URM students in non-ESP sections of Calculus courses in the sequence (81% of URM students pass ESP Calculus I while only 50% of URM students pass non-ESP Calculus I). In addition, ESP URM and ESP non-URM (first-generation but not URM) students succeed at similar levels in the ESP Calculus sequence of courses (81% of URM students and 82% of non-URM students pass ESP Calculus I). Finally, ESP URM students’ one-year retention rates are similar to those of ESP non-URM students and significantly higher than those of URM students in non-ESP sections of Calculus (92% of ESP URM Calculus I students were retained after one year, while only 83% of URM non-ESP Calculus I students were retained). These results suggest that ESP is ideally suited for retaining and graduating URM STEM majors, helping them overcome obstacles and barriers in STEM, and increasing diversity, equity, and inclusion in Calculus.more » « less
-
null (Ed.)Abstract Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. Sound gradually typed languages dynamically check types at runtime at the boundary between statically typed and dynamically typed modules. However, there is much disagreement in the gradual typing literature over how to enforce complex types such as tuples, lists, functions and objects. In this paper, we propose a new perspective on the design of runtime gradual type enforcement: runtime type casts exist precisely to ensure the correctness of certain type-based refactorings and optimizations. For instance, for simple types, a language designer might desire that beta-eta equality is valid. We show that this perspective is useful by demonstrating that a cast semantics can be derived from beta-eta equality. We do this by providing an axiomatic account program equivalence in a gradual cast calculus in a logic we call gradual type theory (GTT). Based on Levy’s call-by-push-value, GTT allows us to axiomatize both call-by-value and call-by-name gradual languages. We then show that we can derive the behavior of casts for simple types from the corresponding eta equality principle and the assumption that the language satisfies a property called graduality , also known as the dynamic gradual guarantee. Since we can derive the semantics from the assumption of eta equality, we also receive a useful contrapositive: any observably different cast semantics that satisfies graduality must violate the eta equality. We show the consistency and applicability of our axiomatic theory by proving that a contract-based implementation using the lazy cast semantics gives a logical relations model of our type theory, where equivalence in GTT implies contextual equivalence of the programs. Since GTT also axiomatizes the dynamic gradual guarantee, our model also establishes this central theorem of gradual typing. The model is parameterized by the implementation of the dynamic types, and so gives a family of implementations that validate type-based optimization and the gradual guarantee.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1145/3563340
