Back to Search
Start Over
Modular specification and verification of closures in Rust
- Source :
- Proceedings of the ACM on Programming Languages, 5 (OOPSLA)
- Publication Year :
- 2021
- Publisher :
- Association for Computing Machinery (ACM), 2021.
-
Abstract
- Closures are a language feature supported by many mainstream languages, combining the ability to package up references to code blocks with the possibility of capturing state from the environment of the closure's declaration. Closures are powerful, but complicate understanding and formal reasoning, especially when closure invocations may mutate objects reachable from the captured state or from closure arguments. This paper presents a novel technique for the modular specification and verification of closure-manipulating code in Rust. Our technique combines Rust's type system guarantees and novel specification features to enable formal verification of rich functional properties. It encodes higher-order concerns into a first-order logic, which enables automation via SMT solvers. Our technique is implemented as an extension of the deductive verifier Prusti, with which we have successfully verified many common idioms of closure usage.<br />Proceedings of the ACM on Programming Languages, 5 (OOPSLA)<br />ISSN:2475-1421
- Subjects :
- Computer science
Programming language
business.industry
Rust
Closures
High-order functions
Software verification
Extension (predicate logic)
computer.software_genre
Automation
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
Closure (computer programming)
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Code (cryptography)
State (computer science)
Safety, Risk, Reliability and Quality
business
computer
Formal verification
Software
Rust (programming language)
computer.programming_language
Subjects
Details
- ISSN :
- 24751421
- Volume :
- 5
- Database :
- OpenAIRE
- Journal :
- Proceedings of the ACM on Programming Languages
- Accession number :
- edsair.doi.dedup.....710eb2673735f52dcc8bd83f20d2c6ea