Constrictor: Immutability as a Design Concept
This program is tentative and subject to change.
Many object-oriented applications in algorithm design rely on objects never changing during their lifetime. This is often tackled by marking object references as read-only, e.g., using the const keyword in C++. In other languages like Python or Java where such a concept does not exist, programmers rely on best practices that are entirely unenforced. While reliance on best practices is obviously too permissive, const-checking is too restrictive: it is possible for a method to mutate the internal state while still satisfying the property we expect from an ``immutable'' object in this setting. We would therefore like to enforce the immutability of an object’s abstract state.
We check an object’s immutability through a view of its abstract state: for instances of an immutable class, the view does not change when running any of the class’s methods, even if some of the internal state does change. If all methods of a class are verified as non-mutating, we can deem the entire class view-immutable. We present an SMT-based algorithm to check view-immutability, and implement it in our linter/verifier, Constrictor.
We evaluate Constrictor on 51 examples of immutability-related design violations. Our evaluation shows that Constrictor is effective at catching a variety of prototypical design violations, and does so in seconds. We also explore Constrictor with two real-world case studies.
This program is tentative and subject to change.
Tue 17 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | |||
10:30 15mTalk | Defining Name Accessibility using Scope Graphs Technical Papers Link to publication Pre-print | ||
10:45 15mTalk | Rose: Composable Autodiff for the Interactive Web Technical Papers Sam Estep Carnegie Mellon University, Wode Ni Carnegie Mellon University, Raven Rothkopf Barnard College, Joshua Sunshine Carnegie Mellon University | ||
11:00 15mTalk | Failure Transparency in Stateful Dataflow Systems Technical Papers Aleksey Veresov KTH Royal Institute of Technology, Jonas Spenger KTH Royal Institute of Technology, Paris Carbone KTH Royal Institute of Technology, Philipp Haller KTH Royal Institute of Technology Pre-print | ||
11:15 15mTalk | Fair join pattern matching for actors Technical Papers Philipp Haller KTH Royal Institute of Technology, Ayman Hussein Technical University of Denmark, Hernan Melgratti University of Buenos Aires, Argentina, Alceste Scalas Technical University of Denmark, Emilio Tuosto Gran Sasso Science Institute, L'Aquila, Italy | ||
11:30 15mTalk | Constrictor: Immutability as a Design Concept Technical Papers Pre-print | ||
11:45 15mTalk | A Language-Based Version Control System for Python Technical Papers Luís Carvalho NOVA School of Science and Technology, João Costa Seco NOVA-LINCS; Nova University of Lisbon |