The has operator #

Syntax #

V@[has_expr] ::= V@[spec_expr]  has V@[spec_expr]
           | V@[spec_expr] !has V@[spec_expr]

Desugaring #

In spec code, the expression expr1 has expr2 desugars to expr1.spec_has(expr2), which is resolved as normal via Rust's standard method resolution.

Likewise, the expression expr1 !has expr2 desugars to !expr1.spec_has(expr2).

Examples #

We typically use the has operator to indicate that a collection contains a particular element. The vstd library provides several container types with spec_has functions defined, e.g., Set::spec_has and Multiset::spec_has.

Example:

proof fn test_set() {
    let s: Set<int> = set![1, 2];
    assert(s has 1);
    assert(s has 2);
    assert(s !has 3);
}

proof fn test_multiset() {
    let s: Multiset<int> = Multiset::empty().insert(1).insert(1).insert(2);
    assert(s has 1);
    assert(s has 2);
    assert(s !has 3);
}