test

fn map1(v: Vec<i32>) -> Vec<i32> {
    let mut r = Vec::new();
    for el in v {
        r.push(el + 1);
    }
    r
}

pres:
(\all 0 <= i < len(v) . v[i] < i32::MAX)

posts:
len(v) == len(result)
(\all 0 <= i < len(v) . result[i] == v[i] + 1)

req: f_pre(x)
ens: f_post(x, result)
fn f(x: i32) -> i32 { ... }

fn map2(v: Vec<i32>) -> Vec<i32> {
    let mut r = Vec::new();
    for (idx, el) in v.iter().enumerate() {
        r.push(f(el));
    }
    r
}

pres:
(\all 0 <= i < len(v) . f_pre(v[i]))

posts:
len(v) == len(result)
(\all 0 <= i < len(v) . f_post(v[i], result[i]))

struct Foo { .. }

req: f_pre(x)
ens: f_post(old(x), x, result)
fn f(x: &mut Foo) -> Foo { ... }

struct Foo { value: i32 }
fn f_example(x: &mut Foo) -> Foo {
    x.value += 1;
    Foo { value: 42 }
}

fn map3(v: &mut Vec<Foo>) -> Vec<Foo> {
    let mut r = Vec::new();
    for (idx, el) in v.iter_mut().enumerate() {
        r.push(f(&mut el));
    }
    r
}

pres:
(\all 0 <= i < v.len() . f_pre(v[i]))

posts:
v.len() == result.len()
(\all 0 <= i < v.len() . f_post(old(v[i]), &v[i], result[i]))