Compositional Reasoning about Advanced Iterator Patterns in Rust
Iteration is a control-flow mechanism that consists of repeating statements. Iterators provide an object-oriented abstraction to iteration. Simple iterators confer access to elements of a data structure, but modern languages such as Rust, Java, and C# generalise iteration far beyond this simple use case, allowing iterators to be parameterised with closures (which can modify their captured state as a side effect) and supporting the composition of iterators to form iterator chains, where each iterator in the chain consumes values from its predecessor and produces values for its successor. Such generalisations pose four major challenges for modular specification and verification of iterators and the client code using them: (1) How can parameterised iterators be specified modularly and their (accumulated) side effects reasoned about? (2) How can the behaviour of an iterator chain be derived from the specifications of its component iterators? (3) How can proofs about such iterators be automated? (4) How to integrate a concrete methodology into the standard library, without requiring the client code to change?
We present a methodology for the modular specification and verification of advanced iteration idioms with computations affecting captured state as a side effect. It addresses the four challenges above using a combination of inductive two-state invariants, higher-order closure contracts, separation logic-like ownership, and a novel type of out-of-band contracts. We implement our methodology in a state-of-the-art SMT-based Rust verifier. Our evaluation shows that our methodology is sufficiently expressive to handle advanced, idiomatic iteration patterns and requires modest annotation overhead.
Tue 24 OctDisplayed time zone: Lisbon change
14:00 - 15:30
|A Mechanized Theory of the Box Calculus|
|Compositional Reasoning about Advanced Iterator Patterns in Rust|
Aurel Bílý ETH Zurich, Jonas Hansen ETH Zurich, Alexander J. Summers University of British Columbia, Peter Müller ETH ZurichFile Attached
|Oxidize: A Step-Debugger for Static Semantics|
Peter Chon Harvard University, Dimi Racordon Northeastern University, USA, Nada Amin Harvard UniversityFile Attached