Closures

NOT YET SUPPORTED: This feature is not yet supported in Prusti. See PR #138 for the status of this feature as well as a prototype. The syntax described here is subject to change.

NOTE: The syntax for attaching specifications to closures is currently not working

Rust closures can be given a specification using the closure!(...) syntax:

use prusti_contracts::*;

fn main() {
    let cl = closure!(
        requires(a > b),
        ensures(result > b),
        |a: i32, b: i32| -> i32 { a }
    );
}

closure! can have any number of pre- and postconditions. The arguments and return type for the closure must be given explicitly. See specification entailments for specifying the contract of a higher-order function (e.g. when taking a closure as an argument).