Add push-pop example

[xldenis]

Currently the specification of Vec::pop is less than optimal: the encoding of match in the logic means that the code in the attached test is not automatically provable without a useless match. This is due to the lack of "triggers" for Why3 to break up the match in pop's post-condition in client code.

An alternative spec can be given in terms of a logical unwrap symbol, this effectively corresponds to changing the encoding of match in why3 to work in terms of 'accessors' rather than the current 'quantifier' approach.

Specifically, the spec would be:

#[ensures((result === None) ==> self.resolve() && (@self).len() === 0)]
#[ensures(!(result === None) ==> (@self) === (@^self).push(unwrap(result)))]

Supposing:

#[logic]
#[requires(!(o === None))]
#[ensures(o === Some(result))]
#[trusted]
fn unwrap<T>(o: Option<T>) -> T {
    std::process::abort()
}

Alternatively, user code can provide a trigger by using the value returned by pop, like shown in the attached example, a dummy match suffices.

I'm opening this PR to provide a place to discuss the broader question of handling logical matches in post-conditions. unwrap may work well enough for Result and None but doesn't scale well with larger or custom data-types and this is a dumb thing to trip over.