You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
Here we have a function
setComp
, its result is a set of integers between 0 to 5 (inclusive). In the methodmain3
, we have a setset1
and we assign the result of the functionsetComp
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 ofset1
(e.g.Set(0, 1, 2, 3)
).In the example, we assert that
Set(0, 1, 2, 3)
is a subset ofset1
(on line 7). The expectation is that it can then be asserted that the size ofset1
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.
The text was updated successfully, but these errors were encountered: