Assertions about mutable references

Assertions containing mutable references allow us to make statements about the prior (at the beginning of the function call) and current state of the piece of memory to which the mutable reference points. Consider the following example:

fn check_and_assert(a: &mut u32)
    requires *old(a) == 0
{
    assert(*old(a) == 0);
    *a = *a + 1;
    assert(*a == 1);
    *a = *a + 1;
    assert(*a == 2);
    assert(*old(a) == 0);
}

fn asserts() 
{
    let mut x: u32 = 0;
    check_and_assert(&mut x);
}

In the check_and_assert function call, *old(a) refers to the dereferenced value of the mutable reference a at the beginning of the function call and *a refers to the current dereferenced value of the mutable reference a.

Below is a slightly more complicated example involving both assert, requires, and ensures:

fn decrease(b: &mut u32)
    requires
        *old(b) == 10,
    ensures
        *b == 0,
{
    let mut i: u32 = 0;
    while (*b > 0) 
        invariant
            *b == (10 - i),
        decreases *b,
    {
        *b = *b - 1;
        i = i + 1;
        assert(*b == (10 - i));
    }
    assert(*b == 0);
    assert(*old(b) == 10);
}

fn complex_example()
{
    let mut d: u32 = 10;
    decrease(&mut d);
    assert(d == 0);
}