Missing axiom(s) in the axiomatization of sets

[viper-admin]

Created by bitbucket user OmerSakar on 2019-12-13 15:25

When reasoning about a set and its subset (using the subset operator), there seems to be an axiom missing that relates the size of the subset to the other set. See the example below.

‌

function setComp(): Set[Int]
ensures forall x: Int :: (x >= 0 && x <= 5) <==> (x in result)

method main2() {
    var set1: Set[Int] 
    set1 := setComp()
    
    assert Set(0, 1, 2, 3) subset set1 
    assert |set1| >= 4 // fails
}

Here we have a function setComp, its result is a set of integers between 0 to 5 (inclusive). In the method main3, we have a set set1 and we assign the result of the function setComp to it.

Reasoning directly about the size of the set is difficult (for example assert |set1| == 6 will not assert on its own). Instead we would like to reason about a lowerbound of the size, given that we can assert that some set (with a known size) is the subset of set1 (e.g. Set(0, 1, 2, 3)).

In the example, we assert that Set(0, 1, 2, 3) is a subset of set1 (on line 7). The expectation is that it can then be asserted that the size of set1 is greater or equal to 4 (as in line 8). Unfortunately, the last assertion fails.

After inspecting the set axioms Viper uses, I see that an axiom is missing which relates the size of the set and the subset.